Detail publikace
Using Model Checker to Analyze and Test Digital Circuits with Regard to Delay Faults
číslicový obvod, časování, zpoždění, porucha, časovaný automat, ověřování modelů, protipříklad, testovací případ, test
Úzké časové hranice v moderních číslicových obvodech vedou na obtížně detekovatelné poruchy zpoždění. Pravděpodobnost toho, že k tomuto defektu dojde, se roste s faktory jako např. zmenšující se rozměry, rostoucí variace procesů, vyšší provozní kmitočty či stárnutí/stres obvodů. Tradičně, časování je bráno v potaz v souvislosti s logickým návrhem, fyzickým návrhem a rozmísťováním, testováním zpoždění vývojového procesu obvodu a staví na principech charakterizace poruch, poruchových modelech a časové analýze. Tento článek prezentuje přístup založený na ověřování modelů s cílem usnadnit řešení problémů souvisejících s analýzou dopadů a testováním poruch zpoždění. Přístup předpokládá, že obvod je modelován coby síť stochastických hybridních časovaných automatů schopných popsat obvod jak v logické tak časové doméně, včetně skutečností jako nejistota a variace. Prezentovaný přístup je založen na shromáždění atributů, formalizaci očekávaných vlastností obvodu a následné transformaci obvodu do našeho modelu. Následně je použit nástroj pro statistické ověřování modelů za účelem ověření očekávaných vlastností a generování protipříkladu pro každou vlastnost, kterou obvod nemá. Konečně, přístup transformuje protipříklady na testovací případy a na test zpoždění schopný ověřit, zda jsou časové požadavky, kladené na obvod, dodrženy.
@INPROCEEDINGS{FITPUB12433,
author = "Josef Strnadel",
title = "Using Model Checker to Analyze and Test Digital Circuits with Regard to Delay Faults",
pages = "111--114",
booktitle = "Proceedings of 2021 24th International Symposium on Design and Diagnostics of Electronic Circuits \& Systems",
year = 2021,
location = "Vienna, AT",
publisher = "Institute of Electrical and Electronics Engineers",
ISBN = "978-1-6654-3595-6",
doi = "10.1109/DDECS52668.2021.9417069",
language = "english",
url = "https://www.fit.vut.cz/research/publication/12433"
}