Loading...
Please wait, while we are loading the content...
Similar Documents
AD-A 274 375 ImhhmhIhIII * Symbolic Model Checking for Sequential Circuit Verification
| Content Provider | Semantic Scholar |
|---|---|
| Author | Clarke, Michael Long Ilai, McU M. |
| Abstract | The temporal logic model checking algorithm of Clarke, Emerson, and. Sistla [17] is modilied to represent state graphs using hmM deision diarg ns (BDDs) [7] and parfitoned wuaition relstions [10, 11]. Because this representation captures some of the regularity in the state space of circuits with data path logic, we are able to verify circuits with an extremely large number of states. We demonstrate this new technique on a synchronous pipelined design with approximately 5 x 101m states. Our model checking algorithm handles funl CTL with fairne constraints. Consequently, we are able to express a number of important liveness and fairness properties, which would otherwise not be expressible in CTL. We give empirical results on the performance of the.algorithm applied to both synchronous and asynchronous circuits with data path logic. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.dtic.mil/dtic/tr/fulltext/u2/a274375.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
