A formal HDL and its use in the FM9001 verification

TLDR

The paper formalizes a synchronous, hierarchical, occurrence‑oriented HDL using Boyer‑Moore logic. The authors formalize the HDL, define a well‑formedness predicate and a unit‑clock simulator, and mechanically prove the FM9001 implementation with the Boyer‑Moore theorem prover, involving over 700 function definitions and millions of inference steps. Using the HDL, the authors mechanically proved that an FM9001 microprocessor implementation satisfies its instruction‑level specification.

Abstract

A synchronous, hierarchical, occurrence-oriented, hardware description language (HDL) has been formalized with the Boyer-Moore logic. Well-formed HDL circuits are recognized by a predicate, and a unit-clock simulator defines the meaning of circuits expressed in the HDL. This HDL has been used to specify an implementation of the FM9001 microprocessor that has been mechanically proved to implement the FM9001 instruction-level specification. All proofs were mechanically checked using the Boyer-Moore theorem-proving system. The formalization of the HDL, the FM9001 user-level specification, and the FM9001 HDL implementation architecture specification required more than 700 function definitions. The mechanical proof is composed of thousands of theorem prover proof requests and millions of theorem prover inference steps.