3C: Model Checking and Applications to Digital and Analog Circuits


3C-1
Title Deeper Bound in BMC by Combining Constant Propagation and Abstraction
Author Roy Armoni (-, Israel), Limor Fix (Intel, United States), Ranan Fraer (Intel, Israel), *Tamir Heyman (Carnegie Mellon University, United States), Moshe Vardi (Rich University, United States), Yakir Vizel, Yael Zbar (Intel, Israel)
Abstract The most successful technologies for automatic verification of large industrial circuits are bounded model checking, abstraction, and iterative refinement. Previous work has demonstrated the ability to verify circuits with thousands of state elements achieving bounds of at most a couple of hundreds. In this paper we present several novel techniques for abstraction-based bounded model checking. specifically, we introduce a constant-propagation technique to simplify the formulas submitted to the CNF SAT solver; we present a new proof-based iterative abstraction technique for bounded model checking; and we show how the two techniques can be combined. The experimental results demonstrate our ability to handle circuit with several thousands state elements reaching bounds nearing 1,000.
Slides (pdf file) 3C-1

3C-2
Title Efficient BMC for Multi-Clock Systems with Clocked Specifications
Author *Malay K Ganai, Aarti Gupta (NEC LABS America, United States)
Abstract Current industry trends in system design — multiple clocks, clocks with arbitrary frequency ratios, multi-phased clocks, gated clocks, level-sensitive latches, combined with clocked specifications – pose additional challenges to verification efforts. We propose an integrated solution that improves SAT-based Bounded Model Checking (BMC) by orders of magnitude, for verification of synchronous multi-clock systems with clocked LTL properties. Our main contributions are: a) Efficient clock modeling schemes to handle clock related challenges uniformly, b) Generation of automatic schedules and clock constraints to avoid unnecessary unrolling and loop-checks in BMC, c) Dynamic simplification of BMC problem instances with clock constraints, and d) Customized BMC translations—with incremental formulations and learning—to directly handle PSL-style clocked specifications. We demonstrate the effectiveness of our approach on some OpenCores multi-clock system benchmarks.
Slides (pdf file) 3C-2

3C-3
Title Symbolic Model Checking of Analog/Mixed-Signal Circuits
Author *David Walter, Scott Little, Nicholas Seegmiller, Chris Myers (University of Utah, United States), Tomohiro Yoneda (National Institute of Informatics, Japan)
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 (LHPNs) 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.
Slides (pdf file) 3C-3

3C-4
Title Efficient Automata-Based Assertion-Checker Synthesis of SEREs for Hardware Emulation
Author *Marc Boule, Zeljko Zilic (McGill University, Canada)
Abstract In this paper, we present a method for generating checker circuits from sequential-extended regular expressions (SEREs). Such sequences form the core of increasingly-used Assertion-Based Verification (ABV) languages. A checker generator capable of transforming assertions into efficient circuits allows the adoption of ABV in hardware emulation. Towards that goal, we introduce the algorithms for sequence fusion and length matching intersection, two SERE operators that are not typically used over regular expressions. We also develop an algorithm for generating failure detection automata, a concept critical to extending regular expressions for ABV, as well as present our efficient symbol encoding. Experiments with complex sequences show that our tool outperforms the best known checker generator.
Slides (pdf file) 3C-4
Last Updated on: January 26, 2007