Browsing by Author "Graham, Brian"
Now showing 1 - 6 of 6
Results Per Page
Sort Options
Item Open Access DEALING WITH THE CHOICE OPERATOR IN HOL88(1990-04-01) Graham, BrianThis paper discusses the choice operator @ in HOL88. It gives an intuitive interpretation, as well as the definition, and presents proof strategies for goals that contain this operator, broken down into cases based on the number of values which satisfy the predicate argument. A working knowledge of the HOL system is assumed.Item Open Access FORMAL SPECIFICATION OF THE SECD CHIP TOP AND REGISTER TRANSFER LEVELS(1989-10-01) Graham, BrianThis report compiles the formal HOL definitions at the top and register transfer levels of the SECD Chip. Three sections cover abstract data types, component and specification definitions, and proofs of correctness of several segments.Item Open Access HARDWARE VERIFICATION BY FORMAL PROOF(1988-10-01) Birtwistle, Graham; Graham, Brian; Melham, Tom; Schediwy, RichHardware 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.Item Open Access OPERATING SPECIFICATION FOR THE SECD CHIP(1989-06-01) Graham, Brian; Williams, Simon; Stone, GlenThis paper gives an operating specification for the SECD chip, which implements Landin's abstract SECD architecture. It is intended to serve as a guide for the design of a chip controller, and includes details of packaging, memory, operating protocols, and guidelines for testing.Item Open Access SECD: DESIGN ISSUES(1989-09-01) Graham, BrianThis paper describes the levels at which the designers found it useful to view the SECD design, and the design issues at each level. The interplay between formal specification and abstraction mechanisms used between views at different levels is described.Item 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.