Post-reboot Equivalence and Compositional Verification of Hardware

We introduce a finer concept of a Hardware Machine, where the set of post-reboot operation states is explicitly a part of the FSM definition. We formalize an ad-hoc flow of combinational equivalence verification of hardware, the way it was performed over the years in the industry. We define a concept of post-reboot bisimulation, which better suits the Hardware Machines, and show that a right form of combinational equivalence is in fact a form of post-reboot bisimulation. Further, we show that alignability equivalence is a form of post-reboot bisimulation, too, and the latter is a refinement of alignability in the context of compositional hardware verification. We find that post-reboot bisimulation has important advantages over alignability also in the wider context of formal hardware verification, where equivalence verification is combined with formal property verification and with validation of a reboot sequence. As a result, we propose a more comprehensive, compositional, and fullyf...

• Type: Conference
• Year: 2006
• Where: FMCAD
• Authors: Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss, Ziyad Hanna
• Keywords: Combinational Equivalence, FMCAD 2006, Formal Methods, Hardware Verification, Post-reboot Bisimulation