Forte is our custom-built verification environment, evolved from Seger's Voss system. Forte integrates model-checking engines, BDDs, circuit manipulation functions, theorem proving, and a functional programming language called 'FL'. Forte compiles standard HDL source code into formal circuit models, and includes tightly integrated graphical interfaces for the display of circuit structures and waveforms.

FL is a strongly typed, lazy, functional programming language. A distinguishing feature is that BDDs are built into the language and every object of the Boolean type 'bool' is represented as a BDD. FL provides a flexible interface for invoking and orchestrating model checking runs, serves as an extensible 'macro language' for expressing specifications, and provides the control language for Forte's theorem prover. This architecture makes Forte a generic, open framework where solutions can be tailored to individual verification problems.

Forte includes graphical tools for FL programming and debugging. In addition, Forte provides extensive, interactive circuit visualization capabilities through three different interfaces: a node browser, a circuit browser, and a waveform viewer. The 'node' browser acts as a search interface for circuit signals, constructs, and interfaces. The waveform viewer displays bit and vector waveforms from both scalar and symbolic simulation. The circuit browser draws gate-level representations of circuits and provides facilities for traversing hierarchy, displaying special circuit constructs, and controlling the depth of fanin displayed.

Symbolic Trajectory Evaluation (STE) performs model checking with an algorithm based on symbolic simulation that is significantly more efficient at datapath verification than more conventional model checking. As a scalar simulator, STE computes the result of executing a circuit with concrete Boolean test vectors as inputs. As a symbolic simulator, it computes signal values as symbolic expressions in terms of arbitrary inputs. As a model-checker, it automatically checks the validity of a simple temporal logic formula for arbitrary inputs—computing an exact characterization of the region of disagreement if the formula is not unconditionally satisfied. STE's straightforward migration between scalar simulation, symbolic simulation, and verification is crucial in satisfying our methodology's requirement for early results, a tight debug loop, and recoverability.

Because the capacity limits of model-checking force many verification tasks to be decomposed, Forte includes ThmTac, a higher-order logic theorem-proving system. ThmTac is a 'lightweight' theorem prover, in that it is optimized for composing and decomposing model-checking results, rather than formalizing arbitrary mathematical theories. ThmTac is implemented in FL and is tightly integrated with the Forte model-checkers. As a result, Thmtac works directly on model-checking results and there is no need for translation or reformulation.