References


The following list is a collection of references I've gathered for my research and is meant to be a quick reference source for me and those with whom I collaborate.

Legend: document link = Link to online source, pdf available = I have a pdf copy.

Verifying Properties Using Sequential ATPG

Abraham, J. A., Vedula, V. M. & Saab, D. G. , , 2002.
Abstract: This paper develops a novel approach for formally verifying both safety and liveness properties of designs using sequential ATPG tools. The properties are automatically mapped into a monitor circuit with a target fault so that finding a test for the fault corresponds to formally establishing the property. The mapping of the properties to the monitor circuit is described in detail and the process is shown to be sound and complete. Experimental results show that the ATPG-based approach performs better than existing verification techniques, especially for large designs.
Keywords: hardware, formal verification, EDF

Co-Design and Refinement for Safety Critical Systems

Aljer, A. & Devienne, P. , DFT '04: Proceedings of the Defect and Fault Tolerance in VLSI Systems, 19th IEEE International Symposium on (DFT'04), 2004.
Abstract: In this paper we focus on design entry of complex systems, that is, the highest abstract tier of the global system without implementation choices to such and such technologies. At this very first level, the use of a formal specification language is more and more considered as the foundation of real validation process. What we would like to emphasize is that from a formal design entry, project management can be formally controlled by formal refinement. We propose an architecture that is based upon stepwise refinement of a formal model to achieve controllable implementations. This leads to implementations that are highly effective, but remain formally related to the first formal specification. Partitioning, fault tolerance, system management are seen as particular cases of refinement in order to conceptualize systems correct by proven construction. In this paper, we present the basic principles of system methodologies and describe the methodology based on the refinement paradigm. In order to prove this approach, we have developed the B-HDL Tool based on VHDL (digital circuits) and B Method (formal language based on set theory and logic). The benefits of such tools would be an amazing productivity gain, a better reuse automation and a formal redundancy management.
Keywords: hardware, requirements specification, refinement, Hardware_Spec_Valid

Synopsys Formality Support

Altera , , 2006.
Abstract: Formal verification of FPGA designs is gaining momentum as multi-million System-on-a-Chip (SoC) designs are targeted at FPGAs. Use the Formality software to easily verify logic equivalency between the RTL and DC FPGA post-synthesis netlist, and between the DC FPGA post-synthesis netlist and Quartus II post-place-and-route netlist. Beginning with version 4.2, the Quartus® II software interfaces with EDA tools including the Formality and DC FPGA software from Synopsys.
Keywords: hardware, formal verification, equivalence checking, EDF

Improvement of Fault Injection Techniques Based on VHDL Code Modification

Baraza, J. C., Gracia, J., Gil, D. & Gil, P. J. , Tenth IEEE International on HLDVT '05: Proceedings of the High-Level Design Validation and Test Workshop., 2005.
Abstract: Fault injection techniques based on the use of VHDL as design language offer important advantages with regard to other fault injection techniques. First, as they can be applied during the design phase of the system, they allow reducing the time-to-market. Second, this type of techniques presents high controllability and reachability. Among the different techniques, those based on the use of saboteurs and mutants are especially attractive due to their high capability of fault modeling. However, it is difficult to implement automatically these techniques in a fault injection tool, mainly the insertion of saboteurs and the generation of mutants. In this paper, we present new models of saboteurs and mutants that can be easily applicable in VFIT, a fault injection tool developed by the Fault-Tolerant Systems Research Group (GSTF) of the Technical University of Valencia.
Keywords: VHDL, hardware, verification, VHDL, ABV_Fault_Injection

Vhdl-Based Distributed Fault Simulation Using SAVANT

Baucom, R. J., DeLong, T. A., Smith, D. T. & Johnson, B. W. , Proceedings of the IEEE 1998 National Aerospace and Electronics Conference, 1998.
Keywords: hardware, VHDL, fault tolerant, ABV_Fault_Injection

Rulebase: An Industry-Oriented Formal Verification Tool

Beer, I., Ben-David, S., Eisner, C. & Landver, A. , DAC '96: Proceedings of the 33rd annual conference on Design automation, 1996.
Abstract: RuleBase is a formal verification tool, developed by the IBM Haifa Research Laboratory. It is the result of three years of experience in practical formal verification of hardware which, we believe, has been a key factor in bringing the tool to its current level of maturity. We present the tool, including several unique features, and summarize our usage experience.
Keywords: hardware, formal verification, EDF, rulebase, ABV

A Simplified Approach to Fault Tolerant State Machine Design for Single Event Upsets

Berg, M. , MAPLD, 2004.
Abstract: A simplified approach to fault tolerant state machine design starting from architectural development through synthesis will also be discussed. Examples of coding schemes that include additional logic for error detection and (in some cases) correction such as One Hot, Sequential, and Hamming will be examined. Due to the fact that users have run into roadblocks with synthesis tools “optimizing” away necessary logic for error handling, special attention will be given to the synthesis tools concerning the necessary techniques involved in producing the correct realization of functionality.
Comments: A look at how to properly design and code a finite state machine with fault-tolerance in mind.
Keywords: hardware, EDF

System Level Design and Verification Using a Synchronous Language

Berry, B., Kishinevsky, M. & Singh, S. , , 2003.
Abstract: Synchronous languages such as Esterel, Lustre, Signal, and others were originally developed for safety-critical embedded software and compiled into C. They have recently been extended to hardware with new language features and compilers to RTL. Contrary to traditional HDL languages (Verilog, VHDL) and recent system-level languages (SystemC, System Verilog), they have well defined formal semantics, which facilitate bug avoidance using correct-by-construction compilation and verification techniques. The tutorial will demonstrate what the synchronous language offers for the modeling, design, analysis and implementation of systems that comprise hardware and software. It will be based on Esterel. Esterel models have proved to be useful for rapid design space exploration and verification at system level, without resorting to detailed implementation and slow bit-level event-based simulation. We show how to model control-dominated IP blocks at a higher level of abstraction and how to use the target C code or RTL in conjunction with other system-level tools. Case studies include examples of design space exploration by synthesizing equivalent hardware or software from the same Esterel description, with formal verification of safety properties such as bus protocol conformance. We conclude with a review of future research directions.
Keywords: hardware, system-level, formal language, model-checking, validation, verification Hardware_Spec_Valid

Model-Based Development And The Implications To Design Assurance And Certification   document link

Bhatt, D., Hall, B., Dajani-Brown, S., Hickman, S. & Paulitsch, M. , Digital Avionics Systems Conference, 2005.
Abstract: The term "Model based design and development" has grown in popularity over the past decade. Within the embedded avionics community the term model based design implies the development and application of "control models and simulations" within tools such as MATLAB. At Honeywell, the authors have been engaged in model based development (MBD) and associated tools development for avionics applications. This position paper applies the lessons learned and discusses several issues, relating to sound model-based design, to meet design assurance and certification objectives. The paper examines the dominant approaches utilized by some of the popular model-based design, code generation and verification tool suites available commercially. It contrasts these approaches to traditional software design, implementation, and verification methods. This paper also recommends taking a broader perspective of MBD and suggests adopting lessons learned from the classical software engineering arena. We discuss this together with areas for future investigation, standardization, and automation tool development and integration.
Keywords: software, model-based, Hardware_Spec_Valid

Cost-efficient soft error protection for embedded microprocessors

Blome, J. A., Gupta, S., Feng, S. & Mahlke, S. , CASES '06: Proceedings of the 2006 international conference on Compilers, architecture and synthesis for embedded systems, 2006.
Abstract: Device scaling trends dramatically increase the susceptibility of microprocessors to soft errors. Further, mounting demand for embedded microprocessors in a wide array of safety critical applications, ranging from automobiles to pacemakers, compounds the importance of addressing the soft error problem. Historically, soft error tolerance techniques have been targeted mainly at high-end server markets, leading to solutions such as coarse-grained modular redundancy and redundant multithreading. However, these techniques tend to be prohibitively expensive to implement in the embedded design space. To address this problem, we first present a thorough analysis of the effects of soft errors on a production-grade, fully synthesized implementation of an ARM926EJ-S embedded microprocessor. We then leverage this analysis in the design of two orthogonal low-costs of terror protection techniques that can be tuned to achieve variable levels of fault coverage as a function of area and power constraints. The first technique uses a small cache of live register values in order to provide nearly twice the fault coverage of a register file protected using traditional error correcting codes at little or no additional area cost. The second technique is a statistical method used to significantly reduce the overhead of deploying time-delayed shadow latches for low-latency fault detection.
Comments: Has a good definition of SEUs.
Keywords: hardware, fault tolerant

Incorporating Effiecient Assertion Checkers into Hardware Emulation

Boule, M. & Zilic, Z. , Computer Design: VLSI in Computers and Processors, 2005. ICCD 2005. Proceedings. 2005 IEEE International Conference on, 2005.
Abstract: Assertion-based verification (ABV) is emerging as a paramount technique for industrial-strength hardware verification, especially through the emerging property specification language (PSL). Since PSL introduces significant overhead to simulators, in this paper we present the infrastructure for hardware emulation capable of supporting ABV. We develop a tool that generates hardware assertion checkers for inclusion into efficient circuit emulation. The MBAC checker generator is outlined, together with the algorithms for optimized assertion-circuit generation. Experiments show that MBAC outperforms the best known checker-generator.
Comments: Approach converts assertions in hardware monitors to verify a design during emulation.
Keywords: hardware, ABV, model-checking

Seven More Myths of Formal Methods

Bowen, J. P. & Hinchey, M. G. , , 1995.
Abstract: In 1990, Anthony Hall published a seminal article that listed and dispelled seven myths about the nature and application of formal methods. Today -- five years and many successful applications later -- formal methods remain one of the most contentious areas of software-engineering practice. Despite 25 years of use, few people understand exactly what formal methods are or how they are applied. Many nonformalists seem to believe that formal methods are merely an academic exercise -- a form of mental masturbation that has no relation to real-world problems. The media's portrayal of formal methods does little to help the situation. In many "popular press" science journals, formal methods are subjected to either deep criticism or, worse, extreme hyperbole. Fortunately, today these myths are held more by the public and the computer-science community at large than by system developers. It is our concern, however, that new myths are being propagated, and more alarmingly, are receiving a certain tacit acceptance from the system-development community.Following Hall's lead, we address and dispel seven new myths about formal methods: Formal methods delay the development process; formal methods lack tools; formal methods replace traditional engineering design methods; formal methods only apply to software; formal methods are unnecessary; formal methods are not supported; and formal-methods people always use formal methods.
Keywords: software, formal methods

The FSAP/NuSMV-SA Safety Analysis Platform

Bozzano, M. & Villafiorita, A. , , 2007.
Abstract: Safety-critical systems are becoming more complex, both in the type of functionality they provide and in the way they are demanded to interact with the environment. Such a growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, including analyzing the behavior of a system in degraded situations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complexity and are now being used more often. However, existing techniques have little tool support and therefore their use for safety analysis remains limited. In this paper, we present FSAP/NuSMV-SA, a platform which aims to improve the development cycle of complex systems by providing a uniform environment that can be used both at design time and for safety assessment. The platform makes the modeling and safety assessment of complex systems easier by providing a facility for automatically augmenting a system model with failure modes, whose definitions are retrieved from a predefined library. In this way, it is possible to assess the system safety both in nominal conditions and in user-specified degraded situations, i.e., in the presence of faults. Furthermore, the platform provides a pattern-based definition of temporal logic formulas, which simplifies the definition of safety requirements. The platform consists of a graphical user interface (FSAP) and an engine (NuSMV-SA) which is based on the NuSMV model checker. The model checking engine provides a support for system simulation and standard model checking capabilities, like property verification and the generation of counterexamples. Furthermore, algorithms have been implemented to automate the generation of artifacts that are typical of reliability analysis, e.g., fault trees. The platform can derive fault trees automatically (for both monotonic and non-monotonic systems) from the definition of the system model and of the possible faults. The interface of the platform has been designed to improve usability for people who are not expert in formal verification. The platform has been evaluated in collaboration with an industrial partner and tested on some industrial case studies.
Keywords: hardware, formal verification, model-checking, ABV_Fault_Injection

Improving System Reliability via Model Checking: the FSAP / NuSMV-SA Safety Analysis Platform

Bozzano, M. & Villafiorita, A. , In Proceedings of SAFECOMP 2003, 2003.
Keywords: hardware, FMEA, model-checking, ABV_Fault_Injection

No Silver Bullet: Essence And Accidents Of Software Engineering

Brooks, F. P. , , 1987.
Comments: Standard paper on Software Engineering
Keywords: software

Binary Decision Diagrams And Beyond: Enabling Technologies For Formal Verification

Bryant, R. E. , ICCAD '95: Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, 1995.
Abstract: Ordered Binary Decision Diagrams (OBDDs) have found widespread use in CAD applications such as formal verification, logic synthesis, and test generation. OBDDs represent Boolean functions in a form that is both canonical and compact for many practical cases. They can be generated and manipulated by efficient graph algorithms. Researchers have found that many tasks can be expressed as series of operations on Boolean functions, making them candidates for OBDD-based methods. The success of OBDDs has inspired efforts to improve their efficiency and to expand their range of applicability. Techniques have been discovered to make the representation more compact and to represent other classes of functions. This has led to improved performance on existing OBDD applications, as well as enabled new classes of problems to be solved. This paper provides an overview of the state of the art in graph-based function representations. We focus on several recent advances of particular importance for formal verification and other CAD applications.
Keywords: hardware, BDD, EDF

Formal Hardware Specification Languages For Protocol Compliance Verification

Bunker, A., Gopalakrishnan, G. & Mckee, S. A. , , 2004.
Abstract: The advent of the system-on-chip and intellectual property hardware design paradigms makes protocol compliance verification increasingly important to the success of a project. One of the central tools in any verification project is the modeling language, and we survey the field of candidate languages for protocol compliance verification, limiting our discussion to languages originally intended for hardware and software design and verification activities. We frame our comparison by first constructing a taxonomy of these languages, and then by discussing the applicability of each approach to the compliance verification problem. Each discussion includes a summary of the development of the language, an evaluation of the language's utility for our problem domain, and, where feasible, an example of how the language might be used to specify hardware protocols. Finally, we make some general observations regarding the languages considered.
Keywords: hardware, specification language, EDF

An Overview Of Formal Hardware Specification Languages

Bunker, A., McKee, S. A. & Gopalakrishnan, G. , Grace Hopper Celebration of Women in Computing, 2002.
Abstract: Verification is widely recognized as one of the most difficult aspects of computer hardware design. The gap between design and verification capabilities grows, as does the cost of missed flaws. Many researchers investigate ways to formally verify processor designs, interconnects, and protocols, but creating verification methods and tools will remain a central problem for computer scientists for at least the next decade. We introduce this field by surveying formal specification languages. We construct a taxonomy of languages and discuss the applicability of each to standard compliance verification, or demonstrating that a hardware design complies to an interconnect standard.
Keywords: hardware, specification language, EDF

Regression Testing: Gate-Level Functional Verification Is Imperative And Equivalence Checking Provides The Solution

Burgess, I. , , 2004.
Keywords: hardware, formal verification, equivalence checking, EDF

Essentials of Electronic Testing for Digital, Memory, and Mixed-Signal VLSI Circuits   document link

Bushnell, M. L. & Agrawal, V. D. , , 2002.
Keywords: hardware, verification, test generation, ABV_Fault_Injection

From VHDL Register Transfer Level to SystemC Transaction Level Modeling: A Comparative Case Study

Calazans, N., Moreno, E., Hessel, F., Rosa, V., Moraes, F. & Carara, E. , SBCCI '03: Proceedings of the 16th symposium on Integrated circuits and systems design, 2003.
Abstract: Transaction level (TL) modeling is regarded today as the next step in the direction of complex integrated circuits and systems design entry. This means that as this modeling level definition evolves, automated synthesis tools will increasingly support it, allowing design capture to start at a higher abstraction level than today. This work presents a comparison of traditional register transfer level (RTL) modeling and transaction level modeling through the implementation of a simple processor case study. SystemC is a language that naturally supports hardware transaction level descriptions. The R8 processor was described in SystemC TL and RTL versions and these were compared to an equivalent hand-coded VHDL RTL description in some key points, such as simulation efficiency and implementation results. The experiments indicate that TL descriptions present a faster path to system validation and that it is possible toenvisage the automation of the design flow from this level of abstraction without significant impact on the quality of the final implementation.
Keywords: hardware, systemc

Triple Module Redundancy Design Techniques for Virtex FPGAs

Carmichael, C. , , 2006.
Abstract: Triple Module Redundancy (TMR) combined with Single Event Upset (SEU) correction through partial reconfiguration is a powerful and effective SEU mitigation strategy. This method is only supported for the VirtexTM series of Xilinx FPGAs. Xilinx Application Note, XAPP216, describes the use of Readback and Partial Configuration for SEU detection and correction. This application note outlines the recommended design methodology for constructing and implementing TMR logic within the Virtex architecture.
Keywords: hardware, TMR

Streamline Verification Process With Formal Property Verification To Meet Highly Compressed Design Cycle

Chatterjee, P. , DAC '05: Proceedings of the 42nd Annual Conference on Design Automation, 2005.
Abstract: In this paper, I describe a methodology and tool flow for using formal verification effectively to reduce the verification burden in large custom ASIC designs.
Comments: A real-world example of the use of formal methods to meet time-to-market requirements.
Keywords: hardware, formal verification, EDF

A survey of fault tolerant methodologies for FPGAs

Cheatham, J. A., Emmert, J. M. & Baumgart, S. , , 2006.
Abstract: A wide range of fault tolerance methods for FPGAs have been proposed. Approaches range from simple architectural redundancy to fully on-line adaptive implementations. The applications of these methods also differ; some are used only for manufacturing yield enhancement, while others can be used in-system. This survey attempts to provide an overview of the current state of the art for fault tolerance in FPGAs. It is assumed that faults have been previously detected and diagnosed; the methods presented are targeted towards tolerating the faults. A detailed description of each method is presented. Where applicable, the methods are compared using common metrics. Results are summarized to present a succinct, comprehensive comparison of the different approaches.
Keywords: hardware, FPGA, fault tolerant

Fault Injection - A Method for Validating Computer-System Dependability

Clark, J. A. & Pradhan, D. K. , , 1995.
Abstract: A fault tolerant computer system's dependability must be validated to ensure that its redundancy has been correctly implemented and the system will provide the desired level of reliable service. Fault injection-the deliberate insertion of faults into an operational system to determine its response offers an effective solution to this problem. We survey several fault injection studies and discuss tools such as React (Reliable Architecture Characterization Tool) that facilitate its application.
Comments: Good discussion on the uses of fault injection.
Keywords: hardware, software, fault tolerant, fault injection, ABV_Fault_Injection

Early Hardware/Software Integration Using System 2.0

Connell, J. & Johnson, B. , , 2002.
Keywords: hardware, software, systemc

Trends and Challenges in VLSI Circuit Reliability

Constantinescu, C. , , 2003.
Abstract: Deep-submicron technology is having a significant impact on permanent, intermittent, and transient classes of faults. This article discusses the main trends and challenges in circuit reliability, and explains evolving techniques for dealing with them.
Comments: Good discussion on reliability challenges in ICs.
Keywords: hardware, fault tolerant, ABV_Fault_Injection

Impact of Deep Submicron Technology on Dependability of VLSI Circuits

Constantinescu, C. , , 2002.
Abstract: Advances in semiconductor technology have led to impressive performance gains of VLSI circuits, in general, and microprocessors, in particular. However, smaller transistor and interconnect dimensions, lower power voltages, and higher operating frequencies have contributed to increased rates of occurrence of transient and intermittent faults. We address the impact of deep submicron technology on permanent, transient and intermittent classes of faults, and discuss the main trends in circuit dependability. Two case studies exemplify this analysis. The first one deals with intermittent faults induced by manufacturing residuals. The second case study shows that transients generated by timing violations are capable of silently corrupting data. It is concluded that the semiconductor industry is approaching a new stage in the design and manufacturing of VLSI circuits. Fault-tolerance features, specific to custom designed computers, have to be integrated into commercial-off-the-shelf (COTS) VLSI systems in the future, in order to preserve data integrity and limit the impact of transient and intermittent faults.
Keywords: hardware, fault model, ABV_Fault_Injection

Assertion Based Verification Using HDVL

Datta, K. & Das, P. P. , VLSID '04: Proceedings of the 17th International Conference on VLSI Design, 2004.
Abstract: Over the past several years verification of largedesigns are becoming more and more complex - bothin terms of the maintaining the code size and inkeeping parity between the specification written inEnglish; design written in HDL (typically Verilog /VHDL) and the verification models written in HDL orsome proprietary verification language. To alleviate this problem, Accellera has come up with the proposalfor standardizing an HDVL - a single language that caters to all the needs for Design (as an HDL) as well as Verification (as an HVL - Hardware VerificationLanguage). SystemVerilog [6] standard where the user can model and verify the correctness of the designs using a unified language whose syntax and semantics is already proven and tested in the industry is being projected as a candidate HDVL. SystemVerilog is a set of major enhancements to the Verilog 2001[1] standard and these enhancements are taken from existing industry standard languages and paradigms including Superlog [3], PSL-Sugar [4], OVA [8] andOVL [7]. In this paper we present an overview of the Assertion based Verification methodology in general and explain, with suitable examples, how can one benefit from using an HDVL for the combined purpose of design as well as verification. It attempts to set the right expectations for an engineer from an HDVL and also illustrates the power of the new paradigm.
Comments: Basically describes ABV and why it is good.
Keywords: hardware, formal verification, specification, ABV Hardware_Spec_Valid

A Novel Fault Injection Technique for Behavioral-Level Modeling using VHDL

DeLong, T. A., Johnson, B. W. & Joseph A. Profeta, I. , VHDL International Users' Forum Fall Conference, 1994.
Abstract: A technique has been developed that allows for the injection of faults into a behavioral-level model of a component. The corruption of a VHDL signal (that is, the fault injection) is accomplished using a bus resolution function (BRF) and an additional process statement (the fault injection process). This process corrupts the VHDL signal based on information read from a text file. The file contains the time to start the fault injection, the time to end the fault injection, which signal to corrupt, and how to corrupt the signal (that is, which bits to stick at a 1, which bits to stick at a 0, and which bits are not affected). The process statement communicates this information to the BRF via additional fields defined for the signal. This technique has several advantages over other techniques. First, the technique is simulator independent since the fault injection is accomplished with standard VHDL features. Second, the technique uses standard VHDL types to perform the fault injection. Third, the fault injection experiment information is communicated to the simulation via text file I/O. Finally, this technique can be applied to existing models with minimal changes to the existing models.
Keywords: fault injection, hardware, ABV_Fault_Injection

A Fault Injection Technique for VHDL Behavioral-Level Models

Delong, T. A., Johnson, B. W. & Profeta, III, J. A. , , 1996.
Abstract: Fault injection is an important technique for the evaluation of design metrics such as reliability, safety, and fault coverage. Fault injection involves inserting faults into a system and monitoring the system to determine its behavior in response to the fault. Recently, designers are realizing the advantages of using simulation to perform fault injection on a model of the design, as opposed to performing the fault injection on the actual system. As designs become more complex, the need arises to perform fault injection at earlier stages in the design process, specifically at the behavioral level of abstraction where a functional description exists for the various components of the design, but the implementation details have not been developed.A technique has been developed that allows for the injection of faults into a Very High Speed Integrated Circuit (VHSIC) Hardware Description Language (VHDL) behavioral-level model. The corruption of a VHDL signal (the fault injection) is accomplished using a bus resolution function (BRF) and an additional process statement that performs the fault injection. This process corrupts the VHDL signal based on information read from a text file. The file contains the time to start the fault injection, the time to end the fault injection, which signal to corrupt, and how to corrupt the signal (for example, which bits to stick at a 1, which bits to stick at a 0, and which bits are not affected).This article outlines the implementation of the fault injection technique using VHDL and demonstrates the use of the technique to evaluate a design. In this case, the design is an embedded control system used to provide fail-safe operation in the railway industry. The article describes how the technique was used to evaluate the control system and provides the results obtained from the fault injection experiments performed on the control system.
Comments: Introduces a clever way to use bus resolution functions to inject faults in VHDL without requiring the VHDL to go through huge modifications. Faults are then injected during simulation.
Keywords: hardware, fault tolerant, verification, ABV_Fault_Injection

Fault Injection for Logic Synthesis Design using VHDL

Delong, T., Ghosh, A. K. & Johnson, B. W. , , .
Keywords: hardware, fault injection, ABV_Fault_Injection

Byzantine Fault Tolerance, from Theory to Reality

Driscoll, K., Hall, B., Sivencrona, H. & Zumsteg, P. , Computer Safety, Reliability, and Security, 2003.
Abstract: Since its introduction nearly 20 years ago, the Byzantine Generals Problem has been the subject of many papers having the scrutiny of the fault tolerance community. Numerous Byzantine tolerant algorithms and architectures have been proposed. However, this problem is not yet sufficiently understood by those who design, build, and maintain systems with high dependability requirements. Today, there are still many misconceptions relating to Byzantine failure, what makes a system vulnerable, and indeed the very nature and reality of Byzantine faults. This paper revisits the Byzantine problem from a practitioner's perspective. It has the intention to provide the reader with a working appreciation of the Byzantine failure from a practical as well as a theoretical perspective. A discussion of typical failure properties and the difficulties in preventing the associated failure propagation is presented. These are illustrated with real Byzantine failure observations. Finally, various architectural solutions to the Byzantine problem are presented.
Keywords: fault model, fault tolerant, ABV_Fault_Injection

Designing Safety-Critical Computer Systems

Dunn, W. R. , , 2003.
Abstract: The ubiquitous computer is the electronic component of choice for systemdevelopers, who increasingly exploit computing's power in safety-critical applications such as steer-by-wire automotive systems and powered prosthetics.However, these computer-based systems raise the ongoing concern that they might fail and cause harm. Exploring the systematic design of safety-critical computer systems helps to show how engineers canverify that these designs will be safe. Achieving risk reduction requires dealing with all the system’s components: hardware and software, sensors, effectors, the operator, and the primary source of harmfulenergy or toxicity—the application.
Comments: Good introductory article about hardware design for safety-critical systems.
Keywords: safety-critical, hardware design

Implementation of a SystemC Assertion Library   document link

Ecker, W. , , ~2005.
Abstract: Implementing advanced temporal assertions in SystemC is an error prone process due to the limited assertion capabilities of the class library. Current approaches focus on linking assertion languages such as PSL or SVA to SystemC code to overcome this restriction. However, linking other languages to SystemC to overcome some language deficiencies contradicts the purely object oriented class library approach, which was used for creating SystemC. Therefore we propose a native SystemC assertion library which is designed in a similar fashion to the OVL, in order to enable assertion based verification especially for system level designs and IP-integration verification in SystemC. Each assertion is implemented as a generic, fully parameterisable SystemC module for easy integration into any system design. It is our aim to provide each assertion implementation with a consistent structure containing the same parameters. Furthermore using SystemC as the implementation language for this library is compliant to the OSCI provided compiler simulator architectures and thus follows the open concept of SystemC.
Comments: This could be a way to introduce assertion-based verification techiniques into SystemC.
Keywords: hardware, systemc, ABV

Use Of Field Programmable Gate Array Technology In Future Space Avionics   document link

Ferguson, R. C. & Tate, R. , The 24th Digital Avionics Systems Conference, 2005. DASC 2005., 2005.
Abstract: The existence of hardware description languages (HDLs), the recent increase in performance, density and radiation tolerance of field programmable gate arrays (FPGAs), and intellectual property (IP) cores provides the technology for reprogrammable systems on a chip (SOC). This technology supports a paradigm better suited for NASA's vision. Hardware and software production are melded for more effective development; they can both evolve together over time. To investigate the flexibility of this technology, the core of the central processing unit and input/output processor of the space shuttle AP101S computer were prototyped in Verilog HDL and synthesized into an Altera Stratix FPGA.
Keywords: hardware, FPGA

Introducing The New Accellera Open Verification Library Standard   document link

Foster, H., Larsen, K. & Turpin, M. , ARM. DVCon, 2006.
Abstract: The new Accellera Open Verification Library (OVL) standard fulfills the long-anticipated vision of creating a vendor- and language-independent assertion library that can be leveraged across multiple verification processes. In this paper, we present the new Accellera OVL standard, which is a completely re-architected version of the original OVL that takes advantage of new features offered by the emerging PSL and SystemVerilog standards.
Keywords: hardware, ABV, EDF

Model Checking Early Requirements Specifications in Tropos

Fuxman, A., Mylopoulos, J., Pistore, M. & Traverso, P. , RE '01: Proceedings of the Fifth IEEE International Symposium on Requirements Engineering (RE '01), 2001.
Abstract: This paper describes an attempt to bridge the gap between early requirements specification and formal methods. In particular, we propose a new specification language, called Formal Tropos, that is founded on the primitive concepts of early requirements frameworks (actor, goal, strategic dependency) [15], but supplements them with a rich temporal specification language. We also extend existing formal analysis techniques, in particular model checking, to allow for an automatic verification of relevant proper-ties for an early requirements specification. Our preliminary experiments demonstrate that formal analysis reveals gaps and inconsistencies in early requirements that are by no means trivial to discover without the help of formal analysis tools.
Keywords: software, requirements validation, specification, Hardware_Spec_Valid

Behavioral-Level Fault Simulation

Ghosh, S. , , 1988.
Abstract: An approach to fault simulation is presented in which behavioral fault models represent complex failures in VLSI designs. Errors are deliberately introduced into the description of a design that contains no faults. These errors can be fault values of variables that represent state or timing parameters, a faulty description that is substituted for part of the good description, or a combination of these. The algorithm guarantees accurate results by deferring the output assignments. The approach can also be used to detect and discard inconsistent output assignments. The algorithm has been implemented in Stanford University's Sable simulator using the Adlib behavioral modeling language.
Keywords: fault location, behavioral fault models, fault simulation, hardware, fault model, ABV_Fault_Injection

Consistency Validation of High-Level Requirements

Gorse, N., Aboulhamid, E. M. & Savaria, Y. , IWSOC '04: Proceedings of the System-on-Chip for Real-Time Applications, 4th IEEE International Workshop on (IWSOC'04), 2004.
Abstract: The size of today's designs makes their validation very time consuming. To manage their complexity, an evolution towards higher levels of abstraction is mandatory. This paper addresses the automatic validation of high-level requirements. It presents an approach to cope with their modeling and conceptual validation. This methodology relies on the use of a very high level formal language for modeling requirements and on characterization of error patterns for their validation. It allows effective modeling and early detection of errors in hardware design cycles.
Keywords: hardware, requirements validation, Hardware_Spec_Valid

Automated Mapping Of Pre-Computed Module-Level Test Sequences To Processor Instructions

Gurumurthy, S., Vasudevan, S. & Abraham, J. A. , Test Conference, 2005. Proceedings. ITC 2005. IEEE International, 2005.
Abstract: Executing instructions from the cache has been shown to improve the defect coverage of real chips. However, although the faults detected by such tests can be determined, there has been no technique to target test generation for an undetected fault. This paper presents a novel technique to map pre-computed test sequences at the module level of a processor, to sequences of instructions. The module level pre-computed test sequence is translated into a temporal logic property and the negation of the property is passed to a bounded model checker. The model checker produces a counter-example for the temporal logic property. This counter-example trace contains the instruction sequence that can be applied at the primary inputs to produce the pre-computed test sequence at the module inputs. This technique has no restrictions on the type of test sequences, so it can be used to map test sequences for any kind of fault to processor instructions. It can also be used in the design phase to produce validation tests.
Keywords: hardware, formal verification, EDF

Seven Myths of Formal Methods

Hall, A. , , 1990.
Abstract: Seven widely held conceptions about formal methods are challenged. These beliefs are variants of the following: formal methods can guarantee that software is perfect; they work by proving that the programs are correct; only highly critical systems benefit from their use; they involve complex mathematics; they increase the cost of development; they are incomprehensible to clients; and nobody uses them for real projects. The arguments are based on the author's experiences. They address the bounds of formal methods, identify the central role of specifications in the development process, and cover education and training.
Keywords: software, formal methods

From Specification Validation to Hardware Testing: A Unified Method   document link

Hayek, G. A. & Robach, C. , Proceedings of the IEEE International Test Conference on Test and Design Validity, 1996.
Abstract: With the great advancement in the design automation field, actual tools allow to describe hardware systems as software programs using high-level hardware description languages such as VHDL or VERILOG. Consequently, a design fault which affects the system specification can be considered as a software fault. To test the system specification against (software) design faults, we propose in this paper an adaptation of the mutation analysis, originally proposed for software testing, to test VHDL functional descriptions. The resulted test set is applied on the gate-level structure of the system to measure its capacity to uncover hardware faults such as the stuck-at faults. Heuristics to enhance the test set in order to be sufficient for testing hardware faults are presented and results are compared to traditional ATPGs. Accordingly, this paper presents a unified method for testing both the system specification and the hardware implementation
Keywords: hardware, testing, Hardware_Spec_Valid

Using FormalPro for Xilinx Verification in a Synplify-Pro Flow

Henson, J. , , 2006.
Abstract: This document describes how to verify Xilinx FPGA designs using FormalPro. Specifically, the flow available in FormalPro is for Xilinx Virtex II designs implemented with Synplify-Pro and Xilinx ISE. You can use FormalPro to verify other families of Xilinx devices; however, this verification flow has been used primarily for designs targeted to Xilinx Virtex II.
Keywords: hardware, formal verification, equivalence checking, EDF

Using FormalPro for Xilinx Verification in a Precision RTL Flow

Henson, J. , , 2006.
Abstract: This document describes how to verify Xilinx FPGA designs using FormalPro. Specifically, the flow available in FormalPro is for Xilinx Virtex family designs implemented with Precision RTL and Xilinx ISE. You can use FormalPro to verify other families of Xilinx devices; however, this verification flow has been used primarily for designs targeted to Xilinx Virtex II.
Keywords: hardware, formal verification, equivalence checking, EDF

Decomposing Refinement Proofs Using Assume-Guarantee Reasoning

Henzinger, T. A., Qadeer, S. & Rajamani, S. K. , ICCAD '00: Proceedings of the 2000 IEEE/ACM international Conference on Computer-aided Design, 2000.
Abstract: Model-checking algorithms can be used to verify, formally and automatically, if a low-level description of a design conforms with a high-level description. However, for designs with very large state spaces, prior to the application of an algorithm, the refinement-checking task needs to be decomposed into subtasks of manageable complexity. It is natural to decompose the task following the component structure of the design. However, an individual component often does not satisfy its requirements unless the component is put into the right context, which constrains the inputs to the component. Thus, in order to verify each component individually, we need to make assumptions about its inputs, which are provided by the other components of the design. This reasoning is circular: component A is verified under the assumption that context B behaves correctly, and symmetrically, B is verified assuming the correctness of A. The assume-guarantee paradigm provides a systematic theory and methodology for ensuring the soundness of the circular style of postulating and discharging assumptions in component-based reasoning.We give a tutorial introduction to the assume-guarantee paradigm for decomposing refinement-checking tasks. To illustrate the method, we step in detail through the formal verification of a processor pipeline against an instruction set architecture. In this example, the verification of a three-stage pipeline is broken up into three subtasks, one for each stage of the pipeline.
Keywords: hardware, assume guarantee, model-checking, EDF

Refining Specifications To Programmable Logic

Hilton, A. & Hall, J. G. , Proceedings of REFINE 2002. Volume 30 of Electronic Notes in Theoretical Computer Science, 2002.
Keywords: hardware, software, specification, Hardware_Spec_Valid

On Applying Software Development Best Practice to FPGAs in Safety-Critical Systems   document link

Hilton, A. & Hall, J. G. , , 2000.
Keywords: hardware, software, specification, Hardware_Spec_Valid

FPGAs In Critical Hardware/Software Systems

Hilton, A. J. H. J. A. J., Townson, G. & Hall, J. G. , FPGA '03: Proceedings of the 2003 ACM/SIGDA eleventh international symposium on Field programmable gate arrays, 2003.
Abstract: FPGAs are being used in increasingly complex roles in critical systems, interacting with conventional critical software. Established safety standards require rigorous justification of safety and correctness of the conventional software in such systems. Newer standards now make similar requirements for safety-related electronic hardware, such as FPGAs, in these systems. In this paper we examine the current state-of-the-art in programming FPGAs, and their use in conventional (low-criticality) hardware/software systems. We discuss the impact that the safety standards requirements have on the co-development of hardware/software combinations in critical systems and suggest adaptations of existing best practice in software development that could discharge them. We pay particular attention to the development and analysis of high-level language programs for FPGAs designed to interact with conventional software.
Keywords: hardware, software, specification, Hardware_Spec_Valid

Automatic Verification Of Implementations Of Large Circuits Againsthdl Specifications

Hoskote, Y. V., Abraham, J. A., Fussell, D. S. & Moondanos, J. , , 1997.
Abstract: This paper addresses the problem of verifying the correctness of gate-level implementations of large synchronous sequential circuits with respect to their higher level specifications in a hardware description language (HDL). The verification strategy is to verify containment of the finite state machine (FSM) represented by the HDL description in the gate-level FSM by computing pairs of compatible states. This formulation of the verification problem dissociates the verification process from the specification of initial states, whose encoding may be unknown or obscured during optimization and also enables verification of reset circuitry. To make verification of large circuits with merged data path and control tractable, the concept of strong containment is introduced. This is a conservative approach which exploits correspondence between data path-registers in the two descriptions without requiring any correspondence between the control units. We also present an important result and associated proof that computation of pairs of equivalent or compatible states can be achieved by considering subsets of the circuit outputs. Consequently, verification of circuits with large and diverse input-output sets, which was previously intractable due to lack of a single effective variable order for the binary decision diagrams (BDD's), is now feasible. Experimental results are presented for the verification of several industry level circuits.
Keywords: hardware, formal verification, EDF

Fault Injection Techniques and Tools   document link

Hsueh, M., Tsai, T. K. & Iyer, R. K. , , 1997.
Abstract: Dependability evaluation involves the study of failures and errors. The destructive nature of a crash and long error latency make it difficult to identify the causes of failures in the operational environment. It is particularly hard to recreate a failure scenario for a large, complex system. To identify and understand potential failures, the authors use an experiment-based approach for studying system dependability. This approach is applied during the conception, design, prototype, and operational phases. To take an experiment-based approach, you must first understand a system's architecture, structure, and behavior. You need to know its tolerance for faults and failures, including its built-in detection and recovery mechanisms,and you need specific instruments and tools to inject faults, create failures or errors, and monitor their effects. Engineers most often use low-cost, simulation-based fault injection to evaluate the dependability of a system that is in the conceptual and design phases. At this point, the system under study is only a series of high-level abstractions; implementation details have yet to be determined. Thus the system is simulated on the basis of simplified assumptions. Simulation-based fault injection, which assumes that errors or failures occur according to predetermined distribution, is useful for evaluating the effectiveness of fault-tolerant mechanisms and a system's dependability; it does provide timely feedback to system engineers. However, it requires accurate input parameters, which are difficult to supply: Design and technology changes often complicate the use of past measurements. Testing a prototype, on the other hand, allows you to evaluate the system without any assumptions about system design. Instead of injecting faults, engineers can directly measure operational systems as they handle real workloads.Measurement-based analysis uses actual data, which contains much information about naturally occurring errors and failures and sometimes about recovery attempts. Although these three experimental methods have limitations, their unique values complement one another and allow for a wide spectrum of dependability studies.
Comments: Good source for an intro to Fault Injection
Keywords: hardware, software, fault injection, fault tolerant, ABV_Fault_Injection

Formal Hardware Verification With Bdds: An Introduction

Hu, A. J. , IEEE Pacific Rim Conference on Communications, Computers and Signal Processing (PACRIM), 1997.
Keywords: hardware, BDD, equivalence checking, EDF

A Comparative Study of Modeling at Different Levels of Abstraction in System on Chip Designs: A Case Study

Jayadevappa, S., Shankar, R. & Mahgoub, I. , , 2004.
Abstract: Abstraction is a powerful technique for the design and implementation of complex systems. A model developed at a higher level of abstraction allows one to tackle complexity by initially hiding the details and elaborating them later. A higher level of abstraction typically has a positive effect on the simulation speed and ease of development of the model, but could affect the accuracy of the model developed. In this paper, we study the effect of model abstraction of a peripheral device developed at a higher level of abstraction using SystemC, and at the register transfer level using Verilog. The parameters compared are accuracy, simulation speed, flexibility, time to develop, code length and ease of verification. In our study we show that by raising the level of abstraction, one not only achieves better simulation speed, flexibility, ease of verification but also reduces time to develop and shorten code length. All this is achieved while being able to maintain almost the same accuracy.
Comments: Compares Verilog to SystemC and shows that design at a higher level has many advantages.
Keywords: hardware, systemc

Fault Injection into VHDL Models: the MEFISTO Tool

Jenn, E., Arlat, J., Rimbn, M., Ohlsson, J. & Karlsson, J. , Twenty-Fourth International Symposium on Fault-Tolerant Computing, 1994.
Abstract: This paper focuses on the integration of the fault injection methodology within the design process of fault-tolerant systems. Due to its wide spectrum of application and hierarchical features, VHDL has been selected as the simulation language to support such an integration. Suitable techniques for injecting faults into VHDL models are identified and depicted. Then, the main features of the MEFISTO environment aimed at supporting these techniques are described. Finally, some preliminary results obtained with MEFISTO are presented and analyzed.
Comments: Fault injection during VHDL simulation. Includes modifying VHDL (sabators and mutants) and using bus resolution functions.
Keywords: hardware, fault tolerant, fault injection, verification, ABV_Fault_Injection

Formal Verification of the Pentium 4 Multiplier

Kaivola, R. & Narasimhan, N. , , 2001.
Abstract: We present the formal verification of the floating-point multiplier in the Intel IA-32 Pentium 4 microprocessor. The verification is based on a combination of theorem-proving and model-checking tasks performed in the Forte hardware verification environment. The tasks are tightly integrated to accomplish complete verification of the multiplier hardware coupled with the rounder logic. The approach does not rely on specialized representations like Binary Moment Diagrams or its variants.
Keywords: hardware, formal verification, model-checking, theorem proving, EDF

Emerging Verification Methods for Complex Hardware in Avionics

Karlsson, K. & Forsberg, H. , The 24th Digital Avionics Systems Conference, 2005. DASC 2005, 2005.
Abstract: During the last ten years, there has been a tremendous increase in the ability to design complex electronic hardware. However, the ability to verify correctness of complex hardware has not redoubled in the same manner. Therefore, the industry faces a test/cost problem where verification and testing represents the larger part of development expenses. This is particularly true for the highest design assurance levels (levels A and B) in avionics. If, for instance, programmed logic devices are used at these assurance levels and no additional design assurance strategies are used, tests and deterministic analysis must demonstrate correct operation under all combinations and permutations of conditions down to the gate level of the device.

This paper discusses the additional design assurance strategies stated in RTCA/DO-254 [1], Appendix B - “Design assurance considerations for level A and level B functions.” In particular, we address the use of formal specification languages such as the Property Specification Language (PSL) in combination with dynamic (simulation) and static (formal) verification methods for programmed logic devices. Using these methods, we suggest a design assurance strategy for complex programmable airborne electronics compliant with the guidelines of RTCA/DO-254. The strategy is a semi-formal solution, a hybrid of static and dynamic assertion based verification.
Comments: This paper present identical arguments to our approach with EDF. They provide a pretty good design flow that includes static and dynamic ABV and also relate it to DO-254 standards.
Keywords: hardware, formal verification, ABV equivalence, checking, EDF

Characterization of Soft Errors Caused by Single Event Upsets in CMOS Processes

Karnik, T., Hazucha, P. & Patel, J. , , 2004.
Abstract: Radiation-induced single event upsets (SEUs) pose a major challenge for the design of memories and logic circuits in high-performance microprocessors in technologies beyond 90nm. Historically, we have considered power-performance-area trade offs. There is a need to include the soft error rate (SER) as another design parameter. In this paper, we present radiation particle interactions with silicon, charge collection effects, soft errors, and their effect on VLSI circuits. We also discuss the impact of SEUs on system reliability. We describe an accelerated measurement of SERs using a high-intensity neutron beam, the characterization of SERs in sequential logic cells, and technology scaling trends. Finally, some directions for future research are given.
Comments: Good description of the history of SEU research.
Keywords: SEU, hardware, ABV_Fault_Injection

Formal Verification In Hardware Design: A Survey

Kern, C. & Greenstreet, M. R. , , 1999.
Abstract: In recent years, formal methods have emerged as an alternative approach to ensuring the quality and correctness of hardware designs, overcoming some of the limitations of traditional validation techniques such as simulation and testing. There are two main aspects to the application of formal methods in a design process: the formal framework used to specify desired properties of a design and the verification techniques and tools used to reason about the relationship between a specification and a corresponding implementation. We survey a variety of frameworks and techniques proposed in the literature and applied to actual designs. The specification frameworks we describe include temporal logics, predicate logic, abstraction and refinement, as well as containment between &ohgr;-regular languages. The verification techniques presented include model checking, automata-theoretic techniques, automated theorem proving, and approaches that integrate the above methods. In order to provide insight into the scope and limitations of currently available techniques, we present a selection of case studies where formal methods were applied to industrial-scale designs, such as microprocessors, floating-point hardware, protocols, memory subsystems, and communications hardware.
Comments: An in-debth paper on the formal hardware verification.
Keywords: hardware, formal verification, EDF

Evaluating coverage of error detection logic for soft errors using formal methods

Krautz, U., Pflanz, M., Jacobi, C., Tast, H. W., Weber, K. & Vierhaus, H. T. , DATE '06: Proceedings of the conference on Design, automation and test in Europe, 2006.
Abstract: In this paper we describe a methodology to measure exactly the quality of fault-tolerant designs by combining fault-injection in high level design (HLD) descriptions with a formal verification approach. We utilize BDD based symbolic simulation to determine the coverage of online error-detection and - correction logic. We describe an easily portable approach, which can be applied to a wide variety of multi-GHz industrial designs.
Comments: This methodology is very similar in concept to ABVFI.
Keywords: formal verification, fault injection, ABV_Fault_Injection

A Framework For Object Oriented Hardware Specification, Verification, And Synthesis

Kuhn, T., Oppold, T., Winterholer, M., Rosenstiel, W., Edwards, M. & Kashai, Y. , DAC '01: Proceedings of the 38th conference on Design automation, 2001.
Abstract: We describe two things. First, we present a uniform framework for object oriented specification and verification of hardware. For this purpose the object oriented language “e” is introduced along with a powerful run-time environment that enables the designer to perform the verification task. Second, we present an object oriented synthesis that enhances “e” and its dedicated run-time environment into a framework for specification, verification, and synthesis. The usability of our approach is demonstrated by real-world examples.
Keywords: hardware, specification language, verification, Hardware_Spec_Valid

Formal Verification of Hardware: Misconception and Reality

Kumar, R. , WESCON/98, 1998.
Abstract: Formal verification in hardware, is a novel technique for validating the functional correctness of designs through the various phases of the design process, starting from the first specification. Simulation, the present industrial standard tool for verification, relies on propagating a set of input test vectors through the design and manually observing the validity of the outputs corresponding to the inputs. In contrast, formal verification does not require any input vectors and at the same time guarantees 100% correctness. The idea behind the formal verification engines is to use mathematical techniques to exercise all possible inputs and automatically check for outputs that are not in order. The use of formal verification for equivalence checking, especially at the lower levels of abstraction, is of real advantage. In spite of the various informalities which creep into the verification process it is definitely a boon for coping with the complexity of today's design. However, giant strides need to be taken by the FV tool vendors in developing an adequate environment for performing sequential equivalence checking and property checking on large industrial designs.
Keywords: hardware, formal verification, EDF

Object-Oriented Techniques in Hardware Design   document link

Kumar, S., Aylor, J. H., Johnson, B. W. & Wulf, W. A. , , 1994.
Abstract: We focus on using object-oriented techniques to improve the hardware design process. The advantages of these techniques for hardware design include: improved modifiability and maintainability of models; easy component instantiation with different parameters; quick composition of new components; the ability to identify and reuse common components; the ability to tailor general-purpose components to more specialized components; support of dynamic object creation and destruction; and the possibility of employing existing software synthesis and verification techniques. We illustrate the application of object-oriented techniques using a load-store, reduced instruction-set processor that contains a local memory. The instruction set consists of 22 instructions, which require one or two 16-bit words. Arithmetic is performed in two's complement. We use C++ to demonstrate the usefulness of object-oriented techniques, not to provide arguments for or against its use in hardware modeling and design.
Keywords: hardware, language, Hardware_Spec_Valid

A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance

Kupferman, O., Li, W. & Seshia, S. A. , Proceedings FMCAD, 2008.
Abstract: The quality of formal specifications and the circuits they are written for can be evaluated through sanity checks such as vacuity and coverage. Both checks involve mutations to the specification or the circuit implementation. We study and prove properties of mutations on finite-state systems. Since faults can be viewed as mutations, our theory of mutations can be used in a formal approach to fault injection. We demonstrate theoretically and with experimental results how relations and orders amongst mutations can be used to improve specifications and reason about coverage of fault tolerant circuits.
Keywords: formal verification, fault injection, model-checking, ABV_Fault_Injection

Safeware: System Safety and Computers

Leveson, N. G. , , 1995.
Comments: Common example of a safety system failure due to design faults.
Keywords: software, safety-critical

A New Approach for Early Dependability Evaluation Based on Formal Property Checking and Controlled Mutations

Leveugle, R. , IOLTS '05: Proceedings of the 11th IEEE International On-Line Testing Symposium, 2005.
Abstract: The interest for early analyses of the functional impact of faults in a circuit is growing, due to the increasing probability of transient faults. However, experiments are often very long, especially when spatial and temporal multiplicity have to be taken into account in the fault model. Formal property checking is an appealing approach to perform comprehensive functional validations but is intended to validate properties only in nominal operation, not after a fault has occurred. This paper proposes a new approach combining formal property checking and the generation of specific circuit mutants to achieve efficient early identification of unacceptable effects of multiplefaults.
Comments: This methodology is very similar to ABVFI
Keywords: formal verification, fault injection, model-checking, ABV, ABV_Fault_Injection

ARIANE 5 Flight 501 Failure Report by the Inquiry Board

Lions, J. , , 1996.
Abstract: On 4 June 1996, the maiden flight of the Ariane 5 launcher ended in a failure. Only about 40 seconds after initiation of the flight sequence, at an altitude of about 3700 m, the launcher veered off its flight path, broke up and exploded. Engineers from the Ariane 5 project teams of CNES and Industry immediately started to investigate the failure.
Comments: The Ariane 5 failure has become a classic example of how incomplete software specifications caused the complete failure of the launch vehicle. In this case the software function that calculates the tragetory failed when a 64-bit floating point number was converted to a 16-bit integer. The nubmer was too big to fit into a 16-bit integer and an exception was thrown. Both the main and backup computers shutdown due to this.
Keywords: software, safety-critical

Fault-Tolerant Computing: An Introduction

Meyer, J. F. & Rault, J. , , 1979.
Comments: Gives an overview of early fault tolerant computing approaches.
Keywords: fault tolerant

Functional Validation of Programmable Architectures

Mishra, P. & Dutt, N. , DSD '04: Proceedings of the Digital System Design, EUROMICRO Systems on (DSD'04), 2004.
Abstract: Validation of programmable architectures, consisting of processor cores, coprocessors, and memory subsystems, is one of the major bottlenecks in current System-on-Chip design methodology. A critical challenge in validation of such systems is the lack of a golden reference model. Traditional validation techniques employ different reference models depending on the abstraction level and verification task (e.g., functional simulation or property checking), resulting in potential inconsistencies between multiple reference models. This paper presents a validation methodology that uses an Architecture Description Language (ADL) based specification as a golden reference model for validation of programmable architectures, and generation of executable models such as simulators and hardware prototypes. We present a validation framework that uses the generated hardware as a reference model to verify the hand-written implementation using a combination ofsymbolic simulation and equivalence checking. We also present functional coverage based test generation techniques for validation of pipelined processor architectures. Finally, the generated simulator and hardware models are also used for early exploration of programmable architectures.
Keywords: hardware, specification, verification, language, Hardware_Spec_Valid

Measuring Architectural Vulnerability Factors

Mukherjee, S. S., Weaver, C. T., Emer, J., Reinhardt, S. K. & Austin, T. , , 2003.
Abstract: Processor designers need accurate estimates of soft-error rates early in the design cycle to make appropriate cost-reliability tradeoffs. Here, the authors present a method for estimating the architectural vulnerability factor—the probability that a fault in a particular structure will result in an error.
Keywords: hardware, fault tolerant

The Byzantine Hardware Fault Model

Nanya, T. & Goosen, H. A. , , 1989.
Keywords: hardware, digital circuits, error correction, error detection, failure analysis, fault tolerant computing, logic design, logic testing, system recovery, transients, Byzantine hardware fault model, concurrent error checking circuits, logic design techniques, short transient, temporary failures, ABV_Fault_Injection

On the Use of Model Checking for the Verification of a Dynamic Signature Monitoring Approach

Nicolescu, B., Gorse, N., Savaria, Y., Aboulhamid, E. M. & Velazco, R. , IEEE Transactions on Nuclear Science, 2005.
Abstract: Consequences of transient faults represent a significant problem for today's electronic circuits and systems. As the probability of such errors increases, incorporation of error detection and correction mechanisms is mandatory. It is well known that traditional techniques that validate system's reliability do not cover the whole spectrum of fault scenarios, because fault models are linked to target architectures. Therefore, validating the completeness of robust fault tolerance techniques is a major issue when assessing reliability improvements these techniques can produce. In this paper, we propose an original approach to evaluate the system reliability with respect to Single Event Upset (SEU) errors. It is based on model-checking principles. In addition, a signature analysis technique is evaluated. This technique was previously validated using a simulation-based fault injection approach. Simulation results showed that no error escapes detection. However, simulation based fault injection cannot guarantee that all fault consequences have been investigated. This limitation motivates us to explore a formal verification approach that targets a complete validation. Model checking has a fundamental advantage over classic fault-injection techniques: it can cover all possible SEU fault scenarios from a predefined class. Results reported in this paper demonstrate the efficiency of this validation approach over usual simulation-based techniques.
Comments: The authors of this paper investigate a fault tolerant approach to protecting the control flow of a process by using signature checking. The SPIN model checking tool was used to verify that their approach works for all fault scenarios.
Keywords: hardware, formal verification, model-checking, ABV_Fault_Injection

Formal Verification - A Viable Alternative To Simulation?

Nordstrom, A. , , 1996.
Abstract: Functional validation and regression simulations constitute a large part of the entire ASIC design process and schedule. The drive to decrease time to market has resulted in pressure to reduce total simulation times. Formal verification addresses the schedule problem by eliminating the need for regression simulations. The paper investigates whether formal verification is a viable alternative to regression simulations for functional verification in a Verilog based design flow. The investigative methods were based on applying formal verification on all steps in the verification process. It is concluded that regression simulations can be mostly replaced by formal verification.
Keywords: hardware, formal verification, EDF

New Techniques for Accelerating Fault Injection in VHDL Descriptions

Parrotta, B., Rebaudengo, M., Reorda, M. S. & Violante, M. , IOLTW '00: Proceedings of the 6th IEEE International On-Line Testing Workshop (IOLTW), 2000.
Abstract: Simulation-based Fault Injection in VHDL descriptions is increasingly common due to the popularity of top-down design flows exploiting this language. However, the large CPU time required to perform VHDL simulations often represents a major drawback stemming from the adoption of this method. This paper presents some techniques for reducing the time to perform the Fault Injection experiments. Static and dynamic methods are proposed to analyze the list of faults to be injected, and for removing faults as soon as their behavior is known. Common features available in most VHDL simulation environments are also exploited. Experimental results show that the proposed techniques are able to reduce the time required by a typical Fault Injection campaign by a factor ranging from 51% to 96%.
Comments: Deals with reducing the simulation time required for simulation fault injection by analyzing the nubmer and types of faults that need to be investigated.
Keywords: hardware, fault tolerant, ABV_Fault_Injection

Formal Analysis Of Hardware Requirements

Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R. & Cimatti, A. , DAC '06: Proceedings of the 43rd annual conference on Design automation, 2006.
Abstract: Formal languages are increasingly used to describe the functional requirements (specifications) of circuits. These requirements are used as a means to communicate design intent and as basis for verification. In both settings it is of utmost importance that the specifications are of high quality. However, formal requirements are seldom the object of validation, even though they can be hard to understand and interactions between them can be subtle. In this paper we present techniques and guidelines to explore and assure the quality of a formal specification. We define a technique to interactively explore the semantics of a specification by simulating its behavior for user-defined scenarios. Further-more, we define techniques to automatically check specifications against a set of user-provided assertions, which must be satisfied, and a set of possibilities, which must not be conradicted. The proposed techniques support the user in the iterative development and refinement of high-quality specifications.
Keywords: hardware, validation, specification, requirements, formal, Hardware_Spec_Valid

A Highly Flexible Hardened RTL Processor Core Based on LEON2

Portolan, M. & Leveugle, R. , , 2006.
Abstract: We present a hardened RTL processor core based on Leon2. Modifications are done at RT-level to achieve high configurability in an early stage of the development process. The main parts of the processor core can be protected against Single Event Upsets and Single Event Transients. Results and tradeoffs are presented and discussed.
Comments: May be a good resource for when I look at the Leon3.
Keywords: hardware, fault tolerant, leon2, ABV_Fault_Injection

Fault-Tolerant Computing

Rennels, D. , , .
Comments: Overview of fault tolerant computing.
Keywords: fault tolerant

Fault-Tolerant Computing - Concepts and Examples

Rennels, D. A. , , 1984.
Comments: Gives a historical overview of fault tolerant computing.
Keywords: fault tolerant

Formal Verification Based On Assume And Guarantee Approach - A Case Study (Short Paper)

Roy, S. K., Iwashita, H. & Nakata, T. , ASP-DAC '00: Proceedings of the 2000 conference on Asia South Pacific design automation, 2000.
Abstract: In this paper, we present a verification case study of the Audio Output Interface (AOF) subsystem based on a compositional verification approach known as the Assume-Guarantee approach. We illustrate how designers can leverage their detailed knowledge of a design to partition it at the module level, and, thereby, enable the Assume-Guarantee approach to overcome intrinsic limitations of a formal verification tool to successfully verify large designs
Keywords: hardware, assume guarantee, formal verification, EDF

An Industrially Effective Environment For Formal Hardware Verification   document link

Seger, C. H., Jones, R. B., O'Learly, J. W., Melham, T., Aagaard, M. D., Barrett, C. & Syme, D. , , 2005.
Abstract: The Forte formal verification environment for datapath-dominated hardware is described. Forte has proven to be effective in large-scale industrial trials and combines an efficient linear-time logic model-checking algorithm, namely the symbolic trajectory evaluation (STE), with lightweight theorem proving in higher-order logic. These are tightly integrated in a general-purpose functional programming language, which both allows the system to be easily customized and at the same time serves as a specification language. The design philosophy behind Forte is presented and the elements of the verification methodology that make it effective in practice are also described.
Keywords: hardware, model-checking, theorem proving, EDF

Formal Verification of a System-on-Chip Using Computation Slicing

Sen, A., Garg, V. K., Abraham, J. A. & Bhadra, J. , ITC '04: Proceedings of the International Test Conference on International Test Conference, 2004.
Abstract: 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.
Keywords: hardware, formal verification, EDF

Verification-guided soft error resilience

Seshia, S. A., Li, W. & Mitra, S. , DATE '07: Proceedings of the conference on Design, automation and test in Europe, 2007.
Abstract: Algorithmic techniques for formal verification can be used not just for bug-finding, but also to estimate vulnerability to reliability problems and to reduce overheads of circuit mechanisms for error resilience. We demonstrate this idea of verification-guided error resilience in the context of soft errors in latches. We show how model checking can be used to identify latches in a circuit that must be protected in order that the circuit satisfies a formal specification. Experimental results on a Verilog implementation of the ESA SpaceWire communication protocol indicate that the power overhead of soft error protection can be reduced by a factor of 4.35 by using our approach rather than protecting all latches.
Comments: This methodology is very similar to ABVFI.
Keywords: formal verification, fault injection, model-checking, ABV_Fault_Injection

Using Formal Specifications for Functional Validation of Hardware Designs

Shimizu, K. & Dill, D. L. , , 2002.
Abstract: Many of today's digital circuit designs depend on the tight integration of multiple design modules. These modules, designed by different engineers, interact via an interface, such as a bus or IP core interface. The interface is of utmost importance because it is where the various designers' conceptions come together. If designers do not uniformly interpret the interface specification, modules will not meld together easily or will behave incorrectly when connected.Therefore, the interface protocols must be clearly defined so that the designers can view the expected module behavior consistently. Furthermore, the protocol must be thoroughly debugged because so much of the module design depends on it.
Keywords: hardware, ABV, EDF

An Introduction to Formal Verification

Shukla, S. K. , , .
Comments: A presentation that gives an introduction to the methodologies behind equivalence checking and model checking. Includes some simple examples.
Keywords: hardware, formal verification, EDF

VHDL Modelling Guidelines

Sinander, P. , , 1994.
Keywords: hardware, VHDL

Assesment of Safety Critical Systems Incorporating Application Specific Integrated Circuits

Smith, D. T., DeLong, T. A., Johnson, B. & Lach, J. , , 2003.
Keywords: hardware, fault models, EDF, ABV_Fault_Injection

Design Guidelines for Optimal Results in FPGAs

Stephenson, J. , , 2005.
Abstract: Design practices have an enormous impact on an FPGA design’s timing performance, logic utilization, and system reliability. Good design practices also aid in successful design migration between FPGA and ASIC implementations for both prototyping and production. Poor design practices can lead to low performance, high logic or resource utilization, and unstable or unreliable designs associated with increased verification time. With FPGA applications increasing in complexity and performance, good design practices are becoming an increasingly important factor in successful designs. This paper discusses how to obtain optimal results for FPGA designs and ASIC migrations by understanding the impact of synchronous design practices, following recommended design techniques, and targeting advanced FPGA architectural features.
Keywords: hardware, EDF

The Engineering Roles of Requirements and Specification

Strunk, E. A., Furia, C. A., Rossi, M., Knight, J. C. & Mandrioli, D. , , 2007.
Abstract: The distinction between requirements and specification in software engineering is often confused in practice. This obstructs the system validation process, because it is unclear what exactly should be validated, and against what it should be validated. The reference model of Gunter et al. addresses this difficulty by providing a framework within which requirements can be distinguished from specification. It separates world phenomena (those of the requirements) from machine phenomena (those of the specification). However, it does not explain how the characterization can be used in practice to help assure system validity. In this paper, we enhance the reference model of Gunter et al. to account for certain key elements that are necessary for the link between requirements and specification. We use the

enhanced version to present a more refined picture of validity, where validation has two steps that can be undertaken separately. We use this picture to question whether the “what the system will do, not how it will do it” paradigm is a useful one in describing how to construct a specification, and propose an alternative. Finally, we present the requirements and specification we developed for an illustrative example based on a runway incursion prevention system, with 2 the ArchiTRIO formal language in a UML-like environment, to show how this might be done in

practical systems.
Comments: The application of this to Hardware may be a good PhD dissertation topic.
Keywords: software, requirements specification, Hardware_Spec_Valid

An Introduction to System-Level Modeling in SystemC 2.0   document link

Swan, S. , , 2003.
Abstract: SystemC is a new modeling language based on C++ that is intended to enable system level design and IP exchange. This tutorial paper briefly reviews the hardware modeling features available in SystemC 1.0 and then introduces the new system level modeling features in SystemC 2.0. A small design example is presented that demonstrates how the new features facilitate system level design tasks such as communication refinement and mapping of design specifications to hardware and software implementations. Also discussed is how the new modeling features enable a wide variety of models of computation to be cleanly expressed within SystemC.
Comments: Great introductory paper. Has good examples that are readable and show the power of SystemC.
Keywords: hardware, system-level, systemc, Hardware_Spec_Valid

Automatic Assume Guarantee Analysis For Assertion-Based Formal Verification

Wang, D. & Levitt, J. , ASP-DAC '05: Proceedings of the 2005 conference on Asia South Pacific design automation, 2005.
Abstract: Assertion based verification encourages the insertion of many assertions into a design. Typically, not all assertions can be proven (or falsified). The indeterminate assertions require manual analysis in order to determine design correctness - a time-consuming and error-prone process. This paper shows how automatic assume guarantee reasoning can be used to reduce the amount of manual analysis. We present algorithms to automatically compute the assume guarantee relations between assertions. We extend circular assume guarantee reasoning to compute more proofs. And, we show how automatic assume guarantee reasoning can be used in practice to reduce the number of indeterminate assertions requiring manual analysis. We present the results of applying our algorithms to large industrial designs.
Keywords: hardware, assume guarantee, EDF

Examining ACE Analysis Reliability Estimates Using Fault-Injection

Wang, N. J., Mahesri, A. & Patel, S. J. , ISCA '07: Proceedings of the 34th Annual International Symposium on Computer Architecture, 2007.
Abstract: ACE analysis is a technique to provide an early reliability estimate for microprocessors. ACE analysis couples data from abstract performance models with low level design details to identify and rule out transient faults that will not cause incorrect execution. While many transient faults are analyzable in ACE analysis frameworks, some are not. As a result, ACE analysis is conservative and provides a lower bound for the reliability of a processor design. Bounding the reliability of a design is useful since it can guarantee that the given design will meet reliability goals.

In this work, we quantify and identify the sources of ACE analysis conservatism by comparing an ACE analysis methodology against a rigorous fault-injection study. We evaluate two flavors of ACE analysis: a "simple" analysis and a refined analysis, finding that even the refined analysis overestimates the soft error vulnerability of an instruction scheduler by 2-3x. The conservatism stems from two key sources: from lack of detail in abstract performance models and from what we term Y-Bits, a result of the single-pass simulation methodology that is typical of ACE analysis. We also examine the efficacy of applying ACE analysis to a class of "partial coverage" error mitigation techniques. In particular, we perform a case study on one such technique and extrapolate our findings to others.
Keywords: hardware, verification, ABV_Fault_Injection

A Specifier's Introduction to Formal Methods

Wing, J. M. , , 1990.
Abstract: Formal methods used in developing computer systems (i.e. mathematically based techniques for describing system properties) are defined, and their role is delineated. Formal specification languages, which provide the formal method's mathematical basis, are examined. Certain pragmatic concerns about formal methods and their users, uses, and characteristics are discussed. Six well-known or commonly used formal methods are illustrated by simple examples. They are Z, VDM, Larch, temporal logic, CSP, and transition axioms.
Keywords: hardware, specification language, EDF

Using the Virtex Delay-Locked Loop

XAPP132 , , 2006.
Abstract: The Virtex™ FPGA series offers up to eight fully digital dedicated on-chip Delay-Locked Loop (DLL) circuits providing zero propagation delay, low clock skew between output clock signals distributed throughout the device, and advanced clock domain control. These dedicated DLLs can be used to implement several circuits, which improve and simplify system-level design.
Keywords: hardware, clocking, EDF

Dependability Analysis Using a Fault Injection Tool Based on Synthesizability of HDL Models

Zarandi, H. R., Miremadi, S. G. & Ejlali, A. , DFT '03: Proceedings of the 18th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, 2003.
Abstract: This paper presents a fault injection tool, called SINJECT that supports several synthesizable and non-synthesizable fault models for dependability analysis of digital systems modeled by popular HDLs. The tool provides injection of transient and permanent faults into the Verilog as well as VHDL models of a digital circuit to study the fault behavior, fault propagation and fault coverage. Moreover, using specific simulators, the SINJECT provides a mixed-mode fault injection, i.e., fault injection into both Verilog and VHDL parts of a model, to achieve high description reality by Verilog and high capability modeling by VHDL. To demonstrate the tool, two case studies are evaluated: 1) an arithmetic processor with a non-synthesizable Verilog model, called ARP and 2) a VHDL model of 32-bit processor with a synthesizable ALU, called DP32. The results show that depending on the fault injection points in the ARP, the effects of faults were significantly different, while in the case of DP32, the fault coverage varied between 51 to 56 percent of total fault injected.
Keywords: hardware, VHDL, fault tolerant, verification, ABV_Fault_Injection

Benchmarking SAT Solvers for Bounded Model Checking

Zarpas, E. , In Proc. SAT’05, number 3569 in LNCS, 2005.
Abstract: Modern SAT solvers are highly dependent on heuristics. Therefore, benchmarking is of prime importance in evaluating the performances of different solvers. However, relevant benchmarking is not necessarily straightforward. We present our experiments using the IBM CNF Benchmark on several SAT solvers. Using the results, we attempt to define guidelines for a relevant benchmarking methodology, using SAT solvers for real life BMC applications.
Keywords: formal verification, benchmarks, ABV_Fault_Injection

Creating Safe State Machines

Zhang, S. Z. , , 2002.
Abstract: Finite state machines are widely used in digital circuit designs. Generally, when designing a state machine using an HDL, the synthesis tools will optimize away all states that cannot be reached and generate a highly optimized circuit. Sometimes, however, the optimization is not acceptable. For example, if the circuit powers up in an invalid state, or the circuit is in an extreme working environment and a glitch sends it into an undesired state, the circuit may never get back to its normal operating condition. This paper discuses a general methodology when creating a state machine using the HDL Designer SeriesTM State Diagram Editor. You can specify the design so that synthesis tools will not optimize away those unused states, thus a “safe” state machine can be generated.
Keywords: hardware, EDF

A Novel Collaborative Scheme Of Simulation And Model Checking For Property Verification   document link

Zhu, M., Bian, J. & Wu, W. , Computer Supported Cooperative Work in Design, 2004. Proceedings. The 8th International Conference on, 2004.
Abstract: A collaborative scheme for verifying classified properties of a design is proposed. These properties are classified for three verification techniques, i.e. module logic simulation, BDD (binary decision diagram) based model checking and CDFG (control data flow graph) matching. The cooperative process is performed on a refined model from CDFG structure and three interactive methods are employed to complete the verification. The optimization techniques, BDD variables reordering and property grouping are discussed and examined. This collaborative scheme is implemented on the benchmarks ITC99, which demonstrates its validity and practicality.
Keywords: hardware, model-checking, EDF

Fault Injection Techniques and Tools for Embedded Systems Reliability Evaluation

, , 2003.
Keywords: hardware, software, fault injection, ABV_Fault_Injection