- What Is Design Verification?
- The Basic Verification Principle
- Verification Methodology
- Simulation-Based Verification versus Formal Verification
- Limitations of Formal Verification
- A Quick Overview of Verilog Scheduling and Execution Semantics
- Summary
This chapter is from the book
This chapter is from the book
This chapter is from the book
1.4 Simulation-Based Verification versus Formal Verification
The most prominent distinction between simulation-based verification and formal verification is that the former requires input vectors and the latter does not. The mind-set in simulation-based verification is first to generate input vectors and then to derive reference outputs. The thinking process is reversed in the formal verification process. The user starts out by stating what output behavior is desirable and then lets the formal checker prove or disprove it. Users do not concern themselves with input stimuli at all. In a way, the simulation-based methodology is input driven and the formal methodology is output driven. It is often more straightforward to think in the input-driven way, and this tendency is reflected in the perceived difficulty in using a formal checker.
Another selling point for formal verification is completeness, in the sense that it does not miss any point in the input space—a problem from which simulation-based verification suffers. However, this strength of formal verification sometimes leads to the misconception that once a design is verified formally, the design is 100% free of bugs. Let's compare simulation-based verification with formal verification and determine whether formal verification is perceived correctly.
Simulating a vector can be conceptually viewed as verifying a point in the input space. With this view, simulation-based verification can be seen as verification through input space sampling. Unless all points are sampled, there exists a possibility that an error escapes verification. As opposed to working at the point level, formal verification works at the property level. Given a property, formal verification exhaustively searches all possible input and state conditions for failures. If viewed from the perspective of output, simulation-based verification checks one output point at a time; formal verification checks a group of output points at a time (a group of output points make up a property). Figure 1.6 illustrates this comparative view of simulation-based verification and formal verification. With this perspective, the formal verification methodology differs from the simulation-based methodology by verifying groups of points in the design space instead of points. Therefore, to verify completely that a design meets its specifications using formal methods, it must be further proved that the set of properties formally verified collectively constitutes the specifications. The fact that formal verification checks a group of points at a time makes formal verification software less intuitive and thus harder to use.
)
Figure 1.6 An output space perspective of simulation-based verification versus formal verification
A major disadvantage of formal verification software is its extensive use of memory and (sometimes) long runtime before a verification decision is reached. When memory capacity is exceeded, tools often shed little light on what went wrong, or give little guidance to fix the problem. As a result, formal verification software, as of this writing, is applicable only to circuits of moderate size, such as blocks or modules.