Abstract
This chapter reports on experiences in verifying synchronous circuit designs using the ReDuX term rewriting laboratory (Bündgen, 1993; Bündgen et al., 1996c; Bündgen and Lauterbach, 1996a). For this purpose a technique is presented that transforms the proof requirements for the verification of a processor design at gate level to purely equational problems. This technique has been successfully applied to the verification of two processors of the Sparrow family.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berkeley: 1992, `Berkeley Logic Interchange Format (BLIF)’. University of California, Berkeley, CA.
Berregeb, N., A. Bouhoula, and M. Rusinowitch: 1996, `Automated Verification by Induction with Associative-Commutative Operators’. In: R. Alur and T. A. Hen-zinger (eds.): Computer Aided Verification (LNCS 1102). pp. 220–231, Springer-Verlag. (Proc. CAV’96, New Brunswick, NJ, USA, July/August 1996 ).
Bubeck, T., U. Kebschull, and W. Rosenstiel: 1993, `— Sparrow — Ein Mikroprozessor-Entwurfs-und Ausbildungssystem’. Technical Report 93–07, WilhelmSchickard-Institut, Universität Tübingen, D-72076 Tübingen. (in German).
Bündgen, R.: 1993, `Reduce the Redex ReDuX’. In: C. Kirchner (ed.): Rewriting Techniques and Applications (LNCS 690). pp. 446–450, Springer-Verlag. (Proc. RTA’93, Montreal, Canada, June 1993 ).
Blindgen, R., M. Göbel, and W. Küchlin: 1996a, `Strategy Compliant Multi-Threaded Term Completion’. Journal of Symbolic Computation 21 (4–6), 475–505.
Blindgen, R., W. Küchlin, and W. Lauterbach: 1996b, `Verification of the Sparrow Processor’. In: IEEE Symposium and Workshop on Engineering of Computer-Based Systems. IEEE Press, pp. 86–93. (Proc. ECBS’96, Friedrichshafen, Germany, March 1996 ).
Bündgen, R. and W. Lauterbach: 1996a, `Combining Reductions and Computations in ReDuX’. In: M. Wirsing and M. Nivat (eds.): Algebraic Methodology and Software Technology (LNCS 1101). pp. 633–636, Springer Verlag. (Proc. AMAST’96, Munich, Germany, July 1996 ).
Bündgen, R. and W Lauterbach: 1996b, `Experiments with Partial Evaluation Domains for Rewrite Specifications’. In: M. Haveraaen, O. Owe, and 0.-J. Dahl (eds.): Recent Trends in Data Type Specifications (LNCS 1130). pp. 125–142, Springer Verlag. (WADT’95, Oslo, Norway, September 1995, selected papers).
Bündgen, R., W. Lauterbach, and W. Küchlin: 1995, `A License to Fly: Verifying the Sparrow-0 Processor’. Technical Report 95–04, Wilhelm-Schickard-Institut, Universität Tübingen, D-72076 Tübingen.
Bündgen, R., C. Sinz, and J. Walter: 1996c, `ReDuX 1.5: New Facets of Rewriting’. In: H. Ganzinger (ed.): Rewriting Techniques and Applications (LNCS 1103). pp. 412–415, Springer-Verlag. (Proc. RTA’96, New Brunswick, NJ, USA, July 1996 ).
Chandrasekhar, M. S., J. P. Privitera, and C. K. W.: 1987, `Application of Term Rewriting Techniques to Hardware Verification’. In: 24th ACM/IEEE Design Automation Conference. pp. 277–282.
Geser, A. and W. Küchlin: 1997, `Structured Formal Verification of a Fragment of the IBM 390 Clock Chip’. In: Technical Report 97–50, RISC Linz Report Series.
Goguen, J. A., T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud: 1993, `Introducing OBJ’.
Hsiang, J.: 1985, `Refutational Theorem Proving using Term-Rewriting Systems’. Artificial Intelligence 25, 255–300.
Hunt, Jr, W. A.: 1989, `Microprocessor Design Verification’. Journal of Automated Reasoning 5 (4), 429–460.
Kapur, D. and M. Subramaniam: 1996, `Mechanically Verifying a Family of Multiplier Circuits’. In: R. Alur and T. A. Henzinger (eds.): Computer Aided Verification (LNCS 1102). pp. 135–146, Springer-Verlag. (Proc. CAV’96, New Brunswick, NJ, USA, July/August 1996 ).
Kebschull, U., E. Schubert, and W. Rosenstiel: 1992, `Multilevel Logic Synthesis Based on Functional Decision Diagrams’. In: Proc. EDAC 1992.
Martin, U. and T. Nipkow: 1988, `Unification in Boolean Rings’. Journal of Automated Reasoning 4, 381–396.
Narendran, P. and J. Stillman: 1989, `Formal Verification of the Sobel Image Processing Chip’. In: G. Birtwistle and P. A. Subrahmanyam (eds.): Current Trends in Hardware Verification and Automated Theorem Proving. New York, NY: Springer-Verlag, pp. 92–127.
Rosenstiel, W. and E. Schubert: 1995, ‘Praktikum VLSI-Design mit VHDL, WS 95/96’. Course notes for the VLSI desing laboratoy at the University of Tübingen (in German).
Sekar, R. C. and M. K. Srivas: 1989, `Formal Verification of a Microprocessor Using Equational Techniques’. In: G. Birtwistle and P. A. Subrahmanyam (eds.): Current Trends in Hardware Verification and Automated Theorem Provin. New York, NY: Springer-Verlag, pp. 171–217.
Staunstrup, J., S. J. Garland, and J. V. Guttag: 1992, `Mechanized Verification of Cir-cuit Descriptions using the Larch Prover’. In: V. Stavridou, T. F Melham, and R. T. Boute (eds.): Theorem Provers in Circuit Design. pp. 277–299, North-Holland.
Stone, M. H.: 1936, `The Theory of Representations of Boolean Algebras’. Trans. American Math. Society 40, 37–111.
Thole, P., U. Kebschull, E. Schubert, and W. Rosenstiel: 1993, `The design and implementation of an educational computer system based on FPGAs’. In: Proc. 4th Eurochip Workshop on VLSI Design Training.
XILINX- 1991, `XILINX The Programmable Gate Array Data Book’. XILINX Inc., 2100 Logic Drive, San Jose, CA 95124.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Bündgen, R. (1998). Rewrite Based Hardware Verification with Redux. In: Bibel, W., Schmitt, P.H. (eds) Automated Deduction — A Basis for Applications. Applied Logic Series, vol 10. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0437-3_12
Download citation
DOI: https://doi.org/10.1007/978-94-017-0437-3_12
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5052-6
Online ISBN: 978-94-017-0437-3
eBook Packages: Springer Book Archive