Proof and Design

Michael P. Fourman

Abstract: We describe a formalisation of the design process, based on the use of predicate logic to model system behaviour. In our formalisation, derived rules of predicate logic are used to represent the design state, design steps are represented as proof steps, and a goal-directed proof-assistant is used as the basis for behavioural design tools.

We introduce the relational model, and discuss its relationship to more operational models. In particular, we show that it is sound (relative to these operational models) for circuits that obey common design rules. We show how derived rules in a sequent calculus may be used to represent the relationship between a partial design, the original specification, and a specification of the tasks remaining to complete the implementation. We show how the relational hardware model can be used to express and relate hardware descriptions at different levels of abstraction. We describe a formal framework for top-down design based on this formulation of refinement. Finally, we give an example of the application of these methods, developed using Abstract Hardware Limited's LAMBDA design system.

LFCS report ECS-LFCS-95-319, February 1995.

This report is available in the following formats:

Previous | Index | Next