## 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