The increasing integration of analog/mixed-signal (AMS) circuits into system designs has further complicated an already difficult verification problem. Recently, formal verification, which has been successful in the purely digital domain, has made …
Researchers are now developing synthetic genetic circuits to manipulate the biochemical processes within living cells. In order to model and predict the behavior of these circuits, the designer must account for numerous reactions among many chemical …
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 …
This paper presents a behavioral synthesis method for asynchronous circuits with bundled-data implementation. This paper extends a behavioral synthesis method for synchronous circuits so that an RTL model of bundled-data implementation is synthesized …
This paper presents an efficient method for verifying hazard-freedom in gate-level timed asynchronous circuits. Timed circuits are a class of asynchronous circuits that are optimized using explicit timing information. In asynchronous circuits, …
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 …
Using a level-oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model datapath circuits. On the other hand, in order to use such a model on large circuits, …
This paper presents a technique to estimate the stochastic cycle period (SCP), a performance metric for timed asynchronous circuits. This technique uses timed stochastic Petri nets (TSPN) which support choice and arbitrary delay distributions. The …
This paper presents a technique to estimate the stochastic cycle period (SCP), a performance metric for timed asynchronous circuits. This technique uses timed stochastic Petri nets (TSPN) which support choice and arbitrary delay distributions. The …