 |
Symbolic Trajectory Evaluation |
- VERSYS symbolic trajectory evaluation tool
- Based on VOSS tool (from UBC/CMU)
- Trajectory formulas
- Boolean expressions with the temporal "next-time" operator
- Ternary valued states represented by a Boolean encoding
-
Properties of the type
Antecedent implies Consequent - Antecedent and consequent are trajectory formulas
- Antecedent sets up the stimulus and the state of the circuit
- Consequent specifies the constraint on the state sequence
|
Hardware Verification
- Application of formal techniques to chip designs
|
Slide 27 of
30 |