Browsing by Author "Melham, Tom"

Now showing 1 - 4 of 4
  • No Thumbnail Available
    ItemMetadata only
    EDICT: AN ENVIRONMENT FOR DESIGN USING INTEGRATED CIRCUIT TOOLS
    (1984-06-01) Birtwistle, Graham; Hill, David; Kendall, John; Coates, Bill; Esau, Richard; Kroeker, Wallace; Liblong, Breen; Liu, Erwin; Melham, Tom; Schediwy, Rick
    We shall conduct research into the design, construction, and applications of a VLSI design environment called EDICT which controls complexity by imposing an iterative structured design methodology, using hierarchies, regularity, and reusable building blocks, and incorporates the different design rules and fabrication processes of most foundries.
  • Thumbnail Image
    ItemOpen Access
    HARDWARE VERIFICATION BY FORMAL PROOF
    (1988-10-01) Birtwistle, Graham; Graham, Brian; Melham, Tom; Schediwy, Rich
    Hardware verification is the art of proving formally that, to within the tolerance of an underlying model, a design meets (or perhaps does not meet) its specification. This paper is an introduction to hardware verification and its limitations. We illustrate the technique by specifying and verifying an $x$ or gate and a ripple carry sub-system using the HOL notation, (see [2,8,9]), and then demonstrate its capabilities with sample applications to VLSI CAD and system re-implementation.
  • Thumbnail Image
    ItemOpen Access
    SPECIFICATION AND VLSI DESIGN
    (1985-11-01) Birtwistle, Graham; Joyce, Jeff; Liblong, Breen; Melham, Tom; Schediwy, Rick
    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.
  • No Thumbnail Available
    ItemMetadata only
    TOWARDS A VLSI DESIGN TOOL SYSTEM
    (1984-11-01) Liblong, Breen; Melham, Tom; Birtwistle, Graham; Kendall, John
    This paper outlines a proposal for VLSI design tools at Calgary. The system will allow a designer to specify the behaviour of a circuit and to generate verified designs. The central element in the environment is a very high level intermediate form which guarantees consistency throughout the design cycle. The VLSI tools will be built on top of the JADE distributed prototyping environment which is also under development at the University of Calgary.