n South African Computer Journal - Generating and model checking a hierarchy of abstract models : research article

Volume 2004, Issue 32
  • ISSN : 1015-7999
  • E-ISSN: 2313-7835



The use of automatic model checking algorithms to verify detailed gate or switch level designs of circuits is very attractive because the method is automatic and such models can accurately capture detailed functional, timing, and even subtle electrical behaviour of circuits. The use of binary decision diagrams has extended by orders of magnitude the size of circuits that can be so verified, but there are still very significant limitations due to the computational complexity of the problem. Verifying abstract versions of the model is attractive to reduce computational costs but this poses the problem of how to build abstractions easily without losing the accuracy of the low-level model. <br>This paper proposes a method of bridging the gap between detailed designs and abstract models, and presents preliminary theoretical and experimental results. Starting with a detailed, low-level model of a circuit (which uses BDDs for representing data), the human verifier picks a set of properties that s/he believes characterises the circuit. These properties are automatically verified by a model checking algorithm. Once proved, these properties are used to synthesise automatically an abstract model of the circuit, which can use symbolic representation of data. An automatic model checking algorithm can then be applied to the abstract model to verify more properties of the circuit. The preliminary results, although limited, were promising: the abstraction could be constructed and verified with relatively modest cost, thereby reducing the human cost of verification significantly.

Loading full text...

Full text loading...


Article metrics loading...


This is a required field
Please enter a valid email address
Approval was a Success
Invalid data
An Error Occurred
Approval was partially successful, following selected items could not be processed due to error