Formal Verification of a Basic Circuits Library

Abstract

We describe the results and status of a project aiming to provide a provably correct library of basic circuits. We use the theorem proving system PVS in order to prove circuits such as incrementers, adders, arithmetic units, multipliers, leading zero counters, shifters, and decoders. All specifica-tions and proofs are available on the web. 1