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