 |
Hybrid Decision Diagrams |
- Useful for verifying arithmetic circuits
- For state variables corresponding to datapath registers, behaves like a BMD
- BMDs have linear representation for some functions whose BDD representation has exponential complexity
- For state variables corresponding to control registers, behaves like an MTBDD
|
Hardware Verification
- Application of formal techniques to chip designs
|
Slide 16 of
30 |