Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints

We are interested in sequential hardware equivalence (or alignability equivalence) verification of synchronous sequential circuits as stated in C. Pixley (1992). To cope with large industrial designs, the circuits must be divided into smaller subcircuits and verified separately. Furthermore, in order to succeed in verifying the subcircuits, design constraints must be added to the subcircuits. These constraints mimic "essential" behavior of the subcircuit environment. In this work, we extend the classical alignability theory in the presence of design constraints, and prove a compositionality result allowing inferring alignability of the circuits from alignability of the subcircuits. As a result, we build a divide and conquer framework for alignability verification. This framework is successfully used on Intel designs.