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

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

Stať ve sborníku v databázi WoS či Scopus

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.

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.

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

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

STRNADEL, J.

2022

01.04.2021

Institute of Electrical and Electronics Engineers

Vienna

978-1-6654-3595-6

Proceedings of 2021 24th International Symposium on Design and Diagnostics of Electronic Circuits & Systems

111

114

4

https://www.fit.vut.cz/research/publication/12433/

strnadel_ddecs2021_poster