 |
Symbolic Simulation |
Exhaustive verification: N-input NAND requires 1 vector and N variables
Antecedent: A = "a" (t0,t1) and B = "b" (t0,t1)
["a" and "b" are Boolean variables]Consequent: C = [~(a AND b)](t1,t2)
|
Hardware Verification
- Application of formal techniques to chip designs
|
Slide 26 of
30 |