by Keith Hanna, University of Kent
This talk described an approach based on the use of ``dependent'' types in a higher-order logic, to capturing within a formal theory, the relation between a circuit and its behaviour. Circuits are treated as graphs and their behavioural specifications are treated as predicates. The key difficulty that has to be overcome is that, in a structural description, the types of the ports have to be treated as values whereas in an associated behavioural description, they appear as types. In a dependently typed language, this poses no difficulty and indeed it is possible to devise a sufficiently fine type for an interface that guarantees the consistency of a its structural and behavioural descriptions. The approach was implemented within the Veritas design logic. As expected, type-checking posed a difficult task, but it was found that it could be largely automated in the proof assistant by devising specialised tactics.