The Forte Formal Verification System

Forte is a formal verification environment for datapath-dominated hardware developed by a team of researchers at Intel Corporation's Strategic CAD Labs. Forte combines an efficient linear-time logic model checking algorithm, Symbolic Trajectory Evaluation, with lightweight theorem proving in higher-order logic. These are tightly integrated in a general-purpose functional programming language, which allows the verification environment to be customised and large verification efforts to be organised and scripted effectively. The functional language at the heart of Forte also serves as an extensible specification language for verification properties.

The following paper gives a detailed account of Forte, the design philosophy behind it, and the verification methodology that makes it effective in practice:
C.-J. H. Seger, R. B. Jones, J. W. O'Leary, T. Melham, M. D. Aagaard, C. Barrett, and D. Syme,
‘An Industrially Effective Environment for Formal Hardware Verification’,
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 24, no. 9 (September 2005), pp. 1381-1405.

Background to the Forte Philosophy

Forte is an evolution of the HOL-Voss system, designed by Seger and Joyce in 1991 at the University of British Columbia as an experiment in using symbolic trajectory evaluation as a decision procedure for the HOL Theorem Prover. The key lessons learned from HOL-Voss were

Applying these lessons and incorporating new inference rules for trajectory evaluation, Seger and Hazelhurst created VossProver, a lightweight proof system built on top of Voss. The success of the VossProver approach was demonstrated by several case studies, including the verification of a pipelined IEEE-compliant floating-point multiplier by Aagaard and Seger.

These experiments with the VossProver approach supported the conclusions drawn from HOL-Voss, where the inability to interact directly with the model checker made the system difficult to use. By providing both theorem proving and model checking in the same environment, VossProver overcame the primary disadvantage of systems that treat model checking and theorem proving as disjoint activities. Some conclusions from analyzing the VossProver work were:

These insights were embodied in the architecture and design of the Forte system, developed by a team at Intel led by Carl Seger. A guiding principle in the design of Forte was the view that formal verification as an interactive activity, with the major result being a set of proof scripts that can be used for debugging and regression, and re-used in future verification efforts targeting similar functionality. Proof script development is seen as program development, in a programming envionment that tightly integrates symbolic trajectory evaluation and lightweight theorem proving within a general-purpose functional programming language. This allows the environment to be customized and large proof efforts organized and scripted effectively. The functional language also provides an expressive specification language at a level much above temporal logic primitives.

Papers on Forte Applications

Here are some papers that describe the use of Forte in formal hardware design verification:

Tom Melham, last updated in April 2007.