Abstract
This chapter continues the description of checkers started in Chap 9. It focuses on the application of checkers to formal verification—composing non-deterministic abstract models. The main feature in checkers supporting non-determinism are free variables, which are introduced in this chapter. We also introduce a special case of free variables: constant free variables, also called rigid variables. We show how free and rigid variables can be used as an alternative to local variables, and discuss advantages and drawbacks of each approach. Another topic addressed in this chapter is the use of checkers as a synthesizable testbench—a DUT environment model supported both in simulation and in formal verification.
Hope is a great falsifier. Let good judgment keep her in check. — Baltasar Gracian
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
This is not true in simulation, where free variables are randomized and hold consistent values across all assertion statements. See Sect. 23.3.
- 2.
Ironically enough, bound variables in first-order logic correspond to free variables in SVA.
- 3.
- 4.
Recall (Sect. 7.2.2) that it is illegal to use future sampled value functions with arbitrary clocks, so we use a past value function here delayed by one clock tick.
- 5.
Since free variables may be assigned only within always_ff procedures and since a variable assigned in an always_ff procedure cannot be assigned in any other process (see Sect. 2.2.1.3), we can focus on a single always_ff procedure.
- 6.
If we assign one free variable to a second free variable, the second one may still be completely nondeterministic by virtue of the nondeterminism of the first. The point is that a free variable that is assigned loses its “own” nondeterminism. See also Sect. 23.2.2.4.
- 7.
Simulators may also do this.
- 8.
Multiple continuous assignments are allowed only for nets.
- 9.
The program does not have to be synthesizable to be represented in SSA form. The synthesizability is required for an efficient representation of the ϕ-function.
- 10.
This is highly dependent on the specific tool.
- 11.
If a free variable is of an aggregate data type—array or structure, some of its elements may be assigned, while others remain unassigned. The LRM defines that all elements of the singular data types (i.e., of all data types except unpacked ones) should be randomized monolithically, whereas different elements of the unpacked data types may be randomized independently: some elements may be randomized, while other may not.
- 12.
There are several subtleties concerning assumption set definition for procedural checker instantiations and for instances involving const cast of checker arguments. These are not covered here. Refer to the LRM [8] for the exact definitions.
- 13.
One should avoid using free variables in all forms of assertion statements but concurrent, see Sect. 23.3.4.
- 14.
This is our interpretation of the standard. The standard is not explicit about free variable randomization with deferred assumptions.
- 15.
It highly depends on the specific tool.
- 16.
In PSL, the construct similar to rigid variables is even called forall.
- 17.
Remember that this problem exists only in simulation. In FV the reset value is sampled even in disable iff clauses.
References
IEEE Std. 1800–2012, IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language (2012)
R. Cytron, J. Ferrante, B.K. Rosen, M.N. Wegman, F.K. Zadeck, Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)
S.S. Muchnick, Advanced Compiler Design and Implementation. (Morgan Kaufmann, San Francisco, 1973)
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Cerny, E., Dudani, S., Havlicek, J., Korchemny, D. (2015). Checkers in Formal Verification. In: SVA: The Power of Assertions in SystemVerilog. Springer, Cham. https://doi.org/10.1007/978-3-319-07139-8_23
Download citation
DOI: https://doi.org/10.1007/978-3-319-07139-8_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07138-1
Online ISBN: 978-3-319-07139-8
eBook Packages: EngineeringEngineering (R0)