A.M. Koelmans
F.P. Burns
D.J. Kinniment
University of Newcastle upon Tyne. 1993
Transformational synthesis is the process of generating a hardware implementation from an initial behavioural description, by repeatedly applying transformations to the behavioural descriptions until a satisfactory implementation can be generated. It is essential to verify the correctness of the applied transformations if the final implementation is to conform to the initial specification. We have implemented a prototype interactive design tool that integrates the Boyer Moore theorem prover into the design process. We describe the reasons for using this particular theorem prover, its basic features, and demonstrate the operation of the design tool and its interaction with the theorem prover with an example.