Using Model Checker to Analyze and Test Digital Circuits with Regard to Delay Faults

digital circuit, timing, delay, fault, timed au­tomaton, model checking, counter-example, test case, test

Narrow timing margins in modern digital circuits result in delay defects that are difficult to detect. The probability that such a defect occurs increases with factors such as shrinking feature sizes, increasing process variations, higher operating frequencies, and aging/stress of the circuits. Traditionally, timing is considered in connection with the logic design, physical design and layout, and delay testing phases of the circuit development process and builds on principles of delay characterization, fault models and timing analysis. This paper presents a model checking approach aiming to facilitate the solutions of problems with regard to analyzing consequences and testing of delay faults. Our approach expects that a circuit is modeled as a network stochastic hybrid timed automata capable to describe the circuit both in the logical and temporal domains, including facts such as uncertainty and variations. In our approach, we gather attributes and formalize expected properties of a circuit and transform the circuit into our model. Then, we use a statistical model checker to check the properties and to produce a counter-example for each property being violated. Further, we transform the counter-examples into test cases and finally, into a delay test able to check whether the timing requirements are met.