SYSTEM AND METHOD FOR FORMAL CIRCUIT VERIFICATION

Abstract

A system and computer-implemented method for calculation and display of a fault propagation path. The method identifies with a computing device a fault location in an electrical circuit under test, identifies with the computing device an observation point in the electrical circuit under test, computes with the computing device a fault path from the fault location to the observation point, and displays in a waveform viewer all signals in the fault path from the fault location to the observation point in order of their creation.

Claims

1. A computer-implemented method for calculation and display of a fault propagation path comprising: identifying with a computing device a fault location in an electrical circuit; identifying with said computing device an observation point in the electrical circuit; computing with said computing device a fault path from said fault location to said observation point; and displaying in a waveform viewer all signals in said fault path from said fault location to said observation point in order of their creation.

2. A computer-implemented method for calculation and display of a fault propagation path according to claim 1, wherein the step of computing a fault path comprises: computing the shortest path of impacted signals from the fault location to the observation point.

3. A computer-implemented method for calculation and display of a fault propagation path according to claim 2, wherein the step of computing the shortest fault path comprises: computing the shortest path in terms of the number of signals.

4. A computer-implemented method for calculation and display of a fault propagation path according to claim 2, wherein the step of computing the shortest fault path comprises: computing the shortest path in terms of the number of instances.

5. A computer-implemented method for calculation and display of a fault propagation path according to claim 2, wherein the step of computing the shortest fault path comprises: computing the shortest path in terms of the number of registers.

6. A computer-implemented method for calculation and display of a fault propagation path according to claim 2, wherein the step of computing the fault path further comprises: adding a deviation or alteration to the shortest path.

7. A computer-implemented method for calculation and display of a fault propagation path according to claim 1, wherein the step of computing a fault path comprises: a. entering an observation point in a current signal list; b. comparing each signal on the current signal list with an impacted signal list; c. for each compared signal, if the signal is not on the impacted signal list, doing nothing with respect to that signal; d. for each compared signal, if the signal is on the impacted signal list, checking if the signal is the fault location; e. for each compared signal on the impacted signal list, if the signal is the fault location skipping to step h; f. for each compared signal on the impacted signal list, if the signal is not the fault location adding the fanin signals of the signal to a next current signal list and storing the signal as the parent of the added fanin signals; g. making the next current signal list the current signal list and returning to step b; h. setting the fault locations at the path signal; i. determining if the path signal has a parent signal; j. if the path signal has a parent signal, using the parent a new path signal, storing the new path signal in a path list, and returning to step i for the new path signal; k. if the path signal does not have a parent signal, outputting the path of impacted signals as the shortest fault path to the waveform viewer.

8. A computer-implemented method for calculation and display of a fault propagation path according to claim 1, wherein the step of displaying in a waveform viewer all signals in said fault path from said fault location to said observation point in order of their creation comprises: displaying the signals in the timing domain, in a stepladder in a different color in the display to show how the fault moves forward from one signal to the next.

9. A computer-implemented method for calculation and display of a fault propagation path according to claim 1, wherein the step of displaying in a waveform viewer all signals in said fault path from said fault location to said observation point in order of their creation comprises using visual indicators including at least one of different color, different line thickness or different type of line or any other visual indicator.

10. A computer-implemented method for calculation and display of a fault propagation path comprising: identifying with a computing device a fault location in an electrical circuit; identifying with said computing device a plurality of observation points in the electrical circuit; computing with said computing device fault paths from said fault location to at least two of said plurality of observation points; and displaying in a waveform viewer all signals in said computed fault paths from said fault location to said at least two of said plurality of observation points in order of their creation.

Description

BRIEF DESCRIPTION OF THE DRAWINGS

[0039] For a more complete understanding of the present invention and the advantages thereof, reference is now made to the following description and the accompanying drawings, in which:

[0040] FIG. 1 is a diagram illustrating various types of faults that may occur in a safety critical system and exemplary results of such faults.

[0041] FIG. 2 is a diagram illustrating a general safety critical system having a hardware safety mechanism.

[0042] FIG. 3 is a system architecture diagram of a system for analyzing and displaying fault propagation in accordance with a preferred embodiment of the present invention.

[0043] FIG. 4 is a flow chart of a method for analyzing and displaying fault propagation in accordance with a preferred embodiment of the present invention.

[0044] FIG. 5 is an illustration of a display of a system for analyzing and displaying fault propagation in accordance with a preferred embodiment of the present invention.

[0045] FIG. 6 is a flow diagram illustrating signal flow through a system for analyzing and displaying fault propagation in accordance with a preferred embodiment of the present invention.

[0046] FIG. 7 is a diagram illustrating a fault path calculation in accordance with a preferred embodiment of the present invention.

[0047] FIG. 8 is a flow diagram of a method for computing a fault path in accordance with a preferred embodiment of the present invention.

DETAILED DESCRIPTION OF THE PREFERRED EMBODIMENTS

[0048] Hardware safety mechanisms are necessary to guarantee determinist SoC behavior in the event of random faults. Typically, implementing hardware safety mechanisms involves some form of redundant logic that does not directly contribute to the implementation of the circuit's mission function. In the presence of faults, this logic becomes truly active and is responsible to detect, possibly correct, and report these faults to relevant part of the system. Functional verification planning, tracking and execution of both mission and safety functions is critical to meet the strict demands of safety standards. Key aspects in the verification of safety functions are that they (1) do not interfere with the hardware functionality under normal operation, (2) detect faults and correctly route information (alarm, fault corrected, etc.) to the relevant part of the system and (3) improve system availability by correcting the effect of some faults.

[0049] Safety mechanisms bring another dimension to the already complex and time-consuming task of functional verification. There are countless fault scenarios to examine and engineers often need a dedicated test environment to handle fault injection, related checkers, and coverage data.

[0050] A general architecture for a system and method for analyzing and displaying fault propagation path in accordance with a preferred embodiment of the present invention is shown in FIG. 3. The system includes a computing device 300, which may be a computer or server having one or more processors, a memory and a non-transitory storage medium such as a hard drive or solid state drive. The computing device 300 has a fault injection module 310, a fault propagation module 320, a fault detection module 330, and a waveform debugger 340. The computing device may have other modules or applications such as a verification module 350 or a Quantifying module 360. The system further has a display 200. The fault injection module or application 310 provides a simple and flexible interface to define and inject fault scenarios, with no need to change the design, go through complex code-instrumentation steps, or develop a dedicated verification environment.

[0051] Fault propagation analysis comprises the injection of faults into the gate level models of integrated circuits during verification to prove that faults will be detected by a safety mechanism. These gate level models can be complex and contain numerous possible fault scenarios. In order to satisfy hardware safety goals, the number of dangerous non-detected faults must be minimized.

[0052] Fault simulation is a standard approach to determine fault metrics. Faults are stimulated and propagated to observation points, to ensure detection by a safety function. Any faults not activated or not propagated by the functional stimulus consume a high proportion of the simulation cycles. They are also difficult to debug when considering stimulus improvements. Thus these faults often remain in the not detected group, detracting from the desired detection ratio.

[0053] A fault scenario can be seen as a set of faulty variants of the original design, the design under test (DUT). The first element of a fault scenario is the set of bit-level design signals where faults shall be injected. The other elements define when and which types of faults shall be injected. The original design corresponds to the particular fault scenario of no faults being present.

[0054] Users have the flexibility of defining custom fault scenarios, or pick predefined ones. A simple scenario could describe the injection of stuck-at-0 faults on all bits of a number of design signals, all the time. A custom scenario could describe the injection of a SEU fault, e.g. a bit-flip, in an arbitrary bit of a memory location, occurring only once and coinciding with some other condition, for example a memory read on a specific address. User assertions can be associated with specific fault scenarios, and powerful proof strategies are automatically setup to handle the simultaneous exhaustive verification of huge fault populations in large and complex designs. Moreover, dedicated debug features speed up the daunting task of examining assertion failures on fault-injected designs, where things can get quite confusing. Finally, the quantify module can measure the coverage of the overall set of assertions at the push of a button and expose both mission and safety-related functional areas that have verification gaps.

[0055] Faults can be classified as propagatable and non-propagatable. Non-propagatable faults can never lead to a malfunction of the system regardless of its state. Hence they are safe and can be removed from the dangerous fault list, improving the fault metric. This is where formal technology can be effectively applied in an automated way using the Fault Propagation Module 320. The Fault Propagation Module 320 automatically identifies non-propagatable faults, allowing their safe elimination prior to simulation, thereby cutting on simulation and debug time while increasing the nominal fault coverage Any know method for identifying non-propagatable faults may be used.

[0056] The Fault Propagation Module 320 is applied to the overall fault population both prior to and after fault simulation. The Fault Propagation Module 320 has a fast mode and a deep mode. Operating in a fast mode the Fault Propagation Module 320 is run pre-simulation, utilizing formal analysis to efficiently identify non-propagatable faults, thereby enabling the desired fault detection ratio to be rapidly achieved while avoiding unnecessary effort. These faults may be pruned from the fault list without the requirement for fault simulation test vectors. The entire fault-simulation process is significantly accelerated through the removal of this class of faults from those that need to be run in fault simulation.

[0057] Operating in a deep mode the Fault Propagation Module 320 can be used to analyze non-propagatable faults identified during a simulation-based fault injection process to either improve the safety mechanism or to classify them as safe. This automated step greatly reduces the manual effort required post-fault simulation to identify any remaining dangerous faults. The analysis is accomplished without modification of the netlista requirement of the certification standards.

[0058] The only required input is a gate or RTL model for the circuit under test. The system identifies fault locations where it already performs optimizations such as net collapsing to avoid duplications. Alternatively, a fault list or design areas of interest indication may be provided, which is used by the tool to refine the fault list.

[0059] Furthermore, an initial design state may be loaded to allow a context analysis. Such an analysis can be important to understand how faults behave when injected at a certain execution time.

[0060] After fault list creation, the system performs a fully automated formal analysis to identify non-propagatable faults. After the analysis, the non-propagatable, as well as the potentially propagatable faults can be written into a simple CSV formatted text file for further processing. In addition, an analysis summary report is generated. A fast statistical analysis may also be performed where the fault list is sampled rather than analyzing all faults.

[0061] In the method of a preferred embodiment of the present invention, as shown in FIG. 4, the system identifies 410 a fault location for injecting a fault and identifies 420 an observation point. The observation point in the circuit design is a point where errors can have a dangerous impact. The system computes 430 the fault path (explained later in further details with reference to FIGS. 7 and 8). The system then opens 440 a viewer in the waveform debugger 340. The system 300 then displays 450 on the display 200 an impacted signal path in an ordered list from the fault location to the observation point whereby each signal inside the past has been impacted by the fault. Impacted refers to the value in the design between different than what the value would be in a golden design. In alternative embodiments, a plurality of observation points may be used, for example, if the fault propagates to more than one observation point.

[0062] As shown in FIG. 5, only one waveform is shown for a given signal. The impacted signals are shown in a different color (e.g., red) than the non-impacted signals. Indicators other than color, such as line thickness, type of line (e.g., dashed, dotted, etc.), markings on the lines (e.g., x's, *'s, etc.) or any other visual indicator, may be used. Preferably, the signals are shown in a different color only when the value of the golden and faulty signal is different. Also, as an alternative to the display shown in FIG. 5, the values of the golden and fault signals could be placed next to each other onto a given single wave. Displaying two values can be particular useful when the displayed signal is not a single bit. The signals are displayed in the timing domain, which results in a stepladder in a different color showing host the fault moves forward from one signal to the next. Different colors may be used in the display to show how the fault moves forward from one signal to the next. As also shown in FIG. 5, it may be beneficial to display the inputs of the device before the signal and the outputs of the device after the signal. In the alternate embodiment having multiple observation points, data and graphs for a plurality of observation points can be shown on the display or waveform viewer.

[0063] An exemplary architecture 600 for verification of hardware safety mechanisms is shown in FIG. 6. The system has a parity encoder 610, read/write 620, write pointer 630, memory 640, read pointer 650, parity coder 660 and full/empty 670.

[0064] As shown in FIG. 7, the inputs for the fault path calculation 700 are start point (fault location) and end point (observation point), a list of signals that were impacted by the fault as calculated from a counterexample (the complete list of impacted signals), and the fanin/fanout relation of each single signal in the design. The output of the fault path calculation is the shortest path from the start point to the end point. The shortest path can be in terms of the number of signals, the number of instances or a number of registers/states. Instances can have different numbers of signals attached to them. An instance is typically a cell (like an AND call or FlipFlop cell). The shortest path from the start point to the end point may not be the absolute shortest path but may include any deviations or alterations between the start point and the end point. Deviations or alterations may added by any means such as FlipFlop and the like.

[0065] An exemplary method for computing a fault path in accordance with a preferred embodiment of the present invention is described with reference to FIG. 8. The inputs for the calculation are shown in FIG. 7. An Observation Point is entered into a Current Signal List at 802. If this is the first iteration, the Current Signal List may have only one signal (the Observation Point). If it is a later iteration, the Current Signal List will have a plurality of signals. At 810, if the Current Signal List is empty, the system knows there is an error and appropriate error notification is undertaken at step 812. If the Current Signal List is not empty at 810, the system determines at 820 for each signal in the Current Signal List whether that signal is on the Impacted Signal List. If a particular signal is not on the Impacted Signal List, the system does nothing at 822 with respect to that signal. If a particular signal is on the Impacted Signal List, the system checks at 830 whether the signal is the Fault Location. If it is not the Fault Location, the system adds the fanin of this signal to a Next Current Signal List and stores the signal as the parent of those fanin signals at 834. Once all signals on the Current Signal List have been checked, the system makes the Next Current Signal List the Current Signal List at 836 and then returns to 810. If a signal is the fault location at step 830, the system sets the fault location as the path signal at 840. The system than determines at 850 whether the path signal has a parent. If yes, the system sues that parent as a new Path Signal and stores that Path Signal in the Path List at 852. The system then returns to step 850. If the Path Signal does not have a parent, the system displays the path in creation order in a waveform viewer at 860. In this way, the shortest path from the fault location to the observation point is determined and displayed.

[0066] The foregoing description of the preferred embodiment of the invention has been presented for purposes of illustration and description. It is not intended to be exhaustive or to limit the invention to the precise form disclosed, and modifications and variations are possible in light of the above teachings or may be acquired from practice of the invention. The embodiment was chosen and described in order to explain the principles of the invention and its practical application to enable one skilled in the art to utilize the invention in various embodiments as are suited to the particular use contemplated. It is intended that the scope of the invention be defined by the claims appended hereto, and their equivalents. The entirety of each of the aforementioned documents is incorporated by reference herein.