Simulation-based verification for high-level synthesis

The verification problem is described, and a way to verify a high-level synthesis system automatically is presented. The system, called Satya, maps an algorithmic description to a logic circuit description and compares descriptions to detect semantic errors and identify the cause of those errors. Satya has been used to verify the Bridge synthesis system, which accepts a subset of C as input, but the simulation-based approach underlying Satya is suitable for verifying synthesis systems that use other high-level languages, such as VHDL. The verification results are discussed, and some of the problems that arise in debugging and regression testing are considered.<>