Proof and synthesis

The authors argue that the next generation of computer-aided design (CAD) tools will represent and manipulate behavior. Behavioral tools are necessary to provide fast reliable design of complex systems. An approach to high-level synthesis is described which has grown out of formal verification using mathematical logic. It is shown that a general-purpose proof strategy combined with simple design rules can be used to represent and automate a simple design strategy. It is noted that the example shown here is clearly trivial. It is concluded that developing a reasonably comprehensive library of proof strategies and of representational abstractions is necessary to produce a useful tool