The enormous number of states reachable during explicit model checking is the main bottleneck for scalability. This paper presents approaches of using decision diagrams to represent very large state space compactly and efficiently. This is possible …
This paper presents two symbolic model checking algorithms for the verification of analog/mixed-signal circuits. The first model checker utilizes binary decision diagrams while the second is a bounded model checker that uses a satisfiability modulo …
Synthetic biology uses engineering principles to design circuits out of genetic materials that are inserted into bacteria to perform various tasks. While synthetic combinational Boolean logic gates have been constructed, there are many open issues in …
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 …
This paper presents a method to address state explosion in timed-circuit verification by using abstraction directed by the failure model. This method allows us to decompose the verification problem into a set of subproblems, each of which proves that …
This paper presents a new timing analysis algorithm for efficient state space exploration during the synthesis of timed circuits or the verification of timed systems. The source of the computational complexity in the synthesis or verification of a …
The design and synthesis of asynchronous circuits is gaining importance in both the industrial and academic worlds. Timed circuits are a class of asynchronous circuits that incorporate explicit timing information in the specification. This …