Use of a theorem prover for transformational synthesis
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.
Use of a theorem prover for transformational synthesis, Page 1 of 2
< Previous page Next page > /docserver/preview/fulltext/books/cs/pbcs004e/PBCS004E_ch2-1.gif /docserver/preview/fulltext/books/cs/pbcs004e/PBCS004E_ch2-2.gif