Using SAT-solvers for deriving patch circuits that mask nodes faults and trojan circuits injections

Combinational circuit C consisting of gates is considered. A sub-circuit with set V of output nodes and set U of input nodes is separated in it. Set V consists of outputs of circuit C fault nodes (logic faults are assumed) and inputs of circuit C fault free nodes that are fed by lines in which Trojan Circuits are injected. Correction of circuit C behavior based on applying as much as possible simple patch circuit (in the frame of Engineering Change Order (ECO) technologies) is suggested. Patch circuit inputs are connected with nodes from set U . Patch circuit outputs are connected either with internal circuit C nodes that are fed by its fault nodes or with nodes that are fed by lines in which Trojan Circuits are injected. Current approaches to correction of circuit C behavior are based on results of circuit C simulation and guarantee correct results on a set of input Boolean vectors that are applied during simulation. We suggest using incompletely specified Boolean functions of nodes from set V and guarantee correct circuit C behavior on all its input vectors. Deriving incompletely specified Boolean functions is based on applying SAT solver. Then incompletely specified Boolean functions of nodes from set V are used by ESPRESSO system followed by ABC system to get patch circuit.

Keywords

Authors

References