next up previous contents
Next: Scientific Output from Up: Scientific Output from Previous: Scientific Output from

Relevant Papers

[Hanna 94]
F K Hanna, Reasoning about real circuits, Proceedings International Conference on Higher-Order Logic and its Applications, Malta, 1994.

The main thrust of NADA research at Kent has been on exploring ways of describing structures (for example, circuit diagrams) and their relations to behaviours. Structures are characterised by sets of nodes, sets of components and an incidence relation. The description is expressed in terms of dependently-typed higher-order logic. From this description, and working within the same logic, a predicate defining the behaviour may be extracted. The use of a dependently-typed logic is particularly beneficial since it allows types to occur both as values (in structural descriptions) and as types (in behavioural descriptions). This work was presented as a paper at the 1994 EUROFORM working group in Marseille.

Work has also been undertaken in developing a methodology for describing and reasoning about digital circuits at the analogue level. This allows formal methods to be satisfactorily applied to varieties of circuit design logic, such as pass transistor logic, which are widely used in practice but are presently beyond the reach of formal methods. This work benefited from liason within the MHDL (Microwave Hardware Design Language) working group, which also addresses the task of formally describing analogue systems.



Bernhard Moeller
Fri May 12 14:21:20 MET DST 1995