We propose a technique for verification of MOS circuits, focusing on signal transitions (events) rather than signal levels. Diverse conditions, behaviors, and even delay assumptions are modeled as processes that can be coupled and compared to circuit specifications in a unified formalism. Verification is performed modularly and hierarchically by a BDD-based tool. We illustrate this technique on a self-timed RAM.
Verification, switch-level, concurrency, asynchronous, event-driven, safety, deadlock, speed-independence, process spaces
Go to the Maveric group publication index.
Go to the Maveric group home page.