EVENT-DRIVEN VERIFICATION OF SWITCH-LEVEL CORRECTNESS CONCERNS

RADU NEGULESCU
Department of Computer Science
University of Waterloo
Waterloo, Ontario, Canada N2L 3G1
email: radu@maveric.uwaterloo.ca

Abstract

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.

Keywords

Verification, switch-level, concurrency, asynchronous, event-driven, safety, deadlock, speed-independence, process spaces

Paper.
Go to the Maveric group publication index.
Go to the Maveric group home page.