Soft error verification in hardware designs

Soft error detection is performed by computation of states based on formal methods and by simulating a synthesized target identification logic together with the design. Soft errors may be simulated in response to detecting that a simulated state of the design is comprised by the states. A BDD representation of the design may be utilized to determine the states. A Boolean satisfiability problem may be defined and solved using an all-SAT solver in order to determine the states.

BACKGROUND

The present disclosure relates to error detection in hardware designs in general, and to detection of errors caused due to soft errors that were not handled properly, in particular.

Computerized devices are an important part of the modern life. They control almost every aspect of our life—from writing documents to controlling traffic lights. However, computerized devices are bug-prone, and thus require a verification phase in which the bugs should be discovered. The verification phase is considered one of the most difficult tasks in developing a computerized device. Many developers of computerized devices invest a significant portion, such as 70%, of the development cycle to discover erroneous behaviors of the computerized device, also referred to as a target computerized system. The target computerized system may comprise hardware, software, firmware, a combination thereof and the like. In some cases, a target device is defined by a design, such as provided by a hardware descriptive language such as VHDL, SystemC, or the like.

A soft error, or a fault, is a transient bit-flip or similar value modification that occurs spontaneously. In some cases, the soft error may be caused due to particle strike. An error in a design occurs when a fault results in data corruption. Typically for hardware designs, an error may be a situation when a corrupted value appears on the outputs of the design (or on a predefined set of cut-points). A fault does not always become an error; it may vanish through logical masking, electrical masking, fault detection modules, and the like. Whether or not a fault becomes an error may depend on a state of the target computerized system when the fault occurs and on input values in subsequent cycles.

Some hardware designs contain fault detection logic configured to detect, correct and/or recover from a fault. In response to detection of a fault, the design may, in some cases recover, such as for example by re-loading a previously saved clean state and re-computing values.

Soft error verification may be performed to detect scenarios in which faults are not handled as they turn to errors. In some cases, a simulated execution of the design is performed, and a fault is simulated by modifying a value of a variable, such as by flipping a value of a latch (also referred to as injecting a bit-flip to the latch). In case the fault detection logic does not handle the fault, it may result in an error during simulation. A huge number of simulation runs may be required in order to achieve appropriate coverage, and this is rarely accomplished on industrial designs.

soft error verification is specifically critical in computerized devices that are operated in a hazardous environment, such as outer-space. Such devices may be extremely expensive, and an undetected bug in them may be very costly. For example, consider a bug in a satellite which may cause the satellite to crash. Even a relatively simple bug, such as that causes the satellite to not function correctly may be very expensive to fix, as fixing it may require sending people to outer-space.

BRIEF SUMMARY

One exemplary embodiment of the disclosed subject matter is a method for detecting an error in a design that may be caused due to a soft error, the method comprising: obtaining the design, wherein the design comprising a plurality of variables and a transition relation from a state to a next state based on at least one input signal; computing a set of states of the design in respect to a variable of the plurality of variables, wherein for each state of the set of states, in case a value of the variable is changed due to the soft error, there exists one or more consecutive values to the at least one input signal that result in an error in the design; synthesizing a target identification logic configured to detect if a current state of the design is comprised by the set of states; simulating the design and the target identification logic, wherein the simulating is performed by a processor; the simulating comprising in response to a detection by the target identification logic, changing a value of the variable to simulate the soft error; and determining whether the error in the design occurred during the simulating.

Another exemplary embodiment of the disclosed subject matter is a computerized apparatus for detecting an error in a design that may be caused due to a soft error, the computerized apparatus having a processor and a storage device; the computerized apparatus comprising: a design obtainer operative to obtain the design, wherein the design comprising a plurality of variables and a transition relation from a state to a next state based on at least one input signal; a target definer configured to determine a set of states of the design in respect to a variable of the plurality of variables, wherein for each state of the set of states, in case a value of the variable is changed due to the soft error, there exists one or more consecutive values to the at least one input signal that result in an error in the design; a target identification logic synthesizer configured to synthesize a target identification logic configured to detect if a current state of the design is comprised by the set of states determined by the target definer; a simulator configured to simulate operation of the design and the target identification logic synthesized by the target identification logic synthesizer; wherein the simulator is operately coupled to a soft error triggering module, the soft error triggering module is configured to change a value of the variable associated with the target identification logic in response to a determination by the target identification logic during simulation that the current state is comprised by the set of states; and

wherein the simulator is operately coupled to an error identification module, the error identification module is configured to indicate whether there is an error in the design based on simulated states of the design.

Yet another exemplary embodiment of the disclosed subject matter is a computer program product for detecting an error in a design that may be caused due to a soft error, the computer program product comprising: a computer readable medium; a first program instruction operative to obtain the design, wherein the design comprising a plurality of variables and a transition relation from a state to a next state based on at least one input signal; a second program instruction operative to compute a set of states of the design in respect to a variable of the plurality of variables, wherein for each state of the set of states, in case a value of the variable is changed due to the soft error, there exists one or more consecutive values to the at least one input signal that result in an error in the design; a third program instruction operative to synthesize a target identification logic configured to detect if a current state of the design is comprised by the set of states; a fourth program instruction operative to simulate the design and the target identification logic, the fourth program instruction is further operative to change a value of the variable to simulate the soft error in response to a detection by the target identification logic during simulation; a fifth program instruction operative to determine whether the error in the design occurred during the simulating; and wherein the first, second, third, fourth and fifth program instructions are stored on the computer readable media.

DETAILED DESCRIPTION

One technical problem dealt with by the disclosed subject matter is to detect errors in the design that may be caused due to faults. The disclosed subject matter may be utilized to verify correctness of a fault detection logic, of correction activities, of data recovery and the like.

One technical solution is to determine a set of target states. The target states are states that if a bit-flip or similar value modification of an associated variable occurs in them, the fault may cause an error. A simulation may be performed and bit-flip may be injected in response to a determination that the simulated state is in the set of target states. Another technical solution is to determine the target states using Binary Decision Diagrams (BDDs). Reverse reachability analysis may be performed on a BDD representative of a comparative design. The comparative design may comprise two copies of the target design, and compare their respective outputs to see whether they are different. Based upon the BDD, reverse reachability analysis may be performed from a set of states in which the outputs of the two copies differ to the set of target states. Yet another technical solution is to determine the target states using an all-SAT solver. A Boolean satisfiability problem may be defined to represent a fault in a variable resulting in an error within a bounded number of cycles of the design. An all-SAT solver may be utilized to determine the set of target states. Yet another technical solution is to synthesize a target identification logic associated with detecting a state of the target states. Simulation of the design and the target identification logic may be performed. In response to a detection by the target identification logic, a fault may be simulated, such as by injecting a bit-flip to the associated latch. Yet another technical solution is to approximate the set of target states or to approximate the target identification logic.

One technical effect of utilizing the disclosed subject matter is to increase the probability of finding an error caused by a fault. Another technical effect is enabling the utilization of formal methods in conjunction with simulation to provide for a relatively reliable verification process with respect to soft errors. Yet another technical effect is to enable dynamic identification of states and latches from which a bit-flip, or other simulated fault, may be simulated. This is in contrast to randomly or heuristically simulating soft errors during simulations. Yet another technical effect is reducing a number of states in which fault simulation may be performed. Yet another technical effect is to utilize formal methods on a large model, without performing a full state exploration of the entire model, which is likely not feasible when using formal methods.

It will be noted that in the present disclosure, an error is a change in an observable output (or cut-off point) caused due to a soft error. This is in opposition to a functional error, which is defined by the design not holding a specification property.

Referring now toFIG. 1showing a computerized environment in which the disclosed subject matter is used, in accordance with some exemplary embodiments of the subject matter. A computerized environment100may comprise a verification machine110.

The verification machine110is configured to perform verification on a design associated with a target computerized device, such as a circuit, a hardware component or the like. In some exemplary embodiments, the design may be provided by a user140, such as a verification engineer, a specification designer, a QA staff member or the like. In some exemplary embodiments, the design may be given in a Hardware Descriptive Language, such as VHDL, SystemC or the like. The design may define a state of the target computerized device in a discrete cycle using one or more values to variables, such as representing latches (also referred to as flip-flops). The design may further define a transition relation function between a current state and a next state based on the current state and based on input signals.

In some exemplary embodiments, the verification machine110may comprise hardware, software and/or firmware components, combination thereof or the like. The verification machine110may be operately coupled to other computerized modules useful for performing verification in accordance with the disclosed subject matter.

In some exemplary embodiments, the verification machine110may be operately coupled to a simulator135. The simulator135be configured to simulate an execution of the design. A simulation of the design may comprise determining a current state and inputs based on the design. In some exemplary embodiments, the simulation is performed in respect to a predefined environment which may provide constraints over the inputs of the design.

In some exemplary embodiments, the verification machine110may be operately coupled to a SAT solver120. The SAT solver120may be configured to determine all satisfying assignments of a Boolean Satisfiability problem.

In some exemplary embodiments, the verification machine110may be operately coupled to a BDD module130. The BDD module130may be configured to perform operations on set of states represented by a BDD.

In some exemplary embodiments, the verification machine110may utilize the BDD module130, the SAT solver120, or a combination thereof, to determine a set of target states. During simulation performed by the simulator135, the verification machine110may simulate a fault in a latch associated with a detected target state.

In some exemplary embodiments, the user140may utilize a Man-Machine Interface (MMI)145, such as a terminal, to review output from the verification machine110and/or to provide input to the verification machine110.

Referring now toFIG. 2showing a block diagram of verification tool, in accordance with some exemplary embodiments of the disclosed subject matter. A verification tool200, such as110ofFIG. 1, may be configured to detect a fault in the design that may cause an error.

In some exemplary embodiments, a design obtainer210may be configured to obtain a design to be verified by the verification tool200. The design obtainer210may obtain the design from a user, such as140ofFIG. 1, from a file, from a predetermined interface, or the like.

In some exemplary embodiments, a target definer220may be configured to define a set of target states in respect to a latch. Target states may be states such that if a fault occurs in the latch while the system is in a target state, then an error may occur. In some cases, there exists a list of consecutive input signals that will cause the fault to become an error. In other cases, target states may be defined in a more restrictive manner—for every set of consecutive input signals, the fault becomes an error. In some exemplary embodiments, the target definer220may define an approximated set of target states. Approximation may be an under-approximation or an over-approximation. Approximation may be utilized in order to simplify the computational complexity of the target definer220.

In some exemplary embodiments, a BDD module225may be configured to perform operations on a BDD.

In some exemplary embodiments, a comparative design definer230may be configured to determine a comparative design. The comparative design may comprise two copies of the design, receiving the same input values. The comparative design may be configured to indicate whether the output of the two copies is different. For example, the output of the comparative design may be defined as a logical XOR operation between an output of the first copy and a corresponding output of the second copy.

In some exemplary embodiments, a backwards reachability determinator235may be configured to determine a set of states from which the indication of the comparative design is reachable. In some exemplary embodiments, the backwards reachability determinator235may utilize the BDD module225to represent sets of states.

Let C=I,O,L,Nbe the design, with inputs I, outputs O, latches L, and next-state functions N={N1|1εL}, where each N1is a function from I×L to 2(0,1)determining the value of 1 in the next clock cycle based on the current values of latches in L and inputs in I. In some cases, the design may comprise a detection logic. The detection logic may comprise a detection flag, such as a signal that is raised in response to a detection of a fault. The detection flag is denoted by “det”. Let tεL be a designated latch for which the target states need to be determined. The comparative design may contain two copies of C (C1=I1, O1, L1, N1and C2=I2, O2,L2, N2) and comparison logic such that in case that an output of C1is different than the corresponding output of C2then an error bit is raised. A comparative design400ofFIG. 4shows an exemplary comparative design. Inputs405are used by both C1410and C2420. An output value430is based on a XOR operation between outputs of C1and C2. The XOR operation may be implemented using a XOR gate440.

In some exemplary embodiments, the target definer220may compute the target states in respect to the latch t by performing the following operations:i←1Build a BDD for f1=error (This is a relatively small BDD that represents all the states, reachable or not, in which error is asserted)Perform backward reachability from f1. For example, perform iterativelyi←i+1front←[EX(fi-1)!det1!det2], where EX(A) is defined as the set of states that have a successor in the BDD A. In other words, front may be a set of states that have a successor state in fi-1and in which the detection flag is not raised in both copies of the design.fi←fi-1frontuntil (fi=fi-1), or until a determination to stop the reachability (e.g., due to limited available resources).from fiextract all the states that differ only in the value of the variable t (i.e., t1≠t2, and ∀l εL, l≠t,l1=l2).From the extracted states, take the state of only one of the copies (e.g., quantify out the state bits of C2)

In some exemplary embodiments, the design may not comprise a detection flag. Therefore the set front may be determined to be EX(fi-1).

In some exemplary embodiments, a Boolean satisfiability problem definer240may be configured to define a Boolean satisfiability problem associated with a bounded comparative design. The bounded comparative design may comprise state variables for two copies of the design for each cycle of a predetermined number of cycles. The values of the state variables may be defined based on combinatorial logic of the design, based on values of the state variables of a previous cycle and based on input signals of the current cycle. The bounded comparative logic may be configured to determine an output value indicating whether there is a difference in an output of the two copies. The bounded comparative logic may be configured to simulate a bit flip in the variable in one of the copies.

A bounded comparative design500ofFIG. 5shows an exemplary bounded comparative design, in accordance with some exemplary embodiments of the disclosed subject matter. An output value540is determined based on a difference between outputs of a first bounded copy of the design, represented by logic510,520and530, and a second bounded copy of the design, represented by logic511,521,531. A XOR gate545may be utilized to determine whether the outputs are the same. Initial state variables505may be given as input to both copies of the bounded design. A bit-flip logic507may be configured to simulate a bit flip in the value of the variable, such that the given initial state of the first copy is the same as that given for the second copy except for the value of the one chosen variable. The same inputs may be given to both copies in each cycle (e.g., inputs1512, inputs2522, inputsN532). In each cycle, the state variables of the previous states are used together with the input signals to determine the output and the next state. For example, the logic520(which is the same as511) computes the state in the second cycle based on the inputs in the second cycle (inputs2522) and based on the state in the first cycle, which is computed by the logic510.

In some exemplary embodiments, the design may be partitioned into two parts, state bits and combinational function that computes the next state based on inputs and the initial state. The combinational logic may be duplicated, wherein each copy corresponds to a different clock cycle. For example, the logic510and520may be the same logic, each corresponding to a different cycle. In some exemplary embodiments, several different bounded comparative designs may be determined, each may be associated with a different variable and/or a different number of cycles.

In some exemplary embodiments, an all-SAT solver245may be configured to determine all satisfying assignments to the Boolean satisfiability problem defined by the Boolean satisfiability problem definer240. In some exemplary embodiments, the all-SAT solver245may be a SAT solver configured to repeatedly provide satisfying assignments to the same Boolean satisfiability problem. In some exemplary embodiments, the all-SAT solver245may be a SAT solver, such as DPLL-based SAT solver configured to iteratively solve the SAT problem and determine new satisfying assignments until an UNSAT is determined. In some exemplary embodiments, the all-SAT solver245may implement the method described in E. Arbel, O. Rokhlenko, K. Yorav “SAT-based synthesis of clock gating functions using 3-valued abstraction” FMCAD'09, which is hereby incorporated by reference.

In some exemplary embodiments, the target definer220may be configured to utilize the Boolean satisfiability problem definer240to determine Boolean satisfiability problems with respect to each variable and with respect to each possible bound on the design, up to the depth of the design. The all-SAT solver245may be configured to determine all possible satisfying assignments of each defined problem. In such a case the target definer220may determine all possible target states. In some exemplary embodiments, a portion of the problems and/or of the assignments may be omitted from computations. In such a case, the target definer220may determine an under-approximated set of the target definer220. In some exemplary embodiments, the portions may be omitted due to limited resources, such as computational power, time or the like.

In some exemplary embodiments, the target definer220may be an approximated target definer that is configured to approximate the set of target states. The approximated set may be an under-approximation (e.g., comprising a portion of the complete set), an over-approximation (e.g., comprising the complete set and surplus states), or the like. In some exemplary embodiments, an approximated backward reachability analysis may be performed, such as by performing an approximated backward step, or the like.

In some exemplary embodiments, a target identification logic synthesizer250may be configured to synthesize a target identification logic that is configured to detect whether a state of the design is comprised by the target states determined by the target definer220. “Synthesizing”, in this context, does not necessarily include fabricating an actual circuit of similar component. In some exemplary embodiments, the target identification logic synthesizer250may determine an automaton that checks whether or not a state is a target state. The target identification logic may be a set of logical operations, a checker, a circuit, or the like, such as defined using a HDL.

In some exemplary embodiments, the target identification logic synthesizer250may be an approximated target identification logic synthesizer. The approximated target identification logic synthesizer may be configured to synthesize an approximated target identification logic which is configured to approximate whether a current state of the design is comprised by the set of target states. For example, the approximated target identification logic may perform its determination without checking all bits that represent the state. Approximation may be used in case of computationally-hard designs or sets of states. In some exemplary embodiments, synthesizing the target identification logic may require non-polynomial computation time, which may, in some cases, be not feasible. Approximation may enable feasible, though not exact, operation.

In some exemplary embodiments, a simulator260may be configured to simulate an execution of a design. The simulator260may be configured to simulate the execution of the design received by the design obtainer210and the target identification logic determined by the target identification logic synthesizer250.

In some exemplary embodiments, a soft error triggering module265may be configured to trigger a soft error simulation in response to a simulated execution in which a target state is detected. In response to a detection by the target identification logic, the soft error triggering module265may trigger a simulated soft error in a variable associated with the target state detected by the target identification logic. The simulated soft error may be, for example, injecting a bit flip to the variable. In some exemplary embodiments, in case more than one target identification logics detect a target state, the state may be duplicated and two or more simulated executions may be invoked, each associated with a simulated soft error in a different variable.

In some exemplary embodiments, an error identification module270may be configured to determine whether a simulated state by the simulator260is an error. An error may be determined based on a value of an output of the design, based on a value in a cut-off point, or the like.

In some exemplary embodiments, a soft error occurring (or simulated to occur) in a unit of the design may be handled in another unit of the design. Therefore, using a simulator260is more likely feasible than using formal methods on the entire design, which may be too large to be handled by currently known formal methods.

The storage device207may be a Random Access Memory (RAM), a hard disk, a Flash drive, a memory chip, or the like. The storage device207may retain the design obtained by the design obtainer210, the one or more sets of target states determined by the target definer220, the one or more target identification logics synthesized by the target identification logic synthesizer250, the simulated state of the design and/or the target identification logic simulated by the simulator260or the like.

In some exemplary embodiments of the disclosed subject matter, the verification tool200may comprise an Input/Output (I/O) module205. The I/O module205may be utilized to provide an output to and receive input from a user, such as140ofFIG. 1.

In some exemplary embodiments, the verification tool200may comprise a processor202. The processor202may be a Central Processing Unit (CPU), a microprocessor, an electronic circuit, an Integrated Circuit (IC) or the like. The processor202may be utilized to perform computations required by the verification tool200or any of it subcomponents.

In some exemplary embodiments, components of the verification tool200may be implemented in software, hardware, firmware or the like. For example, the simulator260may be implemented by a software code retained in the storage device207and by the processor202performing computation in accordance with the software code.

Referring now toFIG. 3showing a flowchart diagram of a method in accordance with some exemplary embodiments of the disclosed subject matter.

In step300, a design may be obtained. The design may be obtained by a design obtainer, such as210ofFIG. 2.

In step310, target states associated with a variable of the design may be computed. The target states may be computed by a target definer, such as220of FIG.2. In some exemplary embodiments, target states may be computed using BDDs or using Boolean satisfiability problems or the like.

In step322, a BDD of a comparative design between two copies of the design may be determined The comparative design may be determined by a comparative design definer, such as230ofFIG. 2. The comparative design may be represented by a BDD using a BDD module, such as225ofFIG. 2.

In step332a set of states in the comparative design for which the output is different in the two copies of the design may be determined The set of states may be determined by the BDD module.

In step342, a backward reachability analysis of the set of states determined in step332may be performed. The backward reachability analysis may be performed by a backwards reachability determinator, such as235ofFIG. 2. The backward reachability analysis may be performed until a fix-point is determined, or until a determination to stop the analysis, such as for example in case of BDD representations becoming relatively big and requiring a relatively high amount of memory, in case of time limit reached or the like.

In some exemplary embodiments, steps324and334may be performed in order to compute the target states.

In step324, a Boolean satisfiability problem may be defined to correspond to a bit-flip resulting in an error within a predetermined number of cycles. The Boolean satisfiability problem may be defined by a Boolean satisfiability problem definer, such as240ofFIG. 2.

In step334an all-SAT solver, such as245ofFIG. 2, may be utilized to determine all satisfying assignments of the problem defined in step324.

In some exemplary embodiments, steps324and334may be performed a plurality of times, each time in respect to a different number of cycles.

In step350, a target identification logic may be synthesized from the target states determined in step310. The target identification logic may be synthesized by a target identification logic synthesizer, such as250ofFIG. 2.

In some exemplary embodiments, steps310and350may be performed a plurality of times, each time in respect to a different latch or variable of the design.

In step360, an operation of the design and the target identification logic may be simulated. The simulation may be performed by a simulator, such as260ofFIG. 2.

In step370, in response to a detection by the target identification logic that a current state of the design is a target state, a simulation of a soft error may be performed. The soft error may be simulated by modifying the value of the variable associated with the triggered target identification logic. The soft error may be simulated, for example, by injecting a bit-flip. The operation of step370may be performed b a soft error triggering module, such as265ofFIG. 2.

In some exemplary embodiments, in response to triggering a simulated soft error, the simulation may continue and an error may be detected. In some exemplary embodiments, a plurality of simulated executions may be performed in order to provide for a relatively high coverage.