Extending VLSI design with higher-order logic

Extending VLSI CAD with higher-order logic integrates formal verification with synthesis. The benefits of doing so are: 1) relating instruction-set descriptions to implementations, 2) designing at a higher level of abstraction than at the level of schematics, 3) verifying by proof, 4) reusing verified parameterized designs, 5) automatically compiling designs in higher-order logic to parameterized cell generators and layouts, and 6) validating electrical and functional properties by simulation. Such an integration is demonstrated by linking the Cambridge Higher-Order Logic (HOL) theorem-prover with the Mentor Graphics GDT design environment. We illustrate its application by creating a parameterized macro-cell generator for an n-bit Am2910 microprogram sequencer, whose design is formally verified with respect to its instruction-set architecture specification.