Formal Verification of a Basic Circuits Library
Christoph Berg, Christian Jacobi, Daniel Kroening · 2001
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