Name
Abstract | ||
|---|---|---|
This paper presents a Boolean based symbolic model checking algorithm for the verification of analog/mixed-signal (AMS) circuits. The systems are modeled in VHDL-AMS, a hardware description language for AMS circuits. The VHDL-AMS description is compiled into labeled hybrid Petri nets (LH-PNs) in which analog values are modeled as continuous variables that can change at rates in a bounded range and digital values are modeled using Boolean signals. System properties are specified as temporal logic formulas using timed CTL (TCTL). The verification proceeds over the structure of the formula and maps separation predicates to Boolean variables. The state space is thus represented as a Boolean function using a binary decision diagram (BDD) and the verification algorithm relies on the efficient use of BDD operations. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1109/ASPDAC.2007.358005 | Yokohama |
Keywords | Field | DocType |
hardware description language,mixed-signal circuits,boolean variable,verification algorithm,symbolic model checking algorithm,bdd operation,analog value,ams circuit,verification proceed,symbolic model checking,vhdl-ams description,boolean signal,boolean variables,binary decision diagram,state space,hardware description languages,boolean functions,temporal logic,boolean function,petri nets,logic design | Boolean function,Boolean network,Boolean circuit,Model checking,Computer science,Algorithm,Binary decision diagram,Boolean data type,Boolean expression,And-inverter graph | Conference |
ISSN | ISBN | Citations |
2153-6961 | 1-4244-0629-3 | 6 |
PageRank | References | Authors |
0.49 | 13 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| D. Walter | 1 | 6 | 0.49 |
| Scott Little | 2 | 132 | 9.42 |
| Nicholas Seegmiller | 3 | 59 | 3.35 |
| C. J. Myers | 4 | 106 | 8.47 |
| Tomohiro Yoneda | 5 | 353 | 41.62 |