Skip to main content
SpringerLink
Log in

Linking Higher Order Logic to a VLSI CAD system

  • Conference paper
  • First Online:
Book cover Higher Order Logic Theorem Proving and Its Applications (HUG 1993)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 780))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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.

    Google Scholar 

  2. 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.

    Google Scholar 

  3. 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.

    Google Scholar 

  4. 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.

    Google Scholar 

  5. 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.

    Google Scholar 

  6. Juin-Yeu Lu and Shiu-Kai Chin, Linking HOL to a VLSI CAD System, CASE Center Tech. Report, Syracuse University, April 1993.

    Google Scholar 

  7. Albert John Camilleri, Executing Behavioural Definitions in Higher Order Logic, Tech. Report No. 140, University of Cambridge Computer Lab., Feb. 1988.

    Google Scholar 

  8. 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.

    Google Scholar 

  9. 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.

    Google Scholar 

  10. Thomas F. Melham, Automating Recursive Type Definitions in Higher Order Logic, Tech. Report No. 146, University of Cambridge Computer Lab., Jan. 1989.

    Google Scholar 

  11. Mandayam Srivas, Mark Bickford, “Formal Verification of a Pipelined Microprocessor,” IEEE Software, Sep. 1990.

    Google Scholar 

  12. Mentor Graphics Corporation, GDT Manuals V.5, CA, 1990.

    Google Scholar 

  13. Xilinx Inc., The Programmable Gate Array Data Bool, CA, 1989.

    Google Scholar 

  14. 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.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Electrical & Computer Engineering, Syracuse University, Syracuse, NY

    Juin-Yeu Lu & Shiu-Kai Chin

Authors
  1. Juin-Yeu Lu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shiu-Kai Chin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jeffrey J. Joyce Carl-Johan H. Seger

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation