|
The synthesis of digital circuits is a complex process involving
a large number of complex tools. Since these tools are large pieces of software and many developers are involved in their development, bugs may exist in the software. As a consequence, the designed circuits may not implement the specification. A possible alternative to the software verification problem is to use post-synthesis verification techniques , especially model checkers . However, their applicability is limited by the size and the nature of the designed circuits. For certain classes of circuits such as controllers it is practicable, but for general classes of circuits which involve large data and control parts, post-synthesis verification techniques fail. The main aim of the formal synthesis group is to develop a methodology where the verification process is closely knitted within the design process, thus obviating the need for post-synthesis verification and software verification of the synthesis tool. We view the Formal synthesis process as a derivation of the implementation by the application of transformations within a logical calculus. The end product is therefore not only the implementation but also the mathematical proof that the implementation satisfies the specification. Adhering to the paradigm, described above, we are developing a toolbox --- HASH (Higher-order logic Applied to Synthesis of Hardware) which offers a set of transformations for each synthesis step at different levels of abstraction. A distinguishing feature of HASH is the ability to integrate the vast amount of knowledge that exists in the non-formal, conventional synthesis domain.
|
