*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.

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.

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

- From the same prompt, the user must be able to interact directly with either the model checker or the proof tool.
- More time is spent in model checking and debugging than in theorem proving.

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:

- When model checking, the user must be unencumbered by artifacts from the theorem prover.
- The specification language for model checking must support simple and useful inference rules.
- The theorem prover and model checker must use the same specification language.
- Even if a proof system has a very narrow focus it should include a general-purpose specification language.

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

- R. Kaivola and K. Kohatsu,
‘Proof engineering in the large: formal verification of pentiumŪ4 floating-point divider’,
*International Journal on Software Tools for Technology Transfer*, vol. 4, no. 3 (May 2003), pp. 323-334. - M. D. Aagaard, R. B. Jones, R. Kaivola,
K. R. Kohatsu, and C.-J. H. Seger,
‘Formal
Verification of Iterative Algorithms in Microprocessors’,
*DAC '00: Proceedings of the 37th Conference on Design automation*(ACM Press, 2000), pp. 201-206. - R. Kaivola and M. D. Aagaard, ‘Divider Circuit
Verification with Model Checking and Theorem Proving’, in
*Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000: Proceedings*, edited by M. Aagaard and J. Harrison, LNCS, vol. 1869 (Springer-Verlag, 2000), pp. 338-355. - J. O'Leary, X. Zhao, R. Gerth, and C.-J. H. Seger,
‘Formally Verifying IEEE
Compliance of Floating-Point Hardware’,
*Intel Technical Journal*, First quarter, 1999. - M. D. Aagaard, R. B. Jones, and C.-J. H. Seger,
‘Combining Theorem Proving and Trajectory Evaluation
in an Industrial Environment’, in
*ACM/IEEE Design Automation Conference*, 1998, pp. 538-541.