Equivalence checking: a rule-based approach

A well-known problem in the design of embedded systems is checking for equivalence of two systems, and the traditional approach constructs and proves equivalence of finite state models of the two systems. Although widely and successfully used, the main problem is state space explosion, and other forms of higher-level analysis are also needed typically. Many typical system level design/synthesis tools and methodologies basically transform the control structures among function calls and/or sets of statements, with little modification to statements themselves. For example, the systems might differ only in statement order, dataflows (for differing amounts of parallelism), or abstraction levels. For such cases, we have developed an approach based on higher level static code analysis, and we have implemented a tool targeted at the SpecC language