Name
Abstract | ||
|---|---|---|
Current statistics attribute up to 75% of the overall design costs of digital hardware and embedded system development to the verification task. In recent years, the trend to augment functional with formal verification tries to alleviate this problem. Efficient property checking algorithms allow automatic verification of middle-sized designs nowadays. However, the steadily increasing design sizes still leave verification the major bottleneck, because formal methodologies do not yet scale to very large designs. In this paper we present the formal verification tool SymC based on forward state space traversal and so-called AR-automata for property checking, both internally represented with BDDs. Furthermore, we introduce a new methodology called dynamic guiding. This methodology best suits multimodule concurrent finite state machine (FSM) designs. The aim of guiding is to reduce the intermediate and final BDD size, which in turn makes this verification technique applicable to larger designs. Our approach exploits abstract information of the design in the form of regular expressions and effectively guides the symbolic traversal depending on the verified property. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1109/HLDVT.2004.1431223 | HLDVT |
Keywords | Field | DocType |
formal methodology,verification task,automatic verification,efficient property checking algorithm,formal verification tool,design size,bounded property checking,large design,larger design,verification technique,formal verification,embedded systems,state space,embedded system,finite state machine,regular expression,finite state machines | Formal equivalence checking,Functional verification,Model checking,Intelligent verification,Computer science,Theoretical computer science,Runtime verification,High-level verification,Software verification,Formal verification | Conference |
ISSN | ISBN | Citations |
1552-6674 | 0-7803-8714-7 | 3 |
PageRank | References | Authors |
0.37 | 7 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| P. M. Peranandam | 1 | 4 | 0.72 |
| R. J. Weiss | 2 | 4 | 0.72 |
| Jürgen Ruf | 3 | 122 | 23.04 |
| T. Kropf | 4 | 4 | 1.06 |
| W. Rosenstiel | 5 | 15 | 4.15 |