mulverif – Verification of multiplier circuits with *BMDs
Introduction
mulverif is a small Haskell program for the formal verification of multiplier circuits, written during my long internship at Chalmers University of Technology in 2002, under the supervision of Mary Sheeran. Circuits are described with the Lava hardware description library; the program builds the binary moment diagram (*BMD) of a circuit backwards from its outputs, compares it with the *BMD of the multiplication function, and can also delegate some proof obligations to the E theorem prover. It is described in the following report:
- Vérification automatique des multiplicateurs (internship report, in French, 2002).
Download
The code is provided as is, as it was left in 2002, for research purposes. It requires the Lava library for GHC of that time and the BXD package of Yirng-An Chen (Carnegie Mellon University) for *BMD manipulation, which is not redistributed here because its license restricts it to internal use.