Verification of embedded systems is complicated by the fact that they are composed of digital hardware, analog sensors and actuators, and low level software. In order to verify the interaction of these heterogeneous components, it would be beneficial …
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 …
Abstract models of analog/mixed-signal (AMS) circuits can be used for formal verification and system-level simulation. The difficulty of creating these models precludes their widespread use. This paper presents an automated method to generate …
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 …
System on a chip design results in the integration of digital, analog, and mixed-signal circuits on the same substrate which further complicates the already difficult validation problem. This paper presents a new model, labeled hybrid Petri nets …
The traditional approach to validate analog circuits is to utilize extensive SPICE-level simulations. The main challenge of this approach is knowing when all important corner cases have been simulated. A new alternative is to utilize formal …
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 an efficient method for verifying hazard freedom in timed asynchronous circuits. Timed circuits are a class of asynchronous circuits that utilize explicit timing information for optimization throughout the entire design process. …
The major barrier that prevents the application of formal verification to large designs is state explosion. This paper presents a new approach for verification of timed circuits using automatic abstraction. This approach partitions the design into …
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, …