Browsing by Subject "Computer systems--Verification"

Now showing 1 - 3 of 3

Automatic generation of instruction sequences for software-based self-test of processors and systems-on-a-chip
(2008-05) Gurumurthy, Sankaranarayanan; Abraham, Jacob A.
At-speed functional tests are an important part of the manufacturing test flow of processors. With delay defects becoming more common due to the properties of the newer process technologies, at-speed functional tests have become indispensable. Traditionally, functional tests needed expensive automatic testing equipment due to the memory and speed requirements associated. This cost issue was solved by native-mode testing which uses the intelligence of the processor to test itself. In the native-mode self-test (also known as software-based self-test) paradigm, instruction sequences are loaded into the cache to test the processor for defects. Generally, only random instructions are used in nativemode tests. As with any random sequence based testing, there are faults that are left undetected by random instructions. Manual effort is necessary to generate the tests that can detect those faults, requiring a detailed knowledge of the instruction set architecture and the micro-architecture of the processor. We propose an automatic technique that alleviates the need for such manual effort. Our technique has a hierarchical approach. We use traditional automatic test pattern generation (ATPG) algorithms for generating tests at the local level (module or combinational blocks). These tests are mapped to instructions at the global level using a verification engine. We also have feedback between these two levels for more efficient testing. We demonstrate the technique on a publicly available processor. We then enhance the technique to test an entire system-on-a-chip (SOC). A typical SOC has an embedded processor. We use this embedded processor to test the other blocks in the SOC. In general, most of these blocks are designed by the design reuse methodology. Therefore, these blocks may be available only as black-boxes. Our technique is well suited to test such blocks. We use existing test vectors for the core and present a technique that generates instruction sequences that when executed by the processor generates the given vectors at the boundaries of the blocks. We designed an SOC using an ARM core and a publicly available encryption core and experimented on it to demonstrate the effectiveness of our technique.
High level static analysis of system descriptions for taming verification complexity
(2007-12) Vasudevan, Shobha; Abraham, Jacob A.
The growing complexity of VLSI and System-on-a-chip(SoC) designs has made their verification extremely expensive, time-consuming and resource intensive. Formal verification of system behavior is critical to the design cycle due to its ability to isolate subtle flaws and provide high quality assurance. However, its computational intractability limits applicability in practice, rendering the state-of-the-art insufficient to meet the needs of the industry. In this dissertation, a suite of techniques that are a significant departure from traditional Boolean level approaches to formal verification are presented. The algorithms are based on a top-down, domain-aware perspective of the system by reasoning at the system level and register transfer level (RTL) descriptions. Static analysis of these high level system descriptions using structural information and symbolic reasoning leads to effective decomposition strategies that create tractable portions of the system. These manageable system components can then be verified by deploying efficient Boolean level algorithms. The techniques presented here apply to the actual RTL source code, and are intended to blend seamlessly into the system design cycle. All approaches using high level static analyis follow a three pronged solution- domain aware analysis, high level symbolic simulation and a decision procedure for the verification task. This work advocates a marked difference in the perspective to formal hardware verification as compared to popular paradigms. The techniques shown here are illustrative of a hardware-aware viewpoint to verification, and argue this case for contemporary verification tasks. Antecedent conditioned slicing, an abstraction technique for reducing RTL design space is introduced. The reduced RTL can then be model checked. An open source RTL implementation of the USB 2.0 protocol is verified using this technique. A technique for pipelined processor verification using antecedent conditioned slicing is introduced. An open source Verilog RTL of OR1200, an embedded processor is explained in a detailed case study for verification using this technique. A static analysis technique is proposed to alleviate the complexity of the sequential equivalence checking problem between system level and RTL descriptions, by efficiently decomposing designs using sequential compare points. A satisfiability (SAT) solver is used as the lower level verification engine. In a case study, sequential equivalence checking between a system level description of a Viterbi decoder and two different RTL implementations are detailed.
Mechanical verification of reactive systems
(2001-08) Manolios, Panagiotis; Moore, J Strother, 1947-