Symbolic Model Checking of Analog/Mixed-Signal Circuits

Abstract

This paper presents a Boolean based symbolic model checking algorithm for the verification of analog/mixed-signal (AMS) circuits. The systems are modeled in VHDL-AMS, a hardware description language for AMS circuits. The VHDL-AMS description is compiled into labeled hybrid Petri nets (LH-PNs) in which analog values are modeled as continuous variables that can change at rates in a bounded range and digital values are modeled using Boolean signals. System properties are specified as temporal logic formulas using timed CTL (TCTL). The verification proceeds over the structure of the formula and maps separation predicates to Boolean variables. The state space is thus represented as a Boolean function using a binary decision diagram (BDD) and the verification algorithm relies on the efficient use of BDD operations.

Publication
2007 Asia and South Pacific Design Automation Conference
David Walter
David Walter
Amazon (AWS S3), Senior SDE
Scott Little
Scott Little
Maxim Integrated, EDA

Related