Specification of control flow properties for verification of synthesized VHDL designs

Behavioral specifications in VHDL contain multiple communicating processes. Register level designs synthesized from these specifications contain a data path represented as a netlist and a controller consisting of multiple communicating synchronous finite state machines. These finite state machines together implement the control flow specified in and implied by the behavioral specification in VHDL. This paper describes a systematic approach to identifying the control flow properties critical to the proper functioning of designs synthesized from VHDL. These properties are then formulated as specifications in Computational Tree Logic (CTL) while presenting a controller model for high-level synthesis. These specifications form a necessary set that must be satisfied by any correct synthesized design. A high-level synthesis system, as a byproduct of creating RTL designs, can automatically generate these CTL specifications.