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