Symbolic Verification of Sequential Circuits Synthesized with CALLAS

We present a solution to the verification problem of high-level synthesis. The high-level synthesis system CALLAS takes as input an algorithmic specification, in VHDL, and produces as output an EDIF netlist. Both, the specification and the generated netlist can be interpreted as finite state machine descriptions. Then, in this context, the verification problem is reduced to proving the behavioral equivalence of both machines. For this equivalence proof we use the symbolic verifier of the CVE System (CVE = Circuit Verification Environment). Recent improvements of the verifier allowed equivalence proofs of machines with up to 260 binary state variables