Stride: a tool for formal interactive system synthesis

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. Although it is essential to verify the correctness of the applied transformations, it is also very important to present the changes to the designer in an understandable form. A prototype interactive design tool has been implemented that allows easy use of a database of formally correct transformations. Its basic features are described, and its operation and interaction with the theorem prover are demonstrated with examples