|
IBM's Verification Track 2005
November 13, 2005
Organized by IBM Research Lab in Haifa, Israel
Verification Track Abstracts
Path-based System-level Stimuli Generation
Shady Copty, Yoav Katz, Itai Jaeger, and Michael Vinov, IBM Haifa Labs
Over the last few years, there is increasing emphasis on integrating ready-made components (IP, cores) into complex system-on-a-chip (SoC) designs. The verification of such designs poses new challenges. At the heart of these challenges stands the requirement to verify the integration of several previously designed components in a relatively short time.
Simulation-based methods are the main verification methodology used for system-level functional verification of SoC designs and therefore stimuli generation plays an important role in this field.
We offer a solution to a common challenge in the context of system verification: Bridging the gap between the need to provide a high-level view of the system in the verification plan, and the necessity of low-level, concrete details in stimuli generation.
We present a generation scheme in which the system behavior is defined by the combination of transaction-based modeling, local component behavior, and the topology of the system. We show how this approach allows the implementation of the verification plan using high-level constructs and promotes the reuse of verification IP.
The ideas described below were implemented as part of X-Gen, a system-level test-case generator developed in IBM.
Conflicting Directions in Hierarchical Verification
Yoav Hollander, Verification Division chief technology officer, Cadence
Complex systems are built, and often verified, in a hierarchical fashion.
For instance, consider a "DMA block" inside an "audio sub-system" inside a "main SoC" inside a "cell phone" inside a "cellular system".
For time-to-market reasons, people are trying to parallelize the verification of the various levels. Also, specifications keep changing. Thus, specifications for a higher level may change well after the verification for the lower levels has started.
This presentation will try to assess the influence of this state of affairs on verification philosophy and practice. For instance, it will discuss the relevance of Coverage Driven Verification at the higher levels, as compared to informal, use-case-based verification.
Multi-core Systems
Michael Rosenfield, Director of VLSI Systems, IBM Research
Future improvements in systems performance will require an integrated design approach. We face fundamental challenges in silicon technology, power, and design. In this talk, I will first provide a brief overview of the IBM Research Division and the VLSI Systems organization. I will then review the current and future environments that affect system design, and then focus on multi-core processor design along with software and performance implications.
PROSYD: PSL-based Methods for Specification, Design and Verification
Cindy Eisner, IBM Haifa Labs
PROSYD is a Sixth Framework European Union project based on the emerging standard PSL. PSL (property specification language) is a standard language for the specification of a hardware design using properties. Traditionally, properties are the core of assertion-based verification, in which assertions about the expected behavior of the design are the core of the verification process. In recent years, assertion-based verification has proven to be an effective and efficient means to achieve high-quality designs. The goal of PROSYD is to expand the use of properties throughout the design cycle to the specification and design stages in addition to the verification stage, with the expectation of improving the effectiveness and efficiency of these stages as well.
In the proposed presentation, I will present the PROSYD vision, including specific tools that are envisioned as well as their expected use in the design flow.
The Safety Simple Subset
Shoham Ben-David, University of Waterloo, Dana Fisman, Weizmann Institute of Science, and Sitvanit Ruah, IBM Haifa Labs
Regular-LTL (RLTL) extends LTL with regular expressions, and it is the core of the IEEE standard temporal logic PSL. Safety formulas of RLTL, as well as of other temporal logics, are easier to verify than other formulas. This is because verification of safety formulas can be reduced to invariance checking using an auxiliary automaton recognizing violating prefixes.
In this paper, we define a special subset of safety RLTL formulas, called RLTL^{LV}, for which the automaton built is \emph{linear} in the size of the formula. We then give two procedures for constructing such an automaton; the first provides a translation into a regular expression of linear size, while the second constructs the automaton directly from the given formula. We have derived the definition of RLTL^{LV} by combining several results in the literature, and we devote a major part of the paper to reviewing these results and exploring the involved relationships.
Keynote: A Case for Runtime Validation of Hardware
Sharad Malik, Princeton University
Increasing hardware design complexity has resulted in significant challenges for hardware design verification. The growing "verification gap" between the complexity of what we can verify and what we can fabricate/design is indicative of a crisis that is likely to get only worse with increasing complexity. A variety of methodology and tool solutions have been proposed to deal with this crisis, but there is little optimism that a single solution or even a set of cooperative solutions will be scalable to enable future design verification to be cost effective. It is time we reconcile ourselves to the fact that hardware, like software, will be shipped with bugs in it. One possible solution to deal with this inevitable scenario is to provide support for runtime validation that detects functional failures at runtime and then recovers from such failures. Such runtime validation hardware will increasingly be used to handle dynamic operational failures caused by reduced reliability of devices due to large process variations as well as increasing soft errors. Expanding the use of such hardware to deal with functional design failures provides for an on-chip insurance policy when design errors inevitably slip through the verification process.
This talk will discuss the strengths and weaknesses of this form of design validation, some possible forms this may take, and implications on design methodology.
Assertion-based Verification for the SpaceCAKE Multiprocessor - A Case Study
Milind Kulkarni and Benita Bommij, Philips Research India
This paper presents a case study of the application of assertion-based verification to a multi-million-gate design of the SpaceCAKE architecture with shared L2 cache. SpaceCAKE L2 cache is highly configurable and implements Distributed Shared Memory (DSM) architecture. This paper discusses the issues faced during the functional verification of this architecture. A number of techniques are employed to verify the design. The paper serves as a case study for verification of such a complex architecture. A description of the different techniques that were used to verify this architecture and an assessment of using a comprehensive coverage-driven verification plan that exploits the benefits of the traditional simulation techniques through the use of assertions is presented. We have found that the tools, currently provided by the market, for assertion-based static verification approach need more maturity. A 50% reduction in debug time has been achieved through the use of assertions.
Simultaneous SAT-based Model Checking of Safety Properties
Zurab Khasidashvili, Alexander Nadel, Amit Palti, and Ziyad Hanna, Design Technology Solutions, INTEL Corporation, Tel Aviv University
We present several algorithms for simultaneous SAT (propositional satisfiability) based model checking of safety properties. More precisely, we focus on Bounded Model Checking and Temporal Induction methods for simultaneously verifying multiple safety properties on the same model. The most efficient among our proposed algorithms for model checking are based on a simultaneous propositional satisfiability procedure (SSAT for short), which we design for solving related propositional objectives simultaneously, by sharing the learned clauses and the search. The SSAT algorithm is fully incremental in the sense that all clauses learned while solving one objective can be reused for the remaining objectives. Furthermore, our SSAT algorithm ensures that the SSAT solver will never re-visit the same sub-space during the search, even if there are several satisfiability objectives, hence one traversal of the search space is enough. Finally, in SSAT, all SAT objectives are watched simultaneously, thus we can solve several other SAT objectives when the search is oriented to solve a particular SAT objective first. Experimental results on Intel designs demonstrate that our new algorithms can be orders of magnitude faster than the previously known techniques in this domain.
A Decision Heuristic Based on an Abstraction/Refinement Model
Roman Gershman and Ofer Strichman, Technion - Israel Institute of Technology
We propose a model for analyzing clause-based decision heuristics in SAT, according to which con ict clauses are abstractions of the clauses from which they were derived. Currently Berkmin is the only published clause-based heuristic, and we analyze its behavior according to our model. We then suggest an alternative clause-based decision heuristic called Clause-Move-To-Front (CMTF), which attempts to follow the order of the clauses in the resolve-graph rather than their chronological order in which they were created. We also show a resolution-based score function for choosing the variable from the selected clause and a similar function for choosing the sign. We implemented the suggested heuristics in our SAT solver HaifaSat. Experiments on hundreds of industrial benchmarks demonstrate the superiority of this method comparing to the Berkmin heuristic. There is still room for research on how to explore better the resolve-graph information, based on the abstraction/refinement model that we propose.
| |
|
