Efficient distributed bounded property checking [Elektronische Ressource] / vorgelegt von Pradeep Kumar Nalla

Sujets

• Informatik

Informations

• Publié par: eberhard_karls_universitat_tubingen
• Publié le: 01 janvier 2008
• Nombre de lectures: 10
• Langue: English
• Poids de l'ouvrage: 2 Mo

Extrait

EfficientDistributedBounded
PropertyChecking
Dissertation
derFakultat¨ fu¨rInformations-undKognitionswissenschaften
derEberhard-Karls-Universitat¨ Tu¨bingen
zurErlangungdesGradeseines
DoktorsderNaturwissenschaften
(Dr. rer. nat.)
vorgelegtvon
Dipl.-Inform. PradeepKumarNalla
ausHyderabad,Indien
Tubi¨ ngen
2008Tagdermu¨ndlichenQualifikation: 09.07.2008
Dekan: Prof. Dr. MichaelDiehl
1. Berichterstatter: Prof. Dr. ThomasKropf
2. Berichterstatter: Prof. Dr. WolfgangRosenstielDedicatedto
AmmaandNanna
Firstyourparents,theygive youyourlife, butthenthey trytogiveyoutheirlife.
-Chuck PalahniukAcknowledgements
Coming together is a beginning. Keeping together is progress. Working together is suc-
cess.
-HenryFord
I would like to thank Prof.Wolfgang Rosenstiel and Prof.Thomas Kropf for
giving me the opportunity to do research and pursue Ph.D. studies in Formal
Methods Group. In particular, I acknowledge the assistance and logistical sup-
portprovidedbyProf.Rosenstiel. Istronglybelieveheisthepersonificationofa
perfect professor. Apart from technical issues, he also helped me in solving bu-
reucratical issues like VISA extensions, etc. My special thanks to Thomas Kropf.
Heisimpeccableandalwaystalkstothepoint. Healthy,positiveandconstructive
criticism he does during presentations makes us improving our confidence and
lifts our morale. We persons in individual become more tough and do goal ori-
entedresearchwork. Healsonurturedhowtobeagoodresearchscientist. Iam
grateful to Dr. Jur¨ gen Ruf for his constant encouragement. Ups and downs are
all part and parcel of the research. During lows Jur¨ gen was always there for me
and supported me. Thanks to his excellent coding skills and the tools he devel-
oped. Most of the times, the code he implemented is self-explanatory. Thereby,
I learned lot of inside depths of formal verification. My sincere thanks to Dr.
Roland J. Weiss for some of his original ideas in my Ph.D. thesis. He motivated
me to be more challenging and competitive at work. During his stay in Tub¨ in-
gen, he had inculcated me a sense of responsibility in writing worthful papers
andgoodorganizingskills. Afterallheisanicehumanbeingandmademystay
very special at Tub¨ ingen. I am particularly grateful to Dipl.Ing.Ingo Kuh¨ n. He
hasinspiredandmotivatedmetodoresearchwhileIwasdoingMastersthesisat
AMDSaxony,Dresden. MyspecialthankstoallthemembersofFormalMethods
Group (FMG) for the care with which they reviewed the original manuscript of
my thesis. In particular, I would like to thank Dr. Prakash Mohan Peranandam.
He has assisted me in resolvinginitialproblems of mine concerning research di-
rection. In many ways I have used both his technical and personal experiences.
TheseexperiencesmademylifemucheasierinTub¨ ingen. Iexpressmydeepgrat-
itude also to M.Sc.Djones Lettnin and Dipl.Inf.Jo¨rg Behrend. It was fun work-
ing with them. I must acknowledge my colleagues Dipl.Inf. Michael Bensch
and Dipl.Inf.Dominik Brugger. Michael was characteristically generous in tak-
ingtimetoreviewmanyofmyresearchpapersandthisthesis. Dominikistruly
inspirational figure and he has provided encouragement and ideas in applying
conceptsfromdifferentrealmsintoformalverificationofsoftware. Ireallyappre-
ciate the support provided by the folks at Technische Informatik. Their friend-
ship and professional collaboration meant a great deal to me. I really enjoyed
theircompanyinski-seminars,collectiveoutings,afternoonlunch,etc. Imustac-
knowledge my wife for patience and understanding she has shown during finalphaseofmythesiswriting. Myspecialthankstomysisterandherfamilyforsup-
portingandtakingcareofmyparentsduringmyperiodofstayinGermany. Iam
thankful to German Research Council (DFG), German Federal Ministry of Edu-
cation,Science,ResearchandTechnology(BMBF)andEdacentrumforproviding
financial support to pursue my research studies in Germany. Last but not least,
thankstowww.google.com(/de)andwww.wikipedia.com(/de). Theymadeour
life much easier to access the enormous amount of information through world
wideweb.
FinallyI wouldliketo make a note: It has been a very long journey I have taken,
butaveryfulfilling one.Abstract
Today, verification of industrial size designs like multi-million gate ASICs (Ap-
plicationSpecificIntegratedCircuit)andSoC(System-on-a-Chip)processorscon-
sumesupto75%ofthedesigneffort. Thetrendtoaugmentfunctionalverification
with formal verification tries to alleviate this problem. Efficient property check-
ingalgorithmsbasedonbinarydecisiondiagrams(BDDs)andsatisfiability(SAT)
solvers allowthe automatic verificationof medium-sized designs. However, the
steadily increasing design sizes still leave verification as the major bottleneck,
becauseformalmethodologiesdonotyetscaletoverylargedesigns.
To address these problems researchers came up with the idea of combining
symbolic simulation and bounded model checking on-the-fly. The current tools
pioneer in handling comparatively larger designs by partitioning the state set
and they can be represented using partitioned ordered BDDs (POBDDs). These
partitions will be explored in a divide-and-conquer manner. However, still they
face memory exhaustion for very large models due to the BDD explosion prob-
lem. Even the SAT based bounded model checking (BMC) can search up to a
maximum depth allowed by the physical memory on a single server. These
observations motivated the parallelization of symbolic state space traversal al-
gorithms. Distributed algorithms verify larger models and return results faster
than sequential versions. Existing schemes for parallelizing BDD-based verifi-
cation algorithms often suffer from state overlap or duplicate work, cross over
states among partitions, inefficient work distribution, improper load balancing,
synchronicityandcommunicationoverhead. Thealgorithmsconcentrateheavily
eitheronreachability(validation)orfalsificationbutnotbothtogether.
My main contributions include a dynamic overlap reduction and a hybrid dis-
tributed algorithms. The dynamic overlap reduction technique smoothens the
state space traversal of each network node by removing the state overlap that
it suffers from. The removal of overlap works in an asynchronous manner, i.e.,
withoutwaitingforotherprocessorstocompletetheirimagecomputations. This
method has the natural side effect of dynamic load balancing among network
nodes, i.e., the nodes that deal with a large state space at one time point will be
later assigned a small state space and vice versa. Since all the nodes perform
asynchronous state space traversal on their whole state subsets, the method is
bestsuitableforvalidation.
Thehybridmethodisanasynchronousdistributedalgorithm,suitedforboth
fasterrordetectionandcompletevalidation. Thisapproachcombineswellknown
windowing and dynamic overlap reduction techniques. The windowing technique
has partitions that are identified by unique combination of variables. Each win-
dow restricts its state space at regular intervals to keep the reachable state space
withinit’swindowregion. Therealstatespaceisdiscriminatedbythewindowas
owned and non-owned states. The nodes on the cluster machine are employedwithtwodifferenttypesoftasks. Somenodes, windowsaimatfasterfalsification
on the basis of the windowing technique. The other type of nodes called helpers
are intending for validation on the basis of the dynamic overlap reduction. All
the network nodes asynchronously traverse their local state spaces for both er-
ror states detection and reachability of a time bound. Thus, the hybrid algorithm
efficiently combines both windowing and dynamic overlap reduction techniques to
obtainmoresynergyandgainstheadvantagesofusingboththeapproaches. Fur-
ther, the algorithm expedites the verification process by reassigning the work to
idle nodes as quickly as possible. As a result it avoids the wasted computation
powerandmakesthesystemworkefficient.
The dynamic overlap reduction and hybrid algorithms are best suitable for
homogeneous system configurations like a cluster. However, this thesis also
presents a grid-based parallelization algorithm which is suitable for fast falsifi-
cationofverylargedesigns. Inaddition, alltheparallelalgorithmsinthisthesis
partition the state space using the Minimal overlap algorithm which pioneers in
staticallyminimizingthecrossoverstatesorstateoverlapamongthepartitions.
The parallel algorithms speedup the distributed verification and automati-
callychecksthecorrectnessofverylargehardwaredesigns. Thedistributedcom-
putation shows approximately linear speedups in execution time and enables
fasterverificationofproperties. Asasupplement,thisthesisalsopresentsanovel
distributedalgorithm,whichusesmixedforwardandbackwardtraversalmech-
anismforBlackBoxverification.Zusammenfassung
Heutzutagebeno¨tigtdieVerifikationvonindustriellenDesignswiez.B.ASICs
(ApplicationSpecificIntegratedCircuit)undSoC(System-on-a-Chip)biszu75%
derEntwicklungskosten.DerTrendfunktionaleVerifikationdurchformaleVeri-
fikation zu erweitern versucht dieses Problem zu lo¨sen. Effiziente Algorithmen
basierend auf BDDs (Binary Decision Diagrams) und SAT (Satisfiability) erlau-
ben die automatische Verifikation von mittelgroßen Designs. Durch die sta¨ndig
wachsenden Designgro¨ßen bleibt die Verifikation trotzdem der Flasc