Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification
by Mark Aagaard, Miriam Leeser
Proceedings of Computer Aided Verification: Proceedings of the Fourth International Workshop (CAV'92)
- unofficial copies PDF
We have proved a logic synthesis tool with the Nuprl proof development system. The logic synthesis tool, Pbs, implements the weak division algorithm, and is part of the Bedroc hardware synthesis system. Our goal was to develop a proven and usable implementation of a hardware synthesis tool. Pbs consists of approximately 1000 lines of code implemented in a functional subset of Standard ML. The program was verified by embedding this subset of SML in Nuprl and then verifying the correctness of the implementation of Pbs in Nuprl. In the process of doing the proof we learned many lessons which can be applied to efforts in verifying functional software. In particular, we were able to safely perform several optimizations to the program. In addition, we have invested effort into verifying software which will be used many times, rather than verifying the output of that software each time the program is used. The work required to verify hardware design tools and other similar software is worthwhile because the results of the proofs will be used many times.
Mark Aagaard is supported by a fellowship from Digital Equipment Corporation. This research was supported in part by the National Science Foundation under Award No. MIP-9100516.
bibTex ref: Aag93