Efficient System Traversal And Property Checking By Exploiting Circuit Locality

Abstract

Traditional methods of verification are empirical in nature and are based on extensive simulation of hand-written or automatically generated diagnostic test vectors. Although, provably effective in early stages of the debugging process, their effectiveness drops quickly along the maturity of the design. Hence, functional verification has problems in catching the corner cases, therefore formal verification complements it in order to cope up with the design growth.

In formal verification efficient search procedures are used to automatically determine whether the state space of a design satisfies an abstract logical specification (properties). The typical problem of such analysis is that after some steps of traversal, the system can not handle the overwhelming state space anymore and hence the memory overflow problem occurs. There is constant work on finding algorithms to reduce the memory requirement bottlenecks. One such novel proposal is to partition the state space into two or more pieces and handle them separately for further state space traversal. To validate a design completely which is relatively large, a divide-and-conquer approach is state-of-the-art. The major problem of this methodology is revisiting of states in different partitions and is known as state space overlap that results in redundant computations.

The “MinOverlap” algorithm in this thesis aims at a reduction of state space overlap of different partitions that minimizes the redundant computation and decreases the verification time. The reduction is achieved automatically by means of collecting the information in the form of influence table of state variables by exploiting the designs transition relation. Similarly, to verify a property faster, the “Guiding” algorithm in this thesis aims at steering the state space traversal algorithm in the direction of the target states automatically. It avoids the un-interesting state space saving memory and speeds up the finding of bugs. The experimental results shows substantial speed up of the verification process by these heuristics.

Hardwarefehler kosten Geld. Jedes Mal, wenn ein Fehler in einem Design auftaucht, muessen Zeit und Geld verschwendet werden, damit das Problem lokalisiert und korrigiert wird. Bei der wachsenden Komplexitaet digitaler Systeme und des riesigen early-time-to-market Drucks kann die Notwendigkeit von Verifikationsmitteln, die den Designern helfen, bugs im Fruehstadium des Designprozesses festzustellen, genug betont werden. Verifikation benoetigt laut Statistiken ungefaeahr 75% der Designzeit.

Die traditionellen Verifikationsmethoden sind empirischer Natur und suetzen sich auf extensive Simulation handgeschriebener oder automatisch erzeugter diag-nostischer Testvektoren. Obwohl ihre Effektivitaet in fruehen Stadien des debugging Prozesses nachgewiesen ist, sinkt diese schnell sobald das Design weniger Fehler aufweist. Deswegen hat die funktionelle Verifikation Probleme bei der Feststellung von Randfaellen und darum wird sie durch die formale Verifikation ergaenzt, um die Designentwicklung zu bewaeltigen.

Bei der formalen Verifikation werden effiziente Suchprozesse verwendet, um automatisch zu bestimmen, ob der Zustandsraum eines Designs eine abstrakte logische Spezifikation erfuellt (properties). Im Allgemeinen ist die Erreichbarkeitsanalyse als ein Hauptbestandteil der formalen Verifikation bekannt. Fuer groessere Eigenschaftsklassen kann Verifikation auf Erreichbarkeitsanalyse reduziert werden. Die Erreichbarkeitsanalyse bezieht sich auf die Gruppe der Zustaende, die durch einen Schritt aus einer Gruppe definierter Eingangszustaende erreicht werden kann. Das typische Problem dieser Vorgehensweise ist, dass das System nach einigen Schritten den ueberwaeltigenden Zustandsraum nicht mehr bewaeltigen kann und folglich ein Speicherueberlauf eintritt. Es wird fortlaufend daran gearbeitet Algorithmen zu finden, um die Speicherengpaesse zu reduzieren. Ein solcher Ansatz, die Speicheranforderungen zu reduzieren ist die symbolische Darstellung des Zustandsraums, in der Binary Decision Diagrams (BDD) als Datenstrukturen verwendet werden. Hierbei wird das Traversieren des Zustandsraums symbolisch durch Manipulieren von BDDs ausgefuehrt.

Grosse Designs koennen jedoch viele Millionen von BDD-Knoten benoetigen, was auch haeufig einen Speicherueberlauf verursacht. Dieses Phaenomen ist als BDD-blow-up bekannt. Es sind mehrere Loesungen vorgeschlagen worden, um die grossen Speicheranforderungen von BDDs zu bewaeltigen. Ein solcher neuer Vorschlag ist, das BDD in zwei oder mehr Teile zu partitionieren und diese separat fuer die weitere Zustandsraumtraversierung zu bearbeiten. Obwohl Algorithmen zum Partitionieren des eigentlichen BDD existieren, sind diese oft nicht optimiert, und somit fuer die exzessive Zunahme der BDDs verantwortlich, welches eine langsame Verifikation oder Speicherprobleme nach sich zieht. Die vorliegende Doktorarbeit befasst sich mit intelligenten Heuristiken, die das Partitionieren optimieren. Die Dissertation traegt zwei Heuristiken bei, MinOverlap feur den vollstaendigen Validierungsansatz und Guiding fuer einen schnellen Falsification Ansatz.

Um ein relativ grosses Design vollstaendig zu validieren, ist eine divide-and-conquer Vorgehensweise Stand der Technik. Sie partitioniert Original-BDDs, deren Knotenzahl einen Schwellwert ueberschreiten, und bearbeitet die Partitionen separat. Das Hauptproblem dieser Methodologie ist das wiederholte besuchen von Zustaenden in unterschiedlichen Partitionen. Dies ist als Zustandsraumueberdeckung (state space overlap) bekannt und fuehrt zu redundante Berechnungen. Der MinOverlap - Algorithmus bezweckt eine Reduktion der Zustandsraumueber-deckung unterschiedlicher Partitionen, was die redundante Berechnung minimiert und die Verifikationszeit verringert. Die Reduktion wird automatisch erreicht, indem die Informationen in der Form von Einflusstabellen (influence tables) von Zustandsvariablen durch Auswerten der Transitionsrelation des Designs gesammelt werden.

Gleichermassen ist die schnellere Verifikation einer Eigenschaft durch guiding Stand der Technik. Jedoch ist dies nicht vollautomatisch zu bewerkstelligen und benoetigt Intervention. Der Guiding-Algorithmus in dieser Doktorarbeit bezweckt, den Zustandsraumtraversierungsalgorithmus automatisch in die Richtung der Zielzustaende zu steuern. Er umgeht den uninteressanten Zustandsraum, wodurch Speicher gespart wird, und beschleunigt das Auffinden von Fehlern. Das Guiding wird umgesetzt, indem Informationen der Eigenschaft und der Transitionsrelation ueber Zielzustaende ausgeschoepft und fuer effizientes Guiding angewendet werden, um die Traversierung automatisch zu steuern. Die experimentellen Ergebnisse zeigen eine beachtliche Beschleunigung des Verifikationsprozesses durch diese Heuristiken.