VERIFYING A LOGIC-SYNTHESIS ALGORITHM AND IMPLEMENTATION - A CASE-STUDY IN SOFTWARE-VERIFICATION

We describe the verification of a logic-synthesis tool with the Nuprl proof-development system. The logic-synthesis tool, Pbs, implements th e weak-division algorithm. Pbs consists of approximately 1,000 lines o f code implemented in a functional subset of Standard ML. It is a prov en and usable implementation and is an integral part of the Bedroc hig h-level synthesis system. The program was verified by embedding the su bset of Standard ML in Nuprl and then verifying the correctness of the implementation of Pbs in the Nuprl logic. The proof required approxim ately 500 theorems. In the process of verifying Pbs we developed a con sistent approach for using a proof-development system to reason about functional programs. The approach hides implementation details and use s higher-order theorems to structure proofs and aid in abstract reason ing. Our approach is quite general, should be applicable to any higher -order proof system, and can aid in the future verification of large s oftware implementations.