Microprocessor Design Verification:Conclusions

By -
Conclusions

Microprocessor design teams use a combination of simulation and formal verification to verify presilicon designs. Simulation is the primary verification methodology in use, since formal methods are applicable mainly to well-defined parts of the RTL or gate-level implementation. The key problem in using formal verification for large designs is the unmanageable state space.

Simulation typically involves the application of a large number of pseudorandom or biased-random vectors in the expectation of exercising a large portion of the design’s functionality. However, random instruction generation does not always lead to certain highly improbable (corner case) sequences, which are the most likely to cause hazards during execution. This has led to the use of a number of semiformal methods, which use knowledge derived from formal verification techniques to cover more fully the design behavior. For example, techniques based on HDL statement coverage ensure that all statements in the HDL representation of the design are executed at least once. At a more formal level, a state graph of the design’s functionality is extracted from the HDL description, and formal techniques are used to derive test sequences that exercise all transitions between control states. Finally, formal methods based on the use of temporal logic assertions and symbolic simulation can be used to automatically generate simulation vectors. We next describe some current directions of research in verification.

Performance Validation

With an increasing sophistication in the art of functional validation, ensuring the lack of performance bugs in microprocessors has become the next focus of verification. The fundamental hurdle to automating performance validation for microprocessors is the lack of formalism in the specification of error-free pipeline execution semantics [26]. Current validation techniques rely on focused, handwritten test cases with expert inspection of the output. In Ref. [26], analytical models are used to generate a controlled class of test sequences with golden signatures. These are used to test for defects in latency, bandwidth, and resource size implementations coded into the processor model. However, increasing the coverage to include complex, context-sensitive parameter faults and generating more elaborate tests to cover the cache hierarchy and pipeline paths remain open problems.

Design for Verification

Design for verification (DFV) is the new buzzword in microprocessor verification today. With the costs of verification becoming prohibitive, verification engineers are increasingly looking to designers for easy-to-verify designs. One way to accomplish DFV is to borrow ideas from design for testability (DFT), which is commonly used to make manufacturing testing easier. Partitioning the design into a number of modules and verifying each module separately is one such popular DFT technique. DFV can also be accomplished by adding extra modes to the design behavior to suppress features such as out-of- order execution during simulation. Finally, a formal level of abstraction, which expresses the micro- architecture in a formal language that is amenable to assertion checking, would be an invaluable aid to formal verification.

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