Publication Details
Using Model Checker to Analyze and Test Digital Circuits with Regard to Delay Faults
digital circuit, timing, delay, fault, timed automaton, 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.
@inproceedings{BUT170908,
author="Josef {Strnadel}",
title="Using Model Checker to Analyze and Test Digital Circuits with Regard to Delay Faults",
booktitle="Proceedings of 2021 24th International Symposium on Design and Diagnostics of Electronic Circuits & Systems",
year="2021",
pages="111--114",
publisher="Institute of Electrical and Electronics Engineers",
address="Vienna",
doi="10.1109/DDECS52668.2021.9417069",
isbn="978-1-6654-3595-6",
url="https://www.fit.vut.cz/research/publication/12433/"
}