Feature selection is essential to rule learning in the context of functional verification. In practice today, features are selected manually and the selection requires domain knowledge. In contrast, this work proposes using automatic feature extraction from design documents as a viable approach to support rule learning. To demonstrate its effectiveness, document-extracted features are employed to learn the rules for covering a set of assertions based on a commercial SoC. Experiments show that 100%-accurate rules can be obtained for more than 70% of the assertions.

Security verification relies on using direct tests manually prepared. Test preparation often requires intensive efforts from experts with in-depth domain knowledge. This work presents an approach to learn from direct tests written by an expert. After the learning, the learned model acts as a surrogate for the expert to produce new tests. The learning software comprises a database for accumulating and sharing security verification knowledge. The learning approach uses process discovery to build an upper-bound model and continuously adds constraints to refine it. We demonstrate the feasibility and effectiveness of the learning approach in a commercial SoC verification environment.

A modern automotive design contains over a hundred microprocessors, several cyber-physical modules, connectivity to a variety of networks, and several hundred megabytes of software. The future is anticipated to see an even sharper rise in complexity of this electronics, with the imminence of driverless vehicles, the potential of connected automobiles within a few years, and work towards seamless integration of automobiles with smart cities and infrastructure systems. Security is a fundamental challenge in the design of automotive systems. Unfortunately, security considerations in automotive systems are complicated by two factors: (1) need for real-time mitigation against in-field threats; and (2) in-field configurability and extensibility of security features. This paper examines the trade-offs between security countermeasures, real-time requirements, and in-field configurability needs for modern automotive systems. We discuss the current state of the practice in automotive security architecture, as well as gaps and challenges that need to be addressed for a viable security solution in future.

This paper investigates how data mining can be applied in functional debug, which is formulated as the problem of explaining a functional simulation error based on human-understandable machine states. We present a rule discovery methodology comprising two steps. The first step selects relevant state variables for constructing the mining dataset. The second step applies rule learning to extract rules that differentiates the tests that excite error behavior from those that do not. We explain the dependency of the second step on the first step and considerations for implementing the methodology in practice. Application of the proposed methodology is illustrated through experiments conducted on a recent commercial SoC design.

This work proposes a methodology of knowledge extraction from constrained-random simulation data. Feature-based analysis is employed to extract rules describing the unique properties of novel assembly programs hitting special conditions. The knowledge learned can be reused to guide constrained-random test generation towards uncovered corners. The experiments are conducted based on the verification environment of a commercial processor design, in parallel with the on-going verification efforts. The experimental results show that by leveraging the knowledge extracted from constrained-random simulation, we can improve the test templates to activate the assertions that otherwise are difficult to activate by extensive simulation.

Along with the shrinking CMOS process and rapid design, scaling, both Iddq values and their variation of chips increase. As a result, the defect leakages become less significant when compared to the full-chip currents, making them more in-distinguishable for traditional Iddq diagnosis. Therefore, in this paper, a new approach called σ-Iddq duagnosis is proposed for reinterpreting original data and diagnosing failing chips, intelligently. The overall flow consists of two key components, (1) σ-Iddq transformation and (2) defect-syndrome matching: σ-Iddq transformation first manifests defect leakages by excluding both the process-variation and design-scaling impacts. Later, defect-syndrome matching applies data mining with a pre-built library to identify types and locations of defects on the fly. Experimental result show that an average of 93.68% accuracy with a resolution of 1.75 defect suspects can be achieved on ISCAS'89 and IWLS'05 benchmark circuits using a 45nm technology, demonstrating the effectiveness of σIddq diagnosis.

Iddq testing has been a critical integral component in test suites for screening unreliable devices. As the silicon technology keeps shrinking, Iddq values and their variation increase as well. Moreover, along with rapid design scaling, defect-induced leakage currents become less significant when compared to full-chip current and also make themselves less distinguishable. Traditional Iddq methods become less effective and cause more test escapes and yield loss. Therefore, in this paper, a new test method named σ-Iddq testing is proposed and integrates (1) a variation-aware full-chip leakage estimator and (2) a clustering algorithm to classify chip without using threshold values. Experimental result shows that σ-Iddq testing achieves a higher classification accuracy in a 45 nm technology when compared to a single-threshold Iddq testing. As a result, both the process-variation and design-scaling impacts are successfully excluded and thus the defective chips can be identified intelligently.

Novel test detection is an approach to improve simulation efficiency by selecting novel tests before their application [1]. Techniques have been proposed to apply the approach in the context of processor verification [2]. This work reports our experience in applying the approach to verifying a commercial processor. Our objectives are threefold: to implement the approach in a practical setting, to assess its effectiveness and to understand its challenges in practical application. The experiments are conducted based on a simulation environment for verifying a commercial dual-thread low-power processor core. By focusing on the complex fixed-point unit, the results show up to 96% saving in simulation time. The main limitation of the implementation is discussed based on the load-store unit with initial promising results to show how to overcome the limitation.

introduction Share on Introduction to special section on verification challenges in the concurrent world Authors: Sandip Ray University of Texas at Austin, TX University of Texas at Austin, TXView Profile , Jayanta Bhadra Freescale Semiconductor Inc., Austin, TX Freescale Semiconductor Inc., Austin, TXView Profile , Magdy S. Abadir Freescale Semiconductor Inc., Austin, TX Freescale Semiconductor Inc., Austin, TXView Profile , Li-C. Wang University of California at Santa Barbara, CA University of California at Santa Barbara, CAView Profile , Aarti Gupta NEC Laboratories America, Inc., Princeton, NJ NEC Laboratories America, Inc., Princeton, NJView Profile Authors Info & Claims ACM Transactions on Design Automation of Electronic SystemsVolume 17Issue 3June 2012 Article No.: 19pp 1–3https://doi.org/10.1145/2209291.2209292Published:05 July 2012Publication History 0citation172DownloadsMetricsTotal Citations0Total Downloads172Last 12 Months1Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

This paper proposes a kernel-based functional test program generation approach for microprocessor test and verification. The fundamental idea in this approach is to select high quality test programs before the simulation from a large number of biased random test programs. Unlike a direct test program generation approach, a selection approach demands much less domain knowledge and intervention from its user for achieving a similar coverage goal, making it more applicable for scenarios targeting on different coverage objectives. We will demonstrate the effectiveness and efficiency of such an approach through performing experiments on a MIPS processor design.

Recent years have seen continuing miniaturization of VLSI technologies, producing chips with very high transistor density. A consequence of this advancement, together with high computational demands of modern applications, is that hardware designs are rising in complexity to make use of all the available transistors. This makes it challenging to develop reliable hardware through hand-crafted RTL implementations. The problem is exacerbated with aggressive time-to-market requirements, leading to a design productivity gap. Electronic System Level (ESL) design is often seen as a solution to this gap: the idea is to raise the design abstraction by specifying a hardware design behaviorally with a high-level language (e.g., SystemC). High-level synthesis translates ESL specifications to RTL, through several inter-dependent transformations (e.g., compilation, scheduling, resource allocation, control synthesis, etc).

Transaction-level modeling is an essential component of system-level design. This paper advocates using rendezvous, a construct common to concurrent programming languages, as a theoretical foundation for transactions. Compared to regular function calls, rendezvous are atomic and support multipartiness and parallel composition. However, scheduling multiparty rendezvous is a challenging task due to its NP-hard complexity. This paper describes a heuristic algorithm that significantly reduces the scheduling complexity in practice. It first constructs a relationship graph among rendezvous. It then simplifies the graph and translates it into a decision tree, which assists the scheduler in partitioning and pruning the search space. Our experimental results show that the algorithm is able to improve the efficiency of the scheduler significantly.

This paper re-examines the soft error effect caused by cosmic radiation in sub 90nm technologies. Considering the impact of process variation, a number of statistical natures of transient faults are found more sophisticated than their static ones. We apply the state-of-the-art statistical learning algorithm to tackle the complexity of these natures and build compact yet accurate generation and propagation models for transient fault distributions. A statistical analysis framework for soft error rate (SER) is also proposed on the basis of these models. Experimental results show that the proposed framework can obtain improved SER estimation compared to the static approaches.

A learning-and-filtering algorithm is proposed to uncover cross-timeframe state-pair constraints for speeding up SAT solving of bounded sequential equivalence checking (BSEC) problems. First, relaxed Boolean functions for flip-flop states at respective timeframes are learned from a small number of simulation data to derive the initial set of the state-pair candidates. Next, each candidate is examined and removed if both values in such a candidate have coordinately appeared during the simulation. Then, the validity of the remaining candidates is checked against the corresponding augmented circuit. Last, only the true constraints are annotated to the BSEC problems to facilitate SAT solving. All benchmark circuits are synthesized under 10 configurations to produce different BSEC problems. Experimental results show that the new SAT solving runs 2-order faster in average compared to using MiniSAT 2.0 only. Moreover, given a time bound, the total number of timeframes can increase by 8X-20X on 4 larger circuits after applying the proposed framework.

Reuse of system-on-chip (SoC) verification stimuli across various design models is a challenging problem. However, if used effectively, it significantly reduces verification time and quickly increases confidence in the robustness of a design. We use pseudo-random stimuli to drive tests on an SoC using simulation BFMs and reuse them on emulation-BFMs. Initial results on a Power Architecture¿Technology-based SoC demonstrate about a 100x speedup on the emulator vis-a¿-vis the simulator.

Multiprocessor systems-on-chip (MPSoC) pose a considerable validation challenge due to their size and complexity. We approach the problem of MPSoC validation through a tool that employs a reusable abstract executable specification written in C++. The tool effectively leverages a simulation-based, trace-driven mechanism. Traces are computed by simulating a system level register-transfer level (RTL) implementation of an MPSoC. The tool then analyzes the traces for correctness by checking them across executions of the abstract executable specification. We have effectively used the tool on various live MPSoC design projects based on the Power Architecture technology (The Power Architecture and Power.org wordmarks and the Power and Power.org logos and related marks are trademarks and service marks licensed by Power.org.). We demonstrate the effectiveness of the technique through results from these projects where we uncovered a number of design errors not found by any other technique.

We present a framework for formal verification of embedded custom memories. Memory verification is complicated by the difficulty in abstracting design parameters induced by the inherently analog nature of transistor-level designs. We develop behavioral formal models that specify a memory as a system of interacting state machines, and relate such models with an abstract read/write view of the memory via refinements. The operating constraints on the individual state machines can be validated by readily available data from analog simulations. The framework handles both static RAM (SRAM) and flash memories, and we show initial results demonstrating its applicability.

Unit-level verification is a critical step to the success of full-chip functional verification for microprocessor designs. In the unit-level verification, a unit is first embedded in a complex software that emulates the behavior of surrounding units, and then a sequence of stimuli is applied to measure the functional coverage. In order to generate such a sequence, designers need to comprehend the relationship between boundaries at the unit under verification and at the inputs to the emulation software. However, figuring out this relationship can be very difficult. Therefore, this paper proposes an incremental learning framework that incorporates an ordered-binary-decision-forest(OBDF) algorithm, to automate estimating the controllability of unit-level signals and to provide full-chip level information for designers to govern these signals. Mathematical analysis shows that the proposed OBDF algorithm has lower model complexity and lower error variance than the previous algorithms. Meanwhile, a commercial microprocessor core is also applied to demonstrate that controllability of input signals on the load/store unit in the microprocessor core can be estimated automatically and information about how to govern these signals can also be extracted successfully.

Functional test-bench development is a tedious and time-consuming process that requires tremendous engineering effort. Developing proper test-benches is crucial for both functional verification and post-silicon performance validation. Constrained random test generation is a popular approach to alleviate the burden of test-bench development. This paper presents an automatic constraint extraction tool that can be easily integrated with an existing commercial constrained random test generation framework. This tool extracts constraints by analyzing test-bench simulation data. These constraints, when added into a test-bench, can provide controllability of signals that are deeply embedded in a complex design. We develop simulation data mining algorithms for constraint extraction and demonstrate the effectiveness of our approach based on OpenSparc Tl microprocessor.

Formal verification of systems-on-chips (SoCs) is an immense challenge to current industrial practice. Most existent formal verification techniques are extremely computation intensive and produce good results only when used on individual sub-components of SoCs. Without major modifications they are of little effectiveness in the SoC world. We attack the problem of SoC verification using an elegant abstraction mechanism, called computation slicing, and show that it enables effective temporal property verification on large designs. The technique targets a set of execution sequences, that is exhaustive with respect to an intended subset of system level properties, and automatically finds counter-example execution sequences in case of errors in the design. We have obtained exponential gains in reducing the global state space using a polynomial-time algorithm, and also applied a polynomial-time algorithm for checking global liveness and safety properties. We have successfully applied the technique to verify properties on two high level transaction based designs - the MSI cache coherence protocol and an admittedly academic SoC having a bus arbiter and a parameterizable number of devices connected to a PCI bus backbone.

Design constraints are artifacts that model an environment of a design under verification by restricting input stimuli to plausible valuations. Judicious usage of design constraints can be effective in eliminating false verification results. Given a particular verification problem, however, it is a difficult proposition to write down all the necessary constraints. We present a technique for automatic generation of design constraints from simple user-provided information about potential design environments. Our method generates a set of design constraints representing varying degrees of assumptions about potential environments of a dynamic circuit. We also present experimental results on verification of custom designed embedded dynamic circuits taken from the Motorola MPC7455 microprocessor.

Equivalence checking between Register Transfer Level (RTL) descriptions and transistor level descriptions of custom memories is an important step in the design flow of high performance microprocessors. Equivalence checking can be done with or without the knowledge of state mapping between the two descriptions. We present evidence that because of state mapping, our verification technique exercises system behavior that exposes hard-to-detect bugs that might otherwise go undetected. This paper defines Crossover Bugs (CB's) that can be present in scan-based custom designs and that are inherently hard-to-detect without state mapping. We demonstrate that such bugs can be missed by equivalence checking techniques that do not have state mappings between the two descriptions. By identifying the state correspondences between the RTL and the transistor implementation of custom memories, a more rigorous equivalence check can be performed compared to traditional equivalence checking methods such as product machine constructions. We also compare the time and memory complexities of crossover bug detection capability of the two equivalence checking approaches. We conclude with experimental results of CB detection on some of the custom designed embedded memories of Motorola's MPC 7455 microprocessor (compliant with IBM's PowerPC instruction set architecture).

Sequential Automatic Test Pattern Generation (ATPG) is extremely computation intensive and produces good results only on relatively small designs. This paper develops an elegant theoretical basis, based on program slicing, for hierarchical ATPG which targets one module at a time and abstracts the rest of the design. The technique for obtaining a "constraint slice" for each embedded Module Under Test (MUT) within a design is described in detail. The technique has been incorporated in an automated tool for designs described in Verilog, and results on large benchmark circuits show the significant benefits of the approach.

Static timing anaylsis sets the industry standard in the design methodology of high speed/performance microprocessors to determine whether timing requirements have been met. Unfortunately, not all the paths identified using such analysis can be sensitized. This leads to a pessimistic estimation of the processor speed. Also, no amount of engineering effort spent on optimizing such paths can improve the timing performance of the chip. In the past we demonstrated initial results of how ATPG techniques can be used to identify false paths efficiently. Due to the gap between the physical design on which the static timing analysis of the chip is bused and the test view on which the ATPG techniques are applied to identify false paths, in many cases only sections of some of the paths in the full-chip were analyzed in our initial results. In this paper, we will fully analyze all the timing paths using the ATPG techniques, thus overcoming the gap between the testing and timing analysis techniques. This enables us to do false path identification at the full-chip level of the circuit. Results of applying our technique to the second generation G4 PowerPC/sup TM/ will be presented.

We present a method for constructing concrete executions or witnesses to abstract behaviour specifications. The key concept is the use of an ordering on states which preserves containment of behaviours seen from the states. We present a modified depth-first search algorithm which uses the ordering to prune the requisite search paths and the memory needed for the history of the search. We apply the search to a model of a superscalar pipeline.