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.
We are currently acquiring citations for the work deposited into this collection. We recognize the distribution rights of this item may have been assigned to another entity, other than the author(s) of the work.If you can provide the citation for this work or you think you own the distribution rights to this work please contact the Institutional Repository Administrator at firstname.lastname@example.org