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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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. …
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. …