Verification of RTL generated from scheduled behavior in a high-level synthesis flow

We propose a complete procedure for verifying register-transfer logic against its scheduled behavior in a high-level synthesis environment. Our proposal advances the state of the art because it is the first such verification procedure that is both complete and practical. Hardware verification is known to be a hard problem and the proposed verification technique leverages off the fact that high-level synthesis - performed manually or by means of high-level synthesis software - proceeds from the algorithmic description of the design to structural RTL through a sequence of very well defined steps, each limited in its scope. The major contribution is the partitioning of the equivalence checking task into two simpler subtasks, verifying the validity of register sharing, and verifying correct synthesis of the RTL interconnect and control. While state space traversal is unavoidable for verifying validity of the register sharing, we automatically abstract out irrelevant portions of the design, significantly simplifying the task that must be performed by a back-end model checker. The second task of verifying the RTL is not only shown to reduce to a combinational equivalence check, we present a novel and fast RTL technique for combinational equivalence check instead of using slower gate level techniques. The verification procedure has been applied to several large circuits, and is illustrated on the implementation of a sort algorithm.