The use of formal methods in VLSI design is currently a very active research area. This requires the specification of the behaviour of a hardware design in a formal, mathematically rigorous manner. Such specifications can subsequently be manipulated by proof systems (usually called 'proof assistants' or 'theorem provers') to prove the equivalence of hierarchical or temporal properties of hardware designs. We describe a prototype tool which integrates a theorem prover into the design environment in such a way as to ensure functional and trans formational correctness at all times. The system is driven from a hardware description language developed at Newcastle called STRICT, and it is interactive. Our aim in developing this tool is to make it easier for the designer to ensure correctness of the final implementation, without losing the benefit of his skill and experience.

Inspec keywords: VLSI; integrated circuit design; hardware description languages; formal specification

Other keywords: formal methods; STRICT; transformational synthesis; proof assistants; hardware designs; prototype tool; hardware description language; theorem provers; VLSI design

Subjects: Semiconductor integrated circuit design, layout, modelling and testing