Coverage-Based Microprocessor Verification

Microprocessor Verification

• DAC94: Panel: Microprocessor Testing: Which Technique is Best?
• Synthesis of Self-Testable ASICs
• Cycle-based simulation
  Cycle-Based Simulators use computational methods that eliminate unnecessary calculations to achieve huge performance gains in verifying Boolean logic: 1.) Results are only calculated at the end of every clock cycle; 2.) The digital logic is the only part of the design simulated (no timing calculations); and 3.) Typically, only two logic states (1s, & 0s) are computed. By limiting the calculations, Cycle-based simulators can provide very large increases in performance over conventional Event-driven simulators.
  In comparison, Event-driven Simulator methods sacrifice performance for rich functionality: every active signal is calculated for every device it propagates through during a clock cycle. Full Event-driven simulators support: 4 to 28 states; simulation of Behavioral HDL, RTL HDL, gate, and transistor representations; full timing calculations for all devices; and the full HDL standard. Cycle Simulators only focus on the logic and therefore can highly optimize the calculations for that one function.
• Tools for System-Level Digital Design - Stanford
  The most important innovation in system-level validation will be combining simulation and verification so that the user can choose a mixture of the two that obtains maximum coverage while keeping the computational problem manageable. In addition, we plan to speed up simulation by using new compilation and hardware emulation techniques, and extend the scope of verification by using new, more powerful symbolic representations.
• Automatic Verification of The Microprocessor Design - Stanford
  We are developing tools to automatically verify the microprocessor design. A symbolic simulator is developed to translate descriptions of the processor implementation and specification into corresponding next state functions. The matching states of the implementation and specification are extracted from these next state functions. These matching states are verified by a validity checker. To speed up the verification, a automatic invariant extraction method is also needed since invariants guarantee that the validity checker does not give any false negative result.