Abstract
When modeling the logic functionality, hardware can be viewed as a Finite State Machine (FSM) [7]. The power-up state of hardware cannot be determined uniquely, therefore the FSM modeling the hardware does not have an initial state (or a set of initial states). Instead, it has a set of legal operation states, and it must be brought into this set of operation states from any power-up state by a reboot sequence.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Huang, S.-Y., Cheng, K.-T.: Formal Equivalence Checking and Design Debugging. Kluwer Academic Publishers, Dordrecht (1998)
Kaiss, D., Goldenberg, S., Hanna, Z., Khasidashvili, Z.: Seqver: A Sequential Equivalence Verifier for Hardware Designs. In: ICCD (2006)
Khasidashvili, Z., Hanna, Z.: TRANS: Efficient sequential verification of loop-free circuits. In: HLDVT (2002)
Khasidashvili, Z., Skaba, M., Kaiss, D.: Theoretical Framework for Compositional Sequential Hardware Equivalence Verification in Presence of Design Constraints. In: ICCAD (2004)
Khasidashvili, Z., Skaba, M., Kaiss, D.: Post-reboot equivalence and compositional verification of hardware. In: FMCAD (2006)
Kohavi, Z.: Switching and Finite Automata Theory. McGraw-Hill, New York (1978)
Moon, I.-H., Bjesse, P., Pixley, C.: A compositional approach to the combination of combinational and sequential equivalence checking of circuits without known reset states. In: DATE (2007)
Pixley, C.: A theory and implementation of sequential hardware equivalence. IEEE transactions on CAD (1992)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Khasidashvili, Z. (2008). On Formal Equivalence Verification of Hardware . In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds) Computer Science – Theory and Applications. CSR 2008. Lecture Notes in Computer Science, vol 5010. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79709-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-79709-8_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79708-1
Online ISBN: 978-3-540-79709-8
eBook Packages: Computer ScienceComputer Science (R0)