A Functional Language for Hardware Modelling and Verification with Metaprogramming and Reflection

Speaker: Tom Melham

1st December 2004 , 2pm , Room 519, Claremont Tower

Abstract

Forte is a formal verification system developed by Intel's Strategic CAD Labs for applications in hardware design and verification. Forte integrates model checking and theorem proving within a functional programming language, which both serves as an extensible specification language and allows the system to be scripted and customized. Forte's functional programming language is also the underlying term language for the higher order logic of its theorem prover.

The latest version of this language, called reFLect, has quotation and antiquotation constructs similar to those in LISP, but typed. These build and decompose expressions in the language itself and provide a combination of pattern-matching and metaprogramming features tailored especially for the Forte applications. The addition of some reflection principles in the higher order logic based on reFLect also provides a framework for making a logically principled connection between theorems in higher-order logic, program execution in the reFLect language, and the results of model checking verifications.

This talk will describe the design philosophy and architecture of the Forte system and give an account of the reFLect functional language and its role in Forte.

This is joint work with Jim Grundy and John O'Leary of Intel Corporation.

------
Tom Melham
Professor of Computer Science
Tutorial Fellow at Balliol College
Oxford University Computing Laboratory