Microprocessor Design Verification:Wide Simulation

By -
Wide Simulation

Near the formal end of the verification spectrum, wide simulation is performed by representing the FSM behavior as a set of transitions between valid control states and symbolically representing large sets of states in relatively few simulations. Assertions covering all the transitions in the state graph are written and are used to derive vectors for simulation.

Partitioning FSM Variables

Geist et al. [23] first focus on specific parts of the design by partitioning the FSM variables into three sets, coverage Co, ignore Ig, and care Ca, based on their respective importance. Using these sets, the number of transitions in the graph that need to be exercised can be reduced.

For example, a state in the FSM is viewed as the 3-tuple {X, Y, Z}, where X ∈Co, Y ∈Ig, and Z ∈Ca.

Two transitions, T1((X1, Y1, Z1), (X2, Y2, Z2)) and T2((X3, Y3, Z3), (X4, Y4, Z4)), which differ in the value of a coverage variable, are distinct and require separate tests; e.g., if X1 * X3 or X2 * X4, then T1 and T2 require different tests. However, two transitions that differ only in the value of an ignored variable are equivalent. Therefore, if X1 = X3, X2 = X4, Z1 = Z3 and Z2 = Z4, then T1 and T2 are equivalent and a vector that tests T1 will also test T2. Finally, two transitions that differ in the value of a care variable do not necessarily require different tests [23].

In this manner, the state graph is represented as the set of all valid transitions T, of which only a few must be exercised, based on the equivalence relations. Next, formal assertions are written for each transition. An assertion is a temporal logic expression of the form antecedent → consequent, where both antecedent and consequent can consist of complex logical expressions [13]. The first step

in the test generation process is to choose a valid transition T1(v, v ′) ∈T and write an assertion of the form state (v) → next (–state(v ′)), which means that if the FSM is in state v, then the next state cannot be v ′.

Deriving Simulation Tests from Assertions

A model checker may be used to generate sequences of input vectors which satisfies the assertion [23]. A model checker is a formal verification tool that is used either to prove that a certain property is satisfied by the system or to generate a counterexample to show that the property does not always hold true. The model checker reports that the assertion state(v) → next(–state(v′)) is false and that the transition is indeed valid. The model checker also outputs a symbolic sequence of states and input patterns which lead to state v. This symbolic (high-level) sequence of patterns is then translated into a simulation vector sequence and is used to verify the design. The transition T1 and all transitions equivalent to T1 are removed from T, and the process is repeated [23].

Wang and Abadir [13,14] use tools to automatically generate formal assertions for PowerPCTM arrays from the RTL model. Symbolic trajectory evaluation, a descendant of symbolic simulation, is used to formally prove that all assertions are true. After the design has been formally verified, simulation vectors are derived from the assertions and are used for simulating the design. The methods used to derive these vectors are as follows. The symbolic values used in the antecedent of each assertion are replaced with a set of vectors based on each condition specified in the consequent. First, symbolic address comparison expressions are replaced with address marching sequences, e.g., to test large decoders. Next, symbolic data comparison expressions are replaced with data marching sequences, e.g., in testing comparators. Stand-alone symbolic values representing sets of states or input patterns are replaced with random vectors. Assertion decision trees are constructed and tests are generated to cover all branches, e.g., in testing control logic. Finally, control signal decision trees are constructed in order to generate tests that cover abnormal functional space [13].

Finally, we have reached the formal end of our discussion on verification techniques, which range from random simulation to semiformal verification. Formal verification, which uses mathematical formulae to prove correctness, is described by Levitan in Chapter 11. In Section 64.8, we describe emulation, which is a means to implement a design using programmable hardware, with performance several orders of magnitude faster than conventional software simulators. Emulation has become popular as a means to test a processor against real-world application programs, which are impossibly slow to run using simulation.

Comments

Post a Comment

Popular posts from this blog

SRAM:Decoder and Word-Line Decoding Circuit [10–13].

By -
Image
Decoder and Word-Line Decoding Circuit [10–13] Two kinds of decoders are used in SRAM: the row decoder and the column decoder. Row decoders are needed to select one row of word-lines out of a set of rows in the array. A fast decoder can be implemented by using AND/NAND and OR/NOR gates. Figure 52.7 shows the schematic diagrams of static and dynamic AND gate decoders. The static NAND-type structure is chosen due to its low power consumption, that is, only the decoded row transitions. The dynamic structure is chosen due to its speed and power improvement over conventional static NAND gates. From a low-voltage operation standpoint, a dynamic NOR-base decoding would provide lower delay times through the decoder due to the limited amount of stacking of devices. Figure 52.8 shows circuit diagrams of dynamic NOR gates. The dynamic CMOS gate as shown in Figure 52.8(a) consists of input- NMOSs whose drain nodes are precharged to a high level by a PMOS when a clock signal Φ is at a low lev...
Read more

ASIC and Custom IC Cell Information Representation:GDS2

By -
Image
GDS2 The Graphical Design System (GDS) format is a binary format developed by Calma Company in 1971 to convey IC layout information between IC designers and fabricators. Calma presented GDS2 format, the improved version of GDS, in 1978. Finally in 1991, when Cadence acquired Calma, GDS2 rights were transferred to it. In the design process, after the completion of routing and placement, design rule check (DRC) and layout versus schematic (LVS) are performed to verify the final layout. Then the verified layout, dumped in a GDS2 file, is transferred to IC foundries for fabrication. GDS2 File Format GDS2 is a standard mask layout intermediate format containing a single cell or a library of cells each of which includes a number of geometrical objects such as boundaries, paths, boxes, etc. These objects correspond to different layers of a cell where each layer is specified by a layer number and data type [3]. The file format of GDS2 is in binary. A GDS2 file contains a number of variable...
Read more

Timing Description Languages:SDF

By -
Image
SDF Standard Delay Format (SDF) is an ASCII format used to convey timing information between EDA tools. SDF was first developed by Cadence in 1990. Open Verilog International (OVI) approved SDF version 2 in 1993 and SDF version 2.1 and 3 in the following years. Improving SDF version 3 features, resulted in IEEE Standard 1497 [1]. Role of SDF in Design Process SDF can be used in different levels of a design process to annotate timing specifications, including timing data and constraints. Timing constraints are used during the forward-annotation process while timing data are applied during the back-annotation process. Forward-annotation process deals with porting timing constraints to synthesis, floorplanner, layout, and routing tools to meet the required constraints. During the design process, timing data can be back-annotated to analysis tools (including simulators, static timing analysis tools, etc.) to provide more accurate timing representations. SDF Structure An SDF f...
Read more