Name
Abstract | ||
|---|---|---|
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 fullyformal framework for hardware verification. Our results are extendible to other forms of labeled transition systems and adaptable to other forms of bisimulation used to model and verify complex hardware and software systems. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1109/FMCAD.2006.25 | FMCAD |
Keywords | Field | DocType |
compositional verification,hardware verification,formal property verification,compositional hardware verification,post-reboot equivalence,complex hardware,post-reboot bisimulation,formal hardware verification,post-reboot operation state,combinational equivalence verification,alignability equivalence,equivalence verification,finite state machines,software systems,finite state machine,formal verification | Reboot,Computer science,Intelligent verification,Theoretical computer science,Software system,Finite-state machine,Real-time computing,Equivalence (measure theory),Bisimulation,Computer hardware,High-level verification,Formal verification | Conference |
ISBN | Citations | PageRank |
0-7695-2707-8 | 6 | 0.55 |
References | Authors | |
11 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Zurab Khasidashvili | 1 | 307 | 25.40 |
| Marcelo Skaba | 2 | 37 | 2.50 |
| Daher Kaiss | 3 | 89 | 7.32 |
| Ziyad Hanna | 4 | 292 | 17.66 |