complexity

Invited: Advances in formal methods for the design of analog/mixed-signal systems

Analog/mixed-signal (AMS) systems are rapidly expanding in all domains of information and communication technology. They are a critical part of the support for large-scale high-performance digital systems, provide important functionalities in …

Compositional Model Checking of Concurrent Systems

This paper presents a compositional framework to address the state explosion problem in model checking of concurrent systems. This framework takes as input a system model described as a network of communicating components in a high-level description …

Verification of timed circuits with failure-directed abstractions

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 …

Automatic synthesis of gate-level timed circuits with choice

This paper presents a CAD tool for the automatic synthesis of gate-level timed circuits from general specifications to basic gates such as AND gates, OR gates, and C-elements. Timed circuits are a class of asynchronous circuits that incorporate …

Synthesis of timed asynchronous circuits

The authors present a systematic procedure for synthesizing timed asynchronous circuits using timing constraints dictated by system integration, thereby facilitating natural interaction between synchronous and asynchronous circuits. Their timed …

Synthesis of timed asynchronous circuits

A synthesis method that utilizes timing constraints to generate timed asynchronous circuits is presented. By unfolding the cyclic graph specification of an asynchronous circuit into an infinite acyclic graph, it is possible to use efficient …