System and method for formal fault propagation analysis
A system and method for formulating a sequential equivalency problem for fault (non)propagation with minimal circuit logic duplication by leveraging information about the location and nature of a fault. The system and method further apply formal checking to safety diagnoses and efficiently models simple and complex transient faults.
1. A computer-implemented method for performing a sequential equivalency check for analysis of fault propagation, the method comprising:
injecting a fault;
identifying, among a plurality of registers, a first set of registers in which the injected fault cannot propagate and a second set of registers in which the injected fault can propagate;
wherein, for each register of the plurality of registers, the identification comprises running an update function and assigning the register to the second set of registers when the register changes as a result of the update function and assigning the register to the first set when the register does not change as a result of the update function; and
duplicating the second set of registers to derive a reduced stated duplication for performing equivalence checking.
2. The computer-implemented method of claim 1 , wherein the identifying of the first set of registers and the second set of registers comprises a combinatorial check, wherein the update function is checked for each register.
3. The computer-implemented method of claim 1 , wherein the identifying comprises a sequential check in one clock cycle.
4. The computer-implemented method of claim 1 , wherein the injecting, the identifying, and the duplicating are iterative and repeated.
5. The computer-implemented method of claim 1 , wherein the fault is injected using transient fault modelling.
6. The computer-implemented method of claim 1 , wherein the assigning of the register to the first set of registers or to the second set of registers is performed for a fixed number of clock cycles after running the update function, and
wherein the fixed number of clock cycles is greater than one.
7. The computer-implemented method of claim 1 , used for detection of faults not needing further checking, wherein fault propagations that happen after an error is detected/diagnosed are considered safe or faults not needing further checking.