Advertisement

Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem Prover

  • Deepak Kapur
  • M. Subramaniam
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1538)

Abstract

Finite tables are commonly used in many hardware and software applications. In most theorem provers, tables are typically axiomatized using predicates over the table indices. For proving conjectures expressed using such tables, provers often have to resort to brute force case analysis, usually based on indices of a table. Resulting proofs can be unnecessarily complicated and lengthy. They are often inefficient to generate as well as difficult to understand. Large tables are often manually abstracted using predicates, which is error-prone; furthermore, the correctness of abstractions must be ensured. An approach for modeling finite tables as a special data structure is proposed for use in Rewrite Rule Laboratory (RRL), a theorem prover for mechanizing equational reasoning and induction based on rewrite techniques. Dontcare entries in tables can be handled explicitly. This approach allows tables to be handled directly without having to resort to any abstraction mechanism. For efficiently processing large tables, concepts of a sparse and weakly sparse tables are introduced based on how frequently particular values appear as table entries. Sparsity in the tables is exploited in correctness proofs by doing case analyses on the table entries rather on the indices. The generated cases are used to deduce constraints on the table indices. Additional domain information about table indices can then be used to further simplify constraints on indices and check them. The methodology is illustrated using a nontrivial correctness proof of the hardware SRT division circuit performed in RRL. 1536 cases originally needed in the correctness proof are reduced to 12 top level cases by using the proposed approach. Each individual top level case generated is much simpler, even though it may have additional subcases. The proposed approach is likely to provide similar gains for applications such as hardware circuits for square root and other arithmetic functions, in which much larger and multiple lookup tables, having structure similar to the sparse structure of the SRT table, are used

Keywords

Case Analysis Lookup Table Table Index Table Entry Correctness Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    E.M. Clarke, S.M. German and X. Zhao, “Verifying the SRT division algorithm using theorem proving techniques,” Proc. Computer Aided Verification, 8th Intl. Conf. Brunswick, August 1996, Springer LNCS 1102, 111–122.Google Scholar
  2. 2.
    Proc. of the IEEE International Symposium on Computer Arithmetic,, IEEE Computer Society 1995.Google Scholar
  3. 3.
    Proc. of the IEEE International Symposium on Computer Arithmetic,, IEEE Computer Society 1997.Google Scholar
  4. 4.
    M.P. Heimdahl and N. Leveson, “Consistency and completeness analyses of state-based requirements,” 17th Intl. Conf. on Software Eng., IEEE, 1995.Google Scholar
  5. 5.
    C. Heitmeyer, A. Bull, C. Gasarch, B. Labaw, “SCR*: A toolset for specifying and analyzing requirements,” In Proc. of COMPASS’95, IEEE 1995.Google Scholar
  6. 6.
    D.N. Hoover and Z. Chen, “Tablewise, a decision table tool”, In Proc. of COMPASS’95, IEEE 1995.Google Scholar
  7. 7.
    P.S. Miner and J.F. Leathrum Jr., “Verification of IEEE compliant subtractive division algorithm,” Proc. FMCAD’96, LNCS 1166, Palo Alto, CA, 1996.Google Scholar
  8. 8.
    D. Kapur, “Rewriting, decision procedures and lemma speculation for automated hardware verification,” Proc. 10th Intl. Conf. Theorem Proving in Higher Order Logics, LNCS 1275, 1997.CrossRefGoogle Scholar
  9. 9.
    D. Kapur and X. Nie, “Reasoning about numbers in Tecton,” Proc. 8th Intl. Symp. Methodologies for Intelligent Systems, (ISMIS’94), October 1994.Google Scholar
  10. 10.
    D. Kapur, M. Subramaniam “Mechanizing Reasoning About Arithmetic Circuits: SRT Division,” In Proc. of 17th FSTTCS, LNCS (eds. Sivakumar and Ramesh), 1997.Google Scholar
  11. 11.
    A.R. Omondi, Computer Arithmetic Systems: Algorithms, Architecture and Imple-mentations, Prentice Hall 1994.Google Scholar
  12. 12.
    K.D. Tocher, “Techniques of multiplication and division for automatic binary com-puters,” Quarterly Journal of Mechanics and Applied Mathematics, 11(3), 1958.Google Scholar
  13. 13.
    G.S. Taylor, “Compatible hardware for division and square root,” Proc. 5th IEEE Symp. on Computer Architecture, May 1981.Google Scholar
  14. 14.
    S. Owre, J.R. Rushby, N. Shankar, “Integration in PVS: Tables, Types, and Model Checking,” Proc. of TACAS,, LNCS 1217, Springer Verlag, April 1997.Google Scholar
  15. 15.
    M.D. Ercegovac, T. Lang, “Radix-4 Square Root Without Initial PLA,” IEEE Trans. on Computers, Vol. 39. No. 8, Aug. 1990.Google Scholar
  16. 16.
    J.H. Zurawski, J.B. Gosling, “Design of a high speed square root multiply and divide unit”, IEEE Trans. on Computers, vol. C-36, 1987.Google Scholar
  17. 17.
    D.D. Sarma and D. Matula, “Measuring the Accuracy of ROM Reciprocal Tables”, IEEE Int. Symp. on Comput. Arithmetic, IEEE Computer Society, 1993.Google Scholar
  18. 18.
    H. Ruess, N. Shankar and M.K. Srivas, “Modular verification of SRT division,” Proc. Computer Aided Verification, 8th Intl. Conf.-CAV’96, New Brunswick, 1996, Springer LNCS 1102 (eds. Alur and Henzinger).Google Scholar
  19. 19.
    J.E. Robertson, “A new class of digital division methods,” IRE Trans. on Electronic Computers, 1958, 218–222.Google Scholar
  20. 20.
    H. Zhang, D. Kapur, and M.S. Krishnamoorthy, “dA mechanizable induction principle for equational specifications,” Proc. 9th (CADE), Springer LNCS 310, 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Deepak Kapur
    • 1
  • M. Subramaniam
    • 1
  1. 1.Computer Science DepartmentState University of New YorkAlbany

Personalised recommendations