Abstract
In this paper, we propose a technique for proving the correctness of the implementations of synchronous sequential circuits automatically, where the specifications of synchronous sequential circuits are described in an algebraic language ASL, which we have designed, and the specifications are described in a restricted style. For a given abstract level's specification, we refine the specification into a synchronous sequential circuit step by step in our framework, and prove the correctness of the refinement at each design step. Using our hardware design support system, to prove the correctness of a design step, we have only to give the system some invariant assertions and theorems for primitive functions. Once they are given, the system automatically generates the logical expressions from the invariant assertions and so on, whose truth guarantees the correctness of the design step, and tries to prove those truth using a decision procedure for the prenex normal form Presburger sentences bounded by only universal quantifiers. Using the system, we have proved the correctness of the implementation of a GCD circuit, the Tamarack microprocessor, a sorting circuit and so on, in a few days. The system has determined the truth of each logical expression within a minute.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
S. Bose and A. Fisher: “Automatic Verification of Synchronous Circuits Using Symbolic Logic Simulation and Temporal Logic”, Proc. IMEC-IFIP Int. Workshop on Applied Formal Methods for Correct VLSI Design, pp.759–764, 1989.
M. Browne, E. M. Clarke, D. Dill and B. Mishra: “Automatic Verification of Sequential Circuits using Temporal Logic”, IEEE Trans. on Computer, Vol. C-35, No. 12, pp. 1035–1044, 1986.
H. Busch: “Transformational Design in a Theorem Prover”, IFIP Conf. on Theorem Provers in Circuit Design, North-Holland, pp.175–196, 1992.
D.C. Cooper: “Theorem Proving in Arithmetic without Multiplication”, Machine Intelligence, No.7, pp. 91–99, 1972.
M. J. C. Gordon: “HOL: A Proof Generating System for Higher Order Logic”, in VLSI Specification, Verification and Synthesis, G. Birtwistle and P. A. Subrahmanyam ed-s., Kluwer Academic Publishers, pp.73–128, 1988.
T. Higashino and K. Taniguchi: “A System for the Refinements of Algebraic Specifications and their Efficient Executions”, Proc. of the IEEE 24-th Hawaii Int. Conf. on System Sciences (HICSS-24), Vol. II, pp. 186–195 (Jan. 1991).
J.E. Hopcroft and J.D. Ullman: “Introduction to Automata, Theory, Languages, and Computation”, Addison-Wesley, 1979.
IEEE: “IEEE Standard VHDL Language Reference Manual”, IEEE, 1988.
J. J. Joyce: “Formal Verification and Implementation of a Microprocessor”, VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, pp.129–157, 1988.
T. Kasami, K. Taniguchi, Y. Sugiyama and H. Seki: “Principles of Algebraic Language ASL/*”, Trans. of IECE Japan, Vol. 69-D, No.7, pp. 1066–1074, July 1986 (in Japanese).
J. Kitamiti, T. Higashino, K. Taniguchi and Y. Sugiyama: “Top-Down Design Method for Synchronous Sequential Logic Circuits Based on Algebraic Technique”, Trans. of IEICE Japan, Vol. 77-A, No.3, March 1994 (in Japanese).
T. Kropf: “Benchmark-Circuits for Hardware — Verification: v.1.0.0”, the Benchmark-Circuits for 2nd Conf. on Theorem Proving in Circuits Design, FTP from Univ. of Karlsruhe (129.13.18.22), Germany, 1994.
Y. Nakamura: “An Integrated Logic Design Environment Based on Behavioral Description”, IEEE Trans. on Computer-Aided Design Integrated Circuits & Systems, Vol. 6, No. 3, pp. 322–336, May 1987.
V. Stavridou, J. A. Goguen, A. Stevens, S. M. Eker, S. N. Aloneftis and K. M. Hobley: “FUNNEL and 2OBJ: Towards as Integrated Hardware Design Environment”, IFIP Conf. on Theorem Provers in Circuit Design, North-Holland, pp.197–223, 1992.
J.B. Saxe S.J. Garland, J.V. Guttag and J.J. Horning, “Using Transformations and Verification in Circuits Design”, Designing Correct Circuits, North-Holland, pp.1–25, 1992.
G. Thuau, B. Berkane, “Using the Language LUSTRE for Sequential Circuit Verification”, Designing Correct Circuits, North-Holland, pp. 81–96, 1992.
Open Verilog International: “Verilog Hardware Description Language Reference Manual”, 1991.
M. Wirsing: “Structured Algebraic Specifications: A Kernel Language”, Tech. Report, TU Mchen, 1984.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kitamichi, J., Morioka, S., Higashino, T., Taniguchi, K. (1995). Automatic correctness proof of the implementation of synchronous sequential circuits using an algebraic approach. In: Kumar, R., Kropf, T. (eds) Theorem Provers in Circuit Design. TPCD 1994. Lecture Notes in Computer Science, vol 901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59047-1_48
Download citation
DOI: https://doi.org/10.1007/3-540-59047-1_48
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59047-7
Online ISBN: 978-3-540-49177-4
eBook Packages: Springer Book Archive