|
IBM Hardware Verification Track 2006
October 23, 2006
Organized by IBM Research Lab in Haifa, Israel
Abstracts
Invited speaker: Sweet and Sour: Adventures in the Development of a Property Specification Language
Cindy Eisner, IBM Haifa Research Labs
This talk is about the creation and development of the recently standardized property specification language PSL. I will tell you what PSL is and what you can do with it, and speak a little about its history. I will give some insights into the difficulties involved in developing a property specification language by presenting some thorny issues we encountered and solved, and some that we encountered and have not yet solved.
Model Checking PSL using HOL and SMV
Thomas Tuerk, Klaus Schneider, and Mike Gordon, University of Kaiserslautern, Germany / University of Cambridge, UK
In our previous work, we formally validated the correctness of a translation from a subset of Accellera's Property Specification Language (PSL) to linear temporal logic (LTL) using the HOL theorem prover. We also built an interface from HOL to the SMV model checker based on a formal translation of LTL to omega-automata. In this paper, we describe how this work has been extended and combined to produce a model checking infrastructure for a significant subset of PSL that works by translating model checking problems to equivalent checks for the existence of fair paths through a Kripke structure specified in higher order logic. This translation is done by theorem proving in HOL, so it is proven to be correct. The existence check is carried out using the interface from HOL to SMV. Moreover, we have applied our infrastructure to implement a tool for validating the soundness of a separate PSL model checker.
Using Linear Programming Techniques for Scheduling-based Random Test-case Generation
Amir Nahir, Yossi Shiloach, and Avi Ziv, IBM Haifa Research Lab
Multimedia SoCs are characterized by a main controller that directs the activity of several cores, each of which is in charge of a stage in the processing of a media stream. Stimuli generation for such systems can be modeled as a scheduling problem that assigns data items to the processing elements of the system. We present a linear programming (LP) modeling scheme for these scheduling problems. We implemented this modeling scheme as part of SoCVer, a stimuli generator for multimedia SoCs. Experimental results show that this LP-based scheme allows easier modeling and provides better performance than CSP-based engines that are widely used for stimuli generation.
Extracting a Simplified View of Design Functionality Based on Vector Simulation
Onur Guzey, Hung-Pin (Charles) Wen, Li-C. Wang, Tao Feng, Hillel Miller and Magdy Abadir, University of California Santa Barbara, Cadence, Freescale Semiconductor
This paper presents a simulation-based methodology for extracting a simplified view of design functionality from a given module. Such a simplified design view can be used to facilitate test pattern justification from the outputs of the module to the inputs of the module.
In this work, we formulate this type of design simplification as a learning problem. By developing a scheme for learning word-level functions, we point out that the core of the problem is to develop an efficient Boolean learner. We discuss the implementation of such a Boolean learner and compare its performance with the one of the best-known learning algorithms, the Fourier analysis based method. We present experimental results that illustrate the implementation of the simulation-based methodology and its usage for extracting a simplified view of the Open RISC 1200 data path.
Reusable On-Chip System Level Verification for Simulation Emulation and Silicon
Avishay Maman, Sharon Goldschlager, Hillel Miller, David Bell, Rob Slater, Oded Bin-Moshe, Nissan Levi, and Hagit Gilboa, Freescale Semiconductor Israel
Absolute verification of System On Chip (SoC) has become infeasible due to the huge number of chip-level scenarios to cover. System level verification validates the integration of independently-verified components such as cores, peripherals, caches, and memories. Some of the most elusive system level bugs can only be detected by scenarios that exercise several components, each in a different configuration. This paper presents a methodology for SoC system level verification, comprised of high level software that simultaneously exercises multiple hardware components. It consists of a light operating system that schedules threads for non-preemptive interleaved runs. Each thread complies with a uniform structure, and activates a specific functionality of the system. The interaction of multiple threads allows for realistic scenarios, testing bus traffic stress, multiplexing, and state machines, reaching unanticipated corner-cases. The OS includes a runtime constraint solver for randomly selecting parameters for peripheral configuration. Similar capabilities require dedicated test-benches such as Vera or e, which lack compilers and thus cannot be applied to silicon. The described framework is not dependent on a specific tool, but based on C, therefore compiled to chip. Re-usability over the project lifecycle is achieved by having the same test-cases run on simulation, emulation, and silicon, allowing comparison of test results. A simulation speed-up of over 100X is achieved, by replacing the RTL core with stub, compiling application code to the host machine, and using an API for the interaction of the design and application. This methodology was applied to the New Quad-Core MSC8144 supporting a very high I/O bandwidth and providing an optimal DSP solution for wireline/wireless infrastructure applications. The same methodology was used in simulation, emulation, and silicon modes. It led to high coverage of system level scenarios, and discovery of system level bugs that could have taken other methodologies much
longer to find.
Keynote: System Modeling and Formal Verification with UCLID
Randal E. Bryant, Dean and University Professor, School of Computer Science, Carnegie Mellon University
The UCLID verifier models systems at a very high level by abstracting data representations and operations while maintaining a detailed representation of the control logic. The UCLID modeling language extends that of CMU SMV, a bit-level model checker, to include integer and function state variables, addition by constants, and relational operations. The underlying logic is expressive enough to model a wide range of systems, but it still permits a decision procedure based on Boolean satisfiability technology. Most recently, we have developed powerful predicate abstraction methods that can automatically generate and prove system invariants using techniques similar those used in symbolic model checking. UCLID has been used to verify a variety of hardware designs, including out-of-order microprocessors and cache coherency protocols, as well as abstract synchronization protocols such as Lamport's Bakery algorithm.
Automatic Fault Localization for Property Checking
Stefan Staber, G?rschwin Fey, Roderick Bloem, and Rolf Drechsler, Graz University of Technology, Austria / University of Bremen, Germany
We present an efficient, fully automatic approach to fault localization for safety properties stated in linear time logic. We view the failure as a contradiction between the specification and the actual behavior and look for components that explain this discrepancy. We find these components by solving the satisfiability of a propositional Boolean formula. We show how to construct this formula and how to extend it so that we find exactly those components that can be used to repair the circuit for a given set of counterexamples. Furthermore, we discuss how to efficiently solve the formula by using the proper decision heuristics and simulation based preprocessing. We demonstrate the quality and efficiency of our approach by experimental results.
Verification of Data Paths using Unbounded Integers: Automata Strike Back
Alexander Tobias Schuele and Klaus Schneider, University of Kaiserslautern, Germany
We present a decision procedure for quantifier-free Presburger arithmetic that is based on a polynomial time translation of Presburger formulas to alternating finite automata (AFAs). Moreover, our approach leverages the advances in SAT solving by reducing the emptiness problem of AFAs to satisfiability problems of propositional logic. To obtain a complete decision procedure, we use an inductive style of reasoning as proposed for proving safety properties in bounded model checking. Besides linear arithmetic constraints, our decision procedure can deal with bitvector operations that frequently occur in hardware design. Thus, it is well-suited for the verification of data paths at a high level of abstraction.
| |
Proceedings publication: Springer Lecture Notes in Computer Science
|
