SAT-Based Methods for Sequential Hardware Equivalence Verification without Synchronization
| Autor: | Ziyad Hanna, Zurab Khasidashvili |
|---|---|
| Rok vydání: | 2003 |
| Předmět: |
Model checking
High-level verification Functional verification General Computer Science business.industry Computer science Theoretical Computer Science Intelligent verification Synchronization (computer science) State (computer science) business Reset (computing) Equivalence (measure theory) Computer hardware Computer Science(all) Hardware_LOGICDESIGN |
| Zdroj: | Electronic Notes in Theoretical Computer Science. 89:593-607 |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/s1571-0661(05)82545-9 |
| Popis: | The BDD- and SAT-based model checking and verification methods normally require an initial state. Here we are concerned with sequential hardware verification, where an initial state must be one of the reset states. In practice, a reset state is not always given by the designer, and computing a reset state of a circuit is a hard problem. In this paper we propose a method allowing usage of SAT-based verification methods without a need for a user-given or a computed initial state. The idea is to employ a binary encoding of 3-valued modeling of circuits, and use the undefined state X as a reset state. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect