Abstract
A methodology for mechanically verifying generic adder circuits is proposed using the rewrite-rule based theorem prover Rewrite Rule Laboratory (RRL). Proofs of properties of adder circuit descriptions are done by rewriting and induction. Carry lookahead adder circuit is described using powerlists, a data structure introduced by Misra to support divide-and-conquer strategy used for designing data-parallel algorithms. This description uses an algorithm for parallel prefix computation on powerlists due to Adams. Reasoning about properties of this algorithm can be of independent interest since parallel prefix operator has been found useful in many data-parallel algorithms. The correctness of the carry-lookahead adder (i.e., the adder indeed implements addition on numbers) is established by showing its equivalence to a recursive description of the ripple-carry adder, which is shown to correctly implement addition on natural numbers. The ripple carry adde r circuit is described in two different but equivalent ways: using powerlists employing the divide-and-conquer strategy, as well as using linear lists employing the linear decomposition strategy. The description of the ripple carry adder using powerlists is useful for showing equivalence of its input-output behavior to that of carry lookahead adder, whereas the description using linear lists is useful for showing its correctness with respect to addition on natural numbers. Descriptions of adder circuits using powerlists are based on Adams' work who also gave a hand proof of their correctness using the powerlist algebra. The emphasis in this paper is to generate proofs mechanically by a theorem prover . RRL exploits the algebraic laws of the powerlist algebra as rewrite rules, and uses heuristics for mechanizing proofs by induction using the cover set method to generate such proofs. The regularity in hardware circuits gets refl ected in compact descriptions generated using the divide-and-conquer strategy as well as in mechanically generated proofs by induction. Mechanical proofs generated by RRL closely follow the well-crafted hand-proofs which is quite encouraging. A comparison with Adams' hand generated proof is also made. There is strong evidence that the proposed methodology for generating proofs should scale up for large circuits exhibiting regularity that can be described using divide-and-conquer strategy in terms of powerlists.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
C.M. Angelo, L. Claesen, and H. De Man. A Methodology for proving correctness of parameterized hardware modules in HOL,, CHDL'91, (eds. D. Borrione and R. Waxman), Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 1991.
C.M. Angelo. Formal Hardware Verification in a Silicon Compilation Environment by Means of Theorem Proving. Ph.D. Thesis, IMEC / Katholieke Universiteit Leuven, Belgium, February 1994.
W. Adams. Verifying adder circuits using powerlists, University of Texas at Austin, CS. Dept Tech. Report, CS-TR-94-02, 1994.
D.A. Basin and N. Klarlund. Hardware verification using monadic second-order logic. Mathematical Induction Workshop, Dagstuhl, Germany, Aug. 1995.
R.S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, New York, 1988.
R.P. Brent and H.T. Kung. A regular layout for parallel adders. In E. E. Swartzlander, editor, Computer Arithmetic, Volume II. IEEE Computer Society Press, 1990.
R.E. Bryant. Graph-based Algorithms for boolean function manipulation”, IEEE transactions on Computers, C-35, 1986.
R.E. Bryant, and Y.-A. Chen. Verification of arithmetic functions with binary moment diagrams. Technical Report CMU-CS-94-160, Carnegie Mellon University, June 1994.
J.R. Burch, E.M. Clarke, K. L. Mcmillan and D.L. Dill. Sequential circuit verification using symbolic model checking. In Proc. 27th ACM/IEEE Design Automation Conference, 1990.
A.J. Camilleri, M.J.C. Gordon and T.F. Melham. Hardware verification using higher-order logic. In D. Borrione, editor, HDL Descriptions to Guaranteed Correct Circuit Designs. North-Holland, Amsterdam 1987, pages 43–67.
E.M. Clarke, S.M. German and X. Zhao. Verifying the SRT division algorithm using theorem proving techniques. In Proc. Computer Aided Verification, 8th Intl. Conf.-CAV'96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, July/August 1996, pages 111–122.
A.J. Cohn. A proof of Correctness of the Viper microprocessors: The first level. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, Boston, 1992, pages 27–72.
T.H. Cormen, C.E. Leiserson, and R.L. Rivest. Introduction to Algorithms. MIT Press, 1991.
D. Cyrluk, S. Rajan, N. Shankar, and M.K. Srivas. Effective theorem proving for hardware verification. In R. Kumar and T. Kropf, editors, Proc. 2nd Conf. on Theorem Provers in Circuit Design, September 1994.
B C. Brock, W.A. Hunt and M. Kaufmann. The FM9001 microprocessor proof. Technical Report 86, CLI, December 1994.
A. Gupta and A.L. Fisher. Parametric circuit representation using inductive boolean functions. In C. Courcoubetis, editor, em Proc. Computer Aided Verification, volume 697 of Lecture Notes in Computer Science, Springer, Berlin, 1993.
W.A. Hunt and B.C. Brock. The Verification of a bit-slice ALU. Proc. Workshop on Hardware Specification, Verification and Synthesis: Mathematical Aspects, volume 408 of Lecture Notes in Computer Science, Springer, Berlin, 1989.
W.A. Hunt. Jr. FM8501: A Verified Microprocessor. Ph.D thesis, University of Texas at Austin, 1985.
V. Stavridou, T.F. Melham and R.T. Boute, editors. Theorem Provers in Circuit Design, IFIP Transactions. North-Holland, 1992.
L.C. Paulson. The foundations of a generic theorem prover. Journal of Automated Reasoning, 5, 1989.
J. Joyce, G. Birtwistle and M. Gordon. Proving a computer correct in HOL. Technical Report 100, Computer Lab. University of Cambridge, 1986.
D. Kapur. Constructors can be partial too. In R. Veroff, editor, Essays in Honor of Larry Wos. MIT Press, Cambridge, MA, 1996.
D. Kapur. Automated tools for analyzing completeness of specifications. In Proc. 1994 Intl. Symp. on Software Testing and Analysis (ISSTA), Seattle, WA, August 1994, pages 28–43.
D. Kapur. Rewriting, decision procedures and lemma speculation for automated hardware verification. Invited Talk. In Proc. Theorem Provers in Higher-order Logics, New Jersey, August 1997.
D. Kapur and D.R. Musser. Tecton: A framework for specifying and verifying generic system components. Invited Talk. In TPCD Conf. 1992 (Theorem Provers in Circuit Design), University of Nijmegen, Netherlands, June 1992.
D. Kapur, D.R. Musser and X. Nie. An Overview of the Tecton proof system, Theoretical Computer Science Journal, 133:307–339, October 1994.
D. Kapur and X. Nie. Reasoning about numbers in Tecton. In Proc. 8th Intl. Symp. Methodologies for Intelligent Systems, (ISMIS'94), Charlotte, North Carolina, October 1994, pages 57–70.
D. Kapur and M. Subramaniam. Automated reasoning about parallel algorithms using powerlists. In V.S. Alagar, editor, Proc. AMAST'95, Springer, July 1995.
D. Kapur and M. Subramaniam. Mechanically verifying a family of multiplier circuits. In Proc. Computer Aided Verification (CAV'96), volume 1102 of Lecture Notes in Computer Science, Springer, Berlin, 1996, pages 135–146.
D. Kapur, and H. Zhang. An overview of Rewrite Rule Laboratory (RRL). Journal of Computer and Mathematics with Applications, 29:91–114, 1995.
C.A. Mead and L.A. Conway. Introduction to VLSI Systems. Addison-Wesley, Reading MA, 1980.
J. Misra. Powerlist: A structure for parallel recursion. In A Classical Mind: Essays in Honor of C.A.R. Hoare. Prentice Hall, January 1994. Also in TOPLAS, November 1994.
P. Narendran and J. Stillman. Hardware verification in the interactive VHDL workstation. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis. Kluwer Academic Publishers, Boston, 1988, pages 235–255.
P. Narendran and J. Stillman. Formal verification of the Sobel image processing chop. In Proc. Design Automation, 1988.
W. Pratt. Digital Image Processing. John Wiley &Sons, Inc., 1978.
M. Sheeran and G. Jones. Circuit design in Ruby. In J. Staunstrup, editor, Formal Methods for VLSI Design. Elsevier, 1990.
L. Rossen. Ruby Algebra. In G. Jones and M. Sheeran, editors, Designing Correct Circuits. Springer-Verlag, 1990.
M. Srivas and M. Bickford. Formal Verification of a pipelined microprocessor. IEEE Software, September 1990.
M. Subramaniam. Failure Analyses of Induction Theorem Provers. Ph.D Thesis, SUNY at Albany, September 1996.
D. Verkest, L. Claesen and H. De Man. Correctness Proofs of Parameterized Hardware Modules in the Cathedral-II Synthesis Environment. In EDAC'90, Glasgow, Scotland, March 1990.
D. Verkest, L. Claesen and H. De Man. On the Use of the Boyer-Moore Theorem Prover for Correctness Proofs of Parameterized Hardware Modules. In L. Claeson, editor, Formal VLSI Specification and Synthesis: VLSI Design Methods I. Elsevier Science Publishers B. V. (North-Holland), 1990.
N. Vasanthavada, R. Baker and N. Kanopoulos. A monolithic image edge detection filter. In Proc. IEEE Custom Integrated Circuits Conference, 1987.
H. Zhang, D. Kapur and M.S. Krishnamoorthy. A mechanizable induction principle for equational specifications. In Proc. 9th Intl. Conf. Automated Deduction (CADE), volume 310 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pages 250–265, 1988.
H. Zhang, Implementing contextual rewriting. Proc. Third International Workshop on Conditional Term Rewriting Systems, volume 665 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pages 363–377, 1992.
Rights and permissions
About this article
Cite this article
Kapur, D., Subramaniam, M. Mechanical Verification of Adder Circuits using Rewrite Rule Laboratory. Formal Methods in System Design 13, 127–158 (1998). https://doi.org/10.1023/A:1008610818519
Issue Date:
DOI: https://doi.org/10.1023/A:1008610818519