 |
Verifying Compliance of Intel Floating-Point Hardware |
Used internal formal verification system, Forte,
an evolution of the VOSS system
- Seamlessly integrates several types of model-checking engines with lightweight theorem proving and extensive debugging capabilities
- Model checkers:
- Based on symbolic trajectory evaluation
- Word-level model checker (linear-time checker tailored to verifying arithmetic circuits, based on Hybrid Decision Diagrams
- Design partitioned to manage complexity, with lightweight theorem prover used to guarantee that no mistakes were made in the partitioning process
- Forte system includes significant support for efficient debugging
|
Hardware Verification
- Application of formal techniques to chip designs
|
Slide 29 of
30 |