formal verification

Design of Asynchronous Genetic Circuits

Most digital electronic circuits utilize a timing reference to synchronize the progression of signals and enable sequential memory elements. These designs may not be realizable in biological substrates due to the lack of a reliable high-frequency …

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 …

Design of Mixed-Signal Systems With Asynchronous Control

This paper presents a novel workflow for the design of mixed-signal systems with asynchronous control. Current methods rely on synchronous control logic and full-system simulation, which might lead to suboptimal results and even project respins due …

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 …

Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip

A fault-tolerant routing algorithm in Network-on-Chip architectures provides adaptivity for on-chip communications. Adding fault-tolerance adaptivity to a routing algorithm increases its design complexity and makes it prone to deadlock and other …

LEMA: A tool for the formal verification of digitally-intensive analog/mixed-signal circuits

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 …

Using decision diagrams to compactly represent the state space for explicit model checking

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 …

An Improvement in Partial Order Reduction Using Behavioral Analysis

Efficacy of partial order reduction in reducing state space relies on adequate extraction of the independence relation among possible behaviors. However, traditional approaches by statically analyzing system model structures are often not able to …

Verification of Analog/Mixed-Signal Circuits Using Labeled Hybrid Petri Nets

Mixed-signal designs integrate digital and analog circuits which complicates the already difficult verification problem. This paper presents a model, labeled hybrid Petri nets (LHPNs), that is developed to model this heterogeneous set of components. …

State space reductions for scalable verification of asynchronous designs

This paper presents several state space reductions for verifying non-trivial asynchronous designs with a compositional minimization approach. These reductions result in a reduced model that contains the exact set of observably equivalent behavior. …