The formal verification of assembler code using hardware verification tools requires memory components, which e.g. hold the code itself and the processed data. Since the count of variables to be proven usually rises with both data-size and address-space, complexity boundaries of formal tools can be reached quickly. Since bounded model checking (BMC) always involves a certain time window and therefore the count of memory accesses is limited, it is possible to optimize the applied memory as far as the address-space and the size in the count of gates is concerned. In this paper we introduce various memory models, which decrease the complexity of formal proofs by applying such optimizations. We provide examples of models with limitations either of the address-space or the amount of storable data. Our analysis shows that these models remarkably enhance the performance, while verifying the instruction-set of a given processor-unit with our in-house BMC-Tool

The tester-related simulation environment (TRSE) and applied methodology close the gap between physical test and simulation. Simulation checks the correctness of the implementation with respect to the specification, and test checks the correctness of the fabricated product with respect to the implementation. Unfortunately, simulation and test are still not connected in a smooth verification flow. Test cases and stimuli from simulation cannot be directly used for test. They may be used only in a restricted way, and after some adaptation. The approach presented here allows a better reuse of simulation stimuli for test issues. The main idea consists of inserting a special simulation element (SE) called a "transforming SE". This transforming SE is responsible for the adaptation and single cycle relation of the pattern. It also traces the interface pattern for direct use on a tester. These patterns are finally used for deriving test programs from functional patterns and for providing patterns for an e-beam analysis of the manufactured chip. The second main feature of the TRSE is the connection of each SE with an appropriate reference clock. This enables the SE to provide both synchronous and asynchronous communication with the unit under verification (UUV). Both the modeling of a test case and general methodology issues have a big influence in how easily a pattern can be adapted for the tester. Some practical modeling and methodology hints are given.

This paper presents a new technology that accelerates functional system verification. Starting with a behavioral testbench, we developed a seamless flow to generate a re-use-oriented architecture for a synthesizable testbench without loosing compatibility towith the original testbench. Consequently, we combine the flexibility of a behavioral testbench and the simulation performance of a synthesizable testbench, while greatly reducing the modeling overhead.The approach itself is hardware independent. To prove the usability of our approach, we verified a hard disc controller on an emulator. With this setup, we achieved a speed-up factor of 5000 versus plain simulation.