Abstract
We show how hardware implementation descriptions written in Higher Order Logic (HOL) are transformed into VLSI layouts. The intent is to link formally verified designs to physical implementations. Once HOL structural descriptions are transformed to structural descriptions and parameterized cell generators in a VLSI CAD system, the tools associated with the VLSI CAD system can be used such as standard cell libraries, automatic placement and routing, and simulation. The cell generator programs derived from verified HOL descriptions provide a means by which verified and parameterized HOL designs can augment a cell library within a CAD system. The particular VLSI CAD system used here is the GDT system from Mentor Graphics. The GDT system includes a CMOS standard cell library, a macrocell synthesis tool which includes automatic placement and routing, and the Lsim multilevel simulator. GDT uses a structural language called L. HOL structural descriptions are first mapped to L, then layouts corresponding to the L descriptions are created using the standard cell library and the layout generation tools. We illustrate this design process by creating the layout for an 8-bit serial/parallel multiplier which has been verified in HOL.
Supported by NY State Center for Advanced Technology at Syracuse University.
Preview
Unable to display preview. Download preview PDF.
References
Mike Gordon, “A proof Generating System for Higher-Order Logic,” in VLSI Specification, Verification and Synthesis, edited by Graham Birtwistle and P.A. Subrahmanyam, Kluwer, 1987.
Mike Gordon, “Why higher-order logic is a good formalism for specifying and verifying hardware,” Formal Aspects of VLSI Design, edited by G. Milne and P.A. Subrahmanyam, North Holland, 1986.
Shiu-Kai Chin and Edward P. Stabler, “Synthesis of Arithmetic Hardware Using Hardware Metafunctions,” IEEE Trans. Computer-Aided Design, Vol. 9, No. 8, August 1990.
Shiu-Kai Chin and Juin-Yeu Lu, The Mechanical Verification and Synthesis of Parameterized Serial/Parallel Multiplier, CASE Center Tech. Report No. 9140, Syracuse University, March 1991.
Shiu-Kai Chin and Graham Birtwistle, “Implementing and Verifying Finite-State Machines Using Types in Higher-Order-Logic,” Proc. 1991 Int. Tutorial Workshop on the HOL Theorem Proving System and its Applications, IEEE Comp. Soc. Press, 1992.
Juin-Yeu Lu and Shiu-Kai Chin, Linking HOL to a VLSI CAD System, CASE Center Tech. Report, Syracuse University, April 1993.
Albert John Camilleri, Executing Behavioural Definitions in Higher Order Logic, Tech. Report No. 140, University of Cambridge Computer Lab., Feb. 1988.
A. J. Cohn, “A Proof of Correctness of the VIPER Microprocessor: The First Level,” in VLSI Specification, Verification and Synthesis, edited by Graham Birtwistle and P.A. Subrahmanyam, Kluwer, 1988.
J. Joyce, “Formal Verification and Implementation of a Microprocessor,” in VLSI Specification, Verification and Synthesis, edited by Graham Birtwistle and P.A. Subrahmanyam, Kluwer, 1988.
Thomas F. Melham, Automating Recursive Type Definitions in Higher Order Logic, Tech. Report No. 146, University of Cambridge Computer Lab., Jan. 1989.
Mandayam Srivas, Mark Bickford, “Formal Verification of a Pipelined Microprocessor,” IEEE Software, Sep. 1990.
Mentor Graphics Corporation, GDT Manuals V.5, CA, 1990.
Xilinx Inc., The Programmable Gate Array Data Bool, CA, 1989.
Thomas Kropf, Ramayya Kumar, Klaus Schneider, “Embedding Hardware Verification within a Commercial Design Framework,” Advanced Research Working Conference on Correct Hardware Design Methodologies (CHARME93), Lecture Notes in Computer Science, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lu, JY., Chin, SK. (1994). Linking Higher Order Logic to a VLSI CAD system. In: Joyce, J.J., Seger, CJ.H. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1993. Lecture Notes in Computer Science, vol 780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57826-9_136
Download citation
DOI: https://doi.org/10.1007/3-540-57826-9_136
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57826-0
Online ISBN: 978-3-540-48346-5
eBook Packages: Springer Book Archive