SPECIFICATION AND VLSI DESIGN

Abstract

We describe research into specification-based VLSI design underway at the University of Calgary. Our long term research goals are directed towards building a specification-based design environment (EDICT) to support an iterative, hierarchic design methodology. Our current research has three aspects: the SHIFT high level design capture format (completed); gaining experience in verifying large designs (underway); and building a specification library. In this paper we describe work in progress on two large proofs. The first is for the elimination unit of a local area network device, for which the proof is well underway. The second project concerns the specification driven design of Landin's SECD machine and is just beginning. To set the context for this work on verification, we start by giving partial descriptions of EDICT and SHIFT to show how they use specifications.