(Back to Session Schedule)

The 15th Asia and South Pacific Design Automation Conference

Session 7C  Design Verification and Debugging
Time: 8:30 - 10:10 Thursday, January 21, 2010
Location: Room 101C
Chairs: Yirng-An Chen (Marvell Corp., U.S.A.), Jie-Hong (Roland) Jiang (National Taiwan University, Taiwan)

7C-1 (Time: 8:30 - 8:55)
TitleManaging Verification Error Traces with Bounded Model Debugging
Author*Sean Safarpour (Vennsa Technologies, Canada), Andreas Veneris, Farid Najm (University of Toronto, Canada)
Pagepp. 601 - 606
Keyworddebugging, verification, simulation, formal
AbstractManaging long verification error traces is one of the key challenges of automated debugging engines. Today, debuggers rely on the iterative logic array to model sequential behavior which drastically limits their application. This work presents Bounded Model Debugging, an iterative, systematic and practical methodology to allow debuggers to tackle larger problems than previously possible. Based on the empirical observation that errors are excited in temporal proximity of the observed failures, we present a framework that improves performance by up to two orders of magnitude and solve 2.7$\times$ more problems than a conventional debugger.
Slides

7C-2 (Time: 8:55 - 9:20)
TitleAutomatic Assertion Extraction via Sequential Data Mining of Simulation Traces
Author*Po-Hsien Chang, Li-C. Wang (University of California, Santa Barbara, U.S.A.)
Pagepp. 607 - 612
KeywordVerification, Simulation traces, Data mining
AbstractThis paper studies the problem of automatic assertion extraction at the input boundary of a given unit embedded in a system. This paper proposes a data mining approach that analyzes simulation traces to extract the assertions. We borrow two key concepts from the sequential data mining and develop an effective assertion extraction approach specific to our problem. These two concepts are (1) the slide-window-based episode definition that decides the space of all potential assertions and (2) the Support-Confidence framework that evaluates the meaningfulness of potential assertions using a given simulation trace. We implement the approach in a system simulation environment built on the AMBA 2.0 standard. Experimental results demonstrate the feasibility of the proposed approachand validity of extracted assertions are verified by comparing to the transactions defined in the specification.

7C-3 (Time: 9:20 - 9:45)
TitleAutomatic Constraint Generation for Guided Random Simulation
Author*Hu-Hsi Yeh, Chung-Yang (Ric) Huang (National Taiwan University, Taiwan)
Pagepp. 613 - 618
Keywordconstraint, simulation, verification
AbstractIn this paper, we proposed an Automatic Target Constraint Generation (ATCG) technique to automatically generate compact and high-quality constraints for the guided random simulation environment. Our objective is to tackle the biggest bottleneck of the entire constrained random simulation process ─ the time-consuming and error-prone manual testbench composition process. By taking only the design under verification and simulation coverage as our inputs, our automatic constraint generation technique can successfully generate just a few key constraints while achieving very high simulation coverage. Our experimental results show that the proposed approach can outperform both directed and random simulations in both coverage and simulation runtime for a variety of designs

7C-4 (Time: 9:45 - 10:10)
TitleA Method for Debugging of Pipelined Processors in Formal Verification by Correspondence Checking
Author*Miroslav Velev, Ping Gao (Aries Design Automation, U.S.A.)
Pagepp. 619 - 624
Keywordformal verification, debugging, pipelined processors, correspondence checking, SAT
AbstractPresented is a method for debugging of pipelined processors in their formal verification with the highly automatic and scalable approach of Correspondence Checking, where a pipelined/superscalar/VLIW implementation is compared against a non-pipelined specification via an inductive correctness criterion based on symbolic simulation in a way that guarantees the correctness of the implementation for all possible execution scenarios. The benefit from the proposed method increases with the complexity of the processor under formal verification. For a 12-stage VLIW processor that imitates the Intel Itanium in many features, the method reduced the size of the EUFM correctness formulas from buggy processors by up to an order of magnitude, the number of Boolean variables in the equivalent propositional correctness formulas and the number of 1s in the counterexample traces by up to 2 orders of magnitude, and resulted in an average speedup in detecting the bugs of 2 orders of magnitude, thus increasing the productivity of the processor designers.