RTL verification of timed asynchronous and heterogeneous systems using symbolic model checking

This paper describes a tool-supported methodology for the register-transfer-level formal verification of a growing hardware design paradigm-timed asynchronous systems. These systems are a network of communicating asynchronous and synchronous components and have correctness constraints that depend on specified bounded delays. This paper formalizes the verification problem and demonstrates how time-discretization, abstraction, and non-determinism can lead to a system model comprised of communicating finite state machines composed synchronously. The paper then describes a translator that accepts structural VHDL system description along with controller specifications and generates the input to a symbolic model checker (SMV). Finally, we describe two case studies in which concurrent verification and design led to the correction of many errors not easily found using simulation.