Abstract-Gived en felaktig design, funktionella verifiering returnerar ett fel spår som uppvisar en obalans mellan specifikationen och genomförandet av en design. Automatiserad design felsökning använder dessa felspår för att identifiera potentiellt felaktiga moduler som orsakar felet. Med den ökande storleken och komplexiteten hos moderna VLSI-designer har felspår blivit längre och svårare att analysera. Samtidigt har designdebugging blivit ett av de mest resursintensiva stegen i chipdesigncykeln. Detta arbete föreslår en skalbar SAT-baserad design debugging algoritm som använder interpolanter för att över approximera uppsättningar av begränsningar som modellerar det felaktiga beteendet. Algoritmen partitionerar det ursprungliga problemet i en sekvens av mindre subproblem genom att använda underavsnitt av felspåret som undersöks iterativt. Detta möjliggörs genom att använda interpolanter för att ordentligt begränsa det felaktiga beteendet för varje subproblem, avsevärt minska antalet samtidiga tidsramar som undersöks i felspåret. Den beskrivna metoden visas vara komplett och en ytterligare teknik presenteras för att förbättra kvaliteten på felsökningsresultaten med hjälp av flera interpolanter. Experiment på äkta design visar en 57% minskning av minnet och 23% minskning av körtiden jämfört med tidigare arbete.
I REF använder författarna interpolanter för att minska antalet tidsramar i ILA genom att ersätta sekvenser av tidsramar med en överskattning av deras begränsningar.
Scaling VLSI design debugging with interpolation
{'venue': '2009 Formal Methods in Computer-Aided Design', 'journal': '2009 Formal Methods in Computer-Aided Design', 'mag_field_of_study': ['Computer Science']}