A compositional theory for post-reboot observational equivalence checking of hardware

We propose an equivalence checking theory in a wider-than-usual sense. The theory shows how to combine Formal Equivalence Checking (FEC) of specification and implementation models with Assertion Based Verification (ABV) of the specification model, and with Reboot Sequence Checking (RSC) on both models, to ensure that the implementation model has the intended logic functionality. Here, FEC is performed to ensure that the input-output behavior of the models coincides in post-reboot states. ABV ensures that the specification model has the intended logic functionality captured by temporal assertions. RSC ensures deterministic behavior of the models after reboot. We propose a flexible compositional theory for FEC, an abstraction method for ABV, and a scalable algorithm for RSC, enabling performance of all three activities in a modular, compositional manner, and largely independently: FEC and ABV are performed without knowing the actual reboot sequence (and the respective initial states) of the two models; and FEC, ABV and RSC have the same observables.