Fault Model
ConceptA fault model in microprocessor and system verification is the explicit set of fault hypotheses that a testing or generation technique is designed to expose or instantiate. Evidence describes fault models across several contexts: model-based test generation from EXPRESSION specifications (with SMV as model checker), OSM-based pipeline modeling, template-based generation (Genesys-Pro, MicroTESK), random generation (RAVEN), constraint-solving test data generation (HOL-TestGen, VAMP case study), stuck-at faults in circuit-level mutation testing, GPU/DNN reliability evaluation (neutron beam fault models, ECC effects, complex fault injection vs single-bit flips), and System-of-Systems contract-based fault modelling.
First seen 5/26/2026
Last seen 6/22/2026
Evidence 5 chunks
Wiki v2
WIKI
Overview
A fault model in the evidence is the explicit set of fault hypotheses that a generation or testing technique is designed to expose or instantiate. The hypothesis can be hardware-level (e.g., single and double bit flips, stuck-at faults, complex multi-bit faults induced by neutron irradiation), microarchitecture-level (e.g., register, operation, pipeline-path, and inter-operation errors), or interaction-level (e.g., contract-level faults in Systems of Systems). [C1][C2][C3][C4][C8][C9]
Fault models in directed, model-based generation
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
5 connectionsStuck-at-fault is a specific type of fault model used in testing.
RAVEN uses fault models to generate test programs.
Model-based generation uses fault models to describe typical errors.
An Approach to Test Programs Generation for Microprocessors Based on Pipeline Hazards Templates ← uses 75% 1e
Related work uses fault models; the paper discusses this in context of related approaches.
The Mishra-Dutt approach requires the test developer to define a fault model.
LINKED ENTITIES
2 linksCITATIONS
10 sources10 citations — click to expand
[1] Directed test program generation translates EXPRESSION specifications into SMV and uses a fault model describing typical errors for registers, individual operations, pipeline paths, and interactions between several operations; for each fault-model element, concrete properties are generated and covered by SMV counterexamples, but the technique does not scale on complex designs. MicroTESK: An Extendable Framework for
[2] In the related work, a generic structure–behaviour SMV model is derived from an EXPRESSION specification; the test developer defines a fault model; for each fault-model element the negation of the corresponding property is produced and a counterexample is generated by the SMV model checker; model checking does not scale on complex designs, so template-based generation is used as an addition. An Approach to Test Programs Generation for Microprocessors Based on Pipeline Hazards Templates
[3] Pipeline structure can be specified as an Operation State Machine (OSM) with operational and hardware levels, where tokens represent resources and the goal of testing is to traverse all transitions of the joint automaton; this approach, like EXPRESSION/SMV, relies on accurate specifications and applies best in late design stages. An Approach to Test Programs Generation for Microprocessors Based on Pipeline Hazards Templates
[4] Genesys-Pro (IBM Research) is composed of an architecture-independent engine and an architecture-specific model; verification engineers develop templates specifying structure and properties of test programs, and Genesys-Pro transforms them into executable tests; the template-based technique requires more effort but scales better than the model-checking approach. An Approach to Test Programs Generation for Microprocessors Based on Pipeline Hazards Templates
[5] In the MicroTESK survey, random generation (including RAVEN, which combines randomization with knowledge of common microprocessor faults), combinatorial enumeration of short instruction sequences (as in the first version of MicroTESK), and template-based generation (the core of MicroTESK) are described as alternative test-program generation strategies whose fault assumptions differ from those of model-based methods. MicroTESK: An Extendable Framework for
[6] HOL-TestGen's VAMP case study uses constraint solving and random instantiation for test data generation, which yields coarsely grained memory access and an underlying fault model described as somewhat arcane (interferences of operations in distant memory areas); for such faults a denser test method is recommended, and additional constraints (address-range bounding, used-predicate linking store- and load-address sets, sub-domain partitioning) refine the implicit fault model. Test Program Generation for a Microprocessor: A Case Study
[7] Stuck-at-fault analysis is described as a white-box mutation technique that uses the structure of the implementation under test; mutators are introduced to capture a fabrication fault model such as broken wires between gates, and the resulting equivalence-class tests are effective for medium-size circuits but cannot reveal some design-level flaws (e.g., write–read errors influenced by byte alignments in memory). Test Program Generation for a Microprocessor: A Case Study
[8] Although a VAMP gate-level model was available, the case study stayed at the design level of the VAMP; the equivalence classes underlying the tests could be refined further by exploring byte- or bit-level representations of registers and memory cells, instead of relying on a coarse hypothesis such as one successful write–read standing for all write–reads in a memory cell. Test Program Generation for a Microprocessor: A Case Study
[9] Software-level fault injection on GPUs running DNNs may produce unrealistic results because it has limited access to hardware resources and adopts naive fault models (single and double bit flips); physical neutron-beam injection gives realistic error rates but lacks fault-propagation visibility; combining both yields a DNN fault model with critical-error rates up to 61% where ECC is ineffective, and YOLOv3 misdetection rates under complex fault models derived from RTL simulations match beam-experiment rates and are 8.66× higher than single-bit-flip injection rates. Characterizing a Neutron-Induced Fault Model for Deep Neural Networks
[10] Existing contractual specifications for constituent systems of Systems of Systems do not provide explicit consideration for faults; the paper extends an existing contract-modelling pattern with fault modelling concepts, instantiated on an Audio Visual SoS case study from Bang and Olufsen. Fault Modelling in System-of-Systems Contracts