Name
Abstract | ||
|---|---|---|
In this paper we firstly introduce a novel symbolic model checker (MScheck) for mixed-signal circuits. MScheck is capable to conflate the continuous behavior, typical for analog designs, and the discrete behavior in the digital domain for formal verification. Timing information of both systems will be symbolically stored within multi terminal binary decision diagrams (MTBDDs) for the entire verification procedure. The effectiveness of our approach is demonstrated on a phase locked loop (PLL) by formal verification of the locking property1.
|
Year | DOI | Venue |
|---|---|---|
2008 | 10.1109/ASPDAC.2008.4483984 | ASP-DAC |
Keywords | Field | DocType |
continuous behavior,novel symbolic model checker,mixed-signal circuit,mixed-signal model checking,multi terminal binary decision,digital domain,discrete behavior,symbolic approach,entire verification procedure,analog design,timing information,formal verification,computer science,mixed signal circuits,phase lock loop,automata,model checker,algorithm,phase locked loop,phase locked loops,binary decision diagram,data structures,analog circuits,model checking,boolean functions,digital circuits | Boolean function,Digital electronics,Model checking,Analogue electronics,Computer science,Binary decision diagram,Real-time computing,Electronic engineering,Mixed-signal integrated circuit,Symbolic trajectory evaluation,Formal verification | Conference |
ISSN | ISBN | Citations |
2153-6961 | 978-1-4244-1922-7 | 4 |
PageRank | References | Authors |
0.59 | 3 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alexander Jesser | 1 | 15 | 2.15 |
| Lars Hedrich | 2 | 267 | 31.08 |