Browsing by Author "Birtwistle, G."
Now showing 1 - 11 of 11
Results Per Page
Sort Options
Item Open Access THE ARCHITECTURE OF HENDERSON'S SECD MACHINE(1989-01-01) Simpson, T.; Birtwistle, G.; Hermann, M.; Graham, B.We explain and document the architecture of an eager SECD machine devised by Henderson. A software interpreter for this architecture has been in use for two years and has been well tested. Expansion of the interpreter leads to the detailed specifications of an architecture in VLSI. Such an SECD chip has been layed out and fabricated.Item Open Access CASE STUDIES IN ASYNCHRONOUS DESIGN. PART I: AMM ARCHITECTURE PART II: A 4 STROKE AMM(1993-12-01) Birtwistle, G.; Spooner, D.; Liu, Y.; Yu, Wanzhen; Stevens, Ken; Aldwinckle, JohnPART I: There seems to be a real need for fully-worked, moderately-sized case studies in asynchronous design which show, explain, compare and contrast the various common design styles. In a series of reports we will describe, specify and implement a variant of Sutherland's MOVE machine in CCS in a number of popular design styles: "4-stroke", "2-stroke", and combined (control in 2-stroke, datapath in 4-stroke), without and then with pipelining. In each case we will show that our designs possess certain desirable properties (neither deadlocks nor livelocks, ...) and that they conform to their specifications. In this first document, we describe our variant of the MOVE machine together with some typical programs. PART II: This is an early draft of a tutorial document which seeks to explain the bread-and-butter design of simple micro. We specify and implement a simple 4 stroke variant of Sutherland's MOVE machine in CCS. We explain the 4 stroke design style, specify a sufficient library of cells, give a "bread and butter" implementation of AMM, and show that it conforms to its specification and possesses several desirable safety and liveness properties.Item Open Access CHARACTERISING THE STRUCTURE OF SIMULATION MODELS IN CCS(1993-10-01) Birtwistle, G.; Pooley, R.; Tofts, C.We describe how to apply the tools and techniques of process algebra to explore and verify the structure of simulation models. Process algebras are concise and precise object-oriented notations in which to express model structure and component interactions. We demonstrate how to specify the structure and basic synchronisations of simulation models using Milner's CCS (Calculus of Communicating Systems) notation, and how to test for the consequences of a specification using the modal $mu$-calculus (Stirling). In this way we open up the possibility of verifying from its static model description that a simulation model has certain basic desirable properties (is deadlock and livelock free and has appropriate safety, liveness and fairness characteristics (Manna and Pnueli)). Thus adopting these techniques from process algebra both makes models more reliable and saves a considerable amount of debugging time.Item Open Access A COMPILER FOR LISPKIT TARGETTED ATHENDERSON'S SECD MACHINE(1989-01-01) Simpson, T.; Birtwistle, G.; Hermann, M.; Graham, B.Long term research plans at Calgary are focussed on system verification. We have been working on hardware verification for some time, and this work will culminate in the verification of an SECD chip in 1989. The chip has been fabricated. We describe a compiler and its associated workbench, written in Franz Lisp, which takes Lispkit source code for Henderson's SECD machine. The compiler has been in operation for two years and has been well tested but not verified.Item Open Access JADE status report: a local computing network for research in distributed programming environments(1986-01-01) Unger, Brian W; Birtwistle, G.; Cleary, J.; Hill, D.; Keenan, T.; Rokne, J.; Kendall, J.; Vollmerhaus, W.; Witten, I.; Wyvill, B.No abstractItem Open Access THE MOSSIM SPECIFICATION OF THE SECD DESIGN(1989-06-01) Birtwistle, G.; Joyce, J.This report gives a complete switch level description of an SECD chip. The notation used is CDL (Circuit Description Language), which is a high level interface to a switch level simulator called Mossim. We give this full documentation in the hope that it can be used as a testbed by others interested in such issues as design for test and formal verification.Item Open Access THE SECD MACHINE ON A CHIP(1989-06-01) Birtwistle, G.; Graham, B.; Joyce, J.; Williams, S.; Brinsmead, M.; Keefe, M.; Kroeker, W.; Liblong, B.; Vollmerhaus, W.We describe work completed on the design, informal specification, and layout of a custom SECD machine. The chip contains around 25,000 transistors excluding memory cells. The work is part of a long term project which aims to support specification based VLSI design, build a library of cell and sub-system specifications, and investigate algorithms for transforming from specifications to other views.Item Metadata only Simulation Environments(1983-11-01) Birtwistle, G.; Cleary, J.; Liblong, B.; Unger, Brian W; Witten, I.No AbstractItem Open Access SOME STEPS TOWARDS A VERIFIED SYSTEM(1992-02-01) Birtwistle, G.; Simpson, Todd; Graham, BrianA totally verified system consists of a meaning preserving compiler and hardware which correctly interprets the resulting machine code. This paper describes work in progress towards this goal using MiniSML, a small functional language, and the SECD machine. A functional language is used to ease software proofs, and the SECD machine was chosen as it was the best documented machine when we began this work. This paper outlines a (hand) proof of the correctness of a translator from MiniSML to SECD machine code and a mechanized HOL proof of the hardware which realizes the abstract SECD machine. To achieve a totally verified system, further work is required to mechanize the translator proof and tie it directly to the machine proof, and to recognize the constraints of the machine (i.e., memory capacity) at the software level.Item Open Access SPECIFYING A GRAPHICS PACKAGE: A CASE STUDY WITH Z(1992-02-01) Birtwistle, G.; Zhang, H.We report on the specification of a subset of graphics package called Polygon Groper. We used \o'\fIZ\(ap'\fR and its associated specification schema methodology to specify the datastructures of Polygon Groper, the set of primitive functions over these data structures, and the set of commands that compose functions over these datastructures. Working strictly from these specifications, we have located and corrected several serious errors in Polygon Groper. The techniques are straightforward and may be applied to any system.Item Open Access VERIFYING SECD IN HOL(1991-01-01) Graham, B.; Birtwistle, G.This paper describes some of the work done at Calgary on the design of an SECD chip and its verification using the Cambridge HOL proof assistant. The chip is a physical realization of Henderson's variant of Landin's abstract architecture to execute the lambda calculus. The machine uses closures and includes explicit machine instructions to assist recursion. The complete proof, which goes from an abstract specification down to the transistor level, is far too involved to be covered in a single paper. In this paper, we discuss the SECD architecture and design and trace through a portion of the proof of correctness of one sequence of the microcode.