Information Technology Reference
In-Depth Information
Property to be
proved
STE
ste_init
initial states
SMC/
BMC
result or
unpruned model
counter-example
environment
pruning
pruned model
FIGURE 19.10
Overview of MIST prototype system.
The verification process starts by running the original model using STE and
computing the initial states for SMC. After that, the parametric representations are
converted to characteristic representations. The SMC tool then is invoked. First, the
large model is pruned automatically using the pruning directives. The resultant model
then is model checked, taking into account the starting state. Although, in MIST, we
must provide some additional information, but the benefit is the reduced cost in
modeling the environment and the performance improvements. Figure 19.10 shows
the MIST steps.
19.4.4.3 Evaluating MIST: A Hybrid Verification Approach.
MIST is a
hybrid method of verification using STE, BMC, and SMC. We can to use the power of
STE to deal with large circuits directly to improve ease of specification, performance,
and productivity. It reduces the work required by the user. The user also can have
much higher confidence in the result, as the validity of the result will not be affected
by the modeling of the environment.
The application of this hybrid approach on real-life industrial test cases shows
that MIST significantly can boost the performance and capacity of SAT/BDD-based
symbolic model checking. Moreover, this methodology enables the verification en-
gineer to have much more control over the verification process, facilitating a better
debugging environment (Yuan et al., 1997).
The insight that initialization is a very important part of the verification of many
systems may be helpful in other flows and verification methodologies.
19.5
BASIC FUNCTIONAL VERIFICATION STRATEGY
The functional verification is based on the idea that some specification implemented
at two different levels of abstraction may have its behaviors compared automatically
by a tool called the test bench.
Search WWH ::
Custom Search