Rule-Based Approaches for Equivalence Checking of SpecC Programs

This paper describes a rule-based approach for equivalence checking of reactive systems. The approach is based on new types of dependence and flow graphs that are more appropriate for reactive languages than traditional notions intended for transformational languages. Equivalence rules utilizing this static dependence and flow information are derived from language semantics. The rules are then applied in a bottom-up fashion, corresponding to the structures of the programs being checked, until equivalence is shown. A prototype toolset has been implemented, and results indicate speedups of several orders of magnitude over more traditional equivalence checkers. The paper describes our approach and tools, and also outlines how our methods can be used in a general equivalence checking system.