This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification
October 1995 (vol. 21 no. 10)
pp. 822-833
We describe the verification of a logic-synthesis tool with the Nuprl proof-development system. The logic-synthesis tool, Pbs, implements the weak-division algorithm. Pbs consists of approximately 1,000 lines of code implemented in a functional subset of Standard ML. It is a proven and usable implementation and is an integral part of the Bedroc high-level synthesis system. The program was verified by embedding the subset of Standard ML in Nuprl and then verifying the correctness of the implementation of Pbs in the Nuprl logic. The proof required approximately 500 theorems. In the process of verifying Pbs we developed a consistent approach for using a proof-development system to reason about functional programs. The approach hides implementation details and uses higher-order theorems to structure proofs and aid in abstract reasoning. Our approach is quite general, should be applicable to any higher-order proof system, and can aid in the future verification of large software implementations.

[1] R.K. Brayton and C. McMullen,“Decomposition and factorization of boolean expressions,” Int’l Symp. on Circuits and Systems, 1982.
[2] M.D. Aagaard and M.E. Leeser,“A methodology for efficient hardware verification,” Formal Methods in System Design, vol. 5, no. 1&2, pp. 95-117, July 1994.
[3] R.L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System.Englewood Cliffs, N.J.: Prentice Hall, 1986.
[4] M. Leeser,R. Chapman,M. Aagaard,M. Linderman,, and S. Meier,“High level synthesis and generating FPGAs with the BEDROC system,” J. of VLSI Signal Processing, vol. 6, no. 2, pp. 193-216, Aug. 1993.
[5] M.D. Aagaard,“A verified system for logic synthesis,” Master’s thesis, School of Electrical Engineering, Cornell Univ., Jan. 1992.
[6] M.D. Aagaard and M.E. Leeser,“A theorem proving based methodology for software verification,” Tech. Rep. Cornell CS:TR93-1335, Dept. of Computer Science, Cornell Univ., Mar. 1993.
[7] M.D. Aagaard and M.E. Leeser,“PBS: Proven Boolean simplification,” IEEE Transactions on Computer Aided Design, vol. 13, no. 4, Apr. 1994.
[8] J.M. Wing,“A specifier’s introduction to formal methods,” IEEE Computer, vol. 23, pp. 8-24, Sept. 1990.
[9] P.A. Lindsay,“A survey of mechanical support for formal reasoning,” Software Eng. J., pp. 3-27, Jan. 1988.
[10] D.R. Musser,“Abstract data type specification in the AFFIRM system,” IEEE Transactions on Software Engineering, vol. 6, no. 1, pp. 24-32, 1980.
[11] D. Kapur and P. Narendran,“The rewrite rule laboratory (RRL),” J. Siekman, ed., Conf. on Automated Deduction.New York: Springer-Verlag, July 1986.
[12] S.J. Garland and J.V. Guttag,“An overview of LP, the Larch proof assistant,” Rewriting Techniques, 1989, pp. 137-151.
[13] M. Broy,“Experiences with software specification and verification using LP, the Larch proof assistant,” Tech. Rep., 93, DEC Systems Research Center, 1992.
[14] D.I. Good,“Mechanical proofs about computer programs,” C.A.R. Hoare and J.C. Shepherdson, eds., Mathematical Logic and Programming Languages.Englewood Cliffs, N.J.: Prentice Hall, 1984.
[15] R. Boyer and J. Moore, A Computational Logic Handbook. New York: Academic Press, 1988.
[16] J. of Automated Reasoning, Dec. 1989, Special Issue on Boyer-Moore Theorem Prover.
[17] Y. Yu,“Automated proofs of object code for a widely used microprocessor,” Tech. Rep. 113, DEC Systems Research Center, Oct. 1993.
[18] M. Gordon,R. Milner,, and C. Wadsworth,Edinburgh LCF: A Mechanized Logic of Computation, vol. 78. New York: Springer Verlag, 1979, Lecture Notes in Computer Science.
[19] M.-J.-C. Gordon and T.-F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. ISBN 0-521-44189-7. Cambridge Univ. Press, 1993.
[20] L. Paulson and T. Nipkow,“Isabelle tutorial and user’s manual,” Tech. Rep. 189, Cambridge Univ. Computer Laboratory, Jan. 1990.
[21] N. Shankar,S. Owre,, and J.M. Rushby,“The PVS proof checker: A reference manual,” draft tech. rep., SRI International, 1993.
[22] A. Bundy,F. Van Harmelen,J. Hesketh,, and A. Smaill,“Experiments with proof plans for induction,” J. of Automated Reasoning, vol. 7, no. 3, pp. 303-324, 1991.
[23] T. Melham,“Formalizing abstraction mechanisms for hardware verification in higher order logic,” PhD thesis, Cambridge Univ. Computer Laboratory, Aug. 1990, Technical Report no. 201.
[24] J. Camilleri and T. Melham,“Reasoning with inductively defined relations in the HOL theorem prover,” Tech. Rep. 265, Univ. of Cambridge Computer Laboratory, Aug 1992.
[25] J. Rushby and F. von Henke, "Formal Verification of Algorithms for Critical Systems," IEEE Trans. Software Engineering, vol. 19, no. 1, pp. 13-23, Jan. 1993.
[26] ——,“The notion of proof in hardware verification,”J. Automated Reasoning, vol. 5, pp. 127–139, 1989.
[27] R.K. Brayton,R. Rudell, et al., “MIS: A multiple-level logic optimization system,” IEEE Transactions on Computer Aided Design, vol. 6, no. 6, 1987.
[28] R. Milner,M. Tofte,, and R. Harper,The Definition of Standard ML.Cambridge, Mass.: MIT Press, 1990.
[29] M. VanInwegen and E. Gunter,“HOL-ML,” J.J. Joyce and C.-J.H. Seger, eds., Higher Order Logic Theorem Proving and Its Applications.New York: Springer Verlag, 1993.
[30] D. Syme,“Reasoning with the formal definition of Standard ML in HOL,” J.J. Joyce and C.-J.H. Seger, eds., Higher Order Logic Theorem Proving and Its Applications.New York: Springer Verlag, 1993.
[31] S. Maharaj and E. Gunter,“Studying the ML module system in HOL,” T.F. Melham and J. Camilleri, eds., Higher Order Logic Theorem Proving and Its Applications.New York: Springer Verlag, pp. 346-361, 1994.

Index Terms:
Software verification, theorem proving, logic synthesis, weak division, hardware verification.
Citation:
Mark Aagaard, Miriam Leeser, "Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification," IEEE Transactions on Software Engineering, vol. 21, no. 10, pp. 822-833, Oct. 1995, doi:10.1109/32.469458
Usage of this product signifies your acceptance of the Terms of Use.