Abstrakt. Predikerad abstraktion är en viktig teknik för att extrahera kompakta finita tillståndsmodeller från stora eller oändliga tillståndssystem. Predicera abstraktion använder beslutsförfaranden för att beräkna en modell som är kompatibel med modellkontroll, och har använts framgångsrikt för programvaruverifiering. Det har dock inte gjorts mycket arbete med att tillämpa predikativ abstraktion på storskaliga finita tillståndssystem, framför allt hårdvara, där beslutsförfarandena är SAT-lösare. Vi anser predikativ abstraktion för hårdvara inom ramen för CounterexampleGuided Abstraction Raffinering där den abstrakta modellen under verifieringen måste förfinas upprepade gånger. Målet med förfiningen är att eliminera falskt beteende i den abstrakta modellen som inte finns i den ursprungliga modellen, och ger upphov till falska negativa (sporriga kontraexempel). I detta dokument presenterar vi två effektiva SAT-baserade algoritmer för att förfina abstrakta hårdvarumodeller som hanterar falska övergångar respektive falska motexempel. Båda algoritmerna använder sig av de konfliktdiagram som skapas av SAT-lösare. Den första algoritmen extraherar begränsningar från de konfliktgrafer som används för att göra den abstrakta modellen mer exakt. När en abstrakt övergång är fast besluten att vara falsk, vår algoritm behöver inte göra några ytterligare samtal till SAT lösare. Vår andra algoritm genererar en kompakt predikat som eliminerar ett falskt motexempel. Denna algoritm använder konfliktdiagrammen för att identifiera de viktiga konkreta variabler som gör kontraexemplet falskt, skapar ytterligare en grund över dessa konkreta variabler, och lägger till det till den abstrakta modellen. Experiment över maskinvarudesign med flera tusentals register visar hur effektiva våra metoder är.
I REF, SAT-baserad predikat abstraktion tillämpas på hårdvaruverifiering.
SAT Based Predicate Abstraction for Hardware Verification
{'venue': 'SAT', 'journal': None, 'mag_field_of_study': ['Computer Science']}