Formal verification methodologies for nonlinear analog circuits [Elektronische Ressource] / von Sebastian Steinhorst

Sebastian Steinhorst

Sujets

• Informatik

Informations

• Publié par: goethe_universitat_frankfurt_am_main
• Publié le: 01 janvier 2011
• Nombre de lectures: 29
• Langue: English
• Poids de l'ouvrage: 4 Mo

Extrait

FormalVerificationMethodologies
forNonlinearAnalogCircuits
Dissertation
zurErlangungdesDoktorgrades
derNaturwissenschaften
vorgelegtbeimFachbereichInformatikundMathematik
derJohannWolfgangGoethe-Universita¨t
inFrankfurtamMain
von
SebastianSteinhorst
ausMainz
Frankfurt(2011)
(D30)vomFachbereichInformatikundMathematikderJohannWolfgang
Goethe-Universita¨talsDissertationangenommen
Dekan: Prof.Dr.TobiasWeth
Gutachter: Prof.Dr.LarsHedrich
Priv.-Doz.Dr.HelmutGra¨b
DatumderDisputation: 3.Februar2011Acknowledgments
Thisthesisistheresultoffiveyearsofmyresearchinthe ElectronicDesignMethodo-
logyGroupattheInstituteofComputerScienceoftheGoethe-UniversityofFrankfurt
amMain.Itwouldnothavebeenpossiblewithoutthesupportofmanypeople.
First of all, I would like to express my deepest gratitude to my doctoral advisor,
LarsHedrich,forhisencouragement,guidanceandsupportfromthebeginningsofmy
researchuntilthefinalizationofthisthesis.Hiskeenmindandoverwhelminginterest
inmyworkhavebeenaninvaluablehelp.
I am especially indebted to Helmut Gra¨b for fruitful discussions, his continuous
interestinthisthesisandforactingasareferee.
Moreover,IoweabigthankyoutomyexaminersGeorgSchnitgerandUweBrink-
schultefortheirinterestingquestionsandvaluableremarks.
Iamgrateful to AngelikaSchifignano forall ofherassistance, beingthe nicestand
mostcaringsecretaryIcouldimagine.
I would like to thank Oliver Mitea, with whom I shared the office for 4 years, for
the great time we had together as colleagues and most of all for becoming a friend.
Furthermore,IwouldliketothankmycolleaguesMingyuMa,MarkusMeissner,Julius
von Rosen and Felix Salfelder for the great working atmosphere in our group. Thank
you also to Ronja Du¨ffel, Andreas Hofmann, Conrad Rau, David Sabel and Manfred
Schmidt-Schaußforthegoodtimeswehad.
Finally, I would like to thank my wonderful wife Christina Steinhorst, my parents
Doris and Gerhard Steinhorst, my parents-in-law Melitta and Fred Bayer and grand-
ma Ottilia Gutermann for their patience, continuous support and for allowing me to
concentrateonmyresearchworkbymanagingmyprivateaffairs.
iiiAbstract
The objective of this thesis is to develop new methodologies for formal verification of
nonlinear analog circuits. Therefore, new approaches to discrete modeling of analog
circuits, specification of analog circuit properties and formal verification algorithms
areintroduced.
While the design flow for digital circuits is mostly automated and formalized, the
analogdesignflowstillcontainsseveralmanualsteps. Thisparticularlyappliestothe
areaofverification,whichistheprocessofsystematicallyassuringspecificationconfor-
manceofalldesignsteps. Therearetwoglobalclassesofverification approaches,rep-
resentedbyconventional non-formal verification andformal verification. Non-formal
test bench-based simulation is the state of the art in the area of analog verification in
industrial design flows. Due to the experimental character of this approach, critical
specification-violating corner-case behavior can remain unreached by the simulation
runsandtherewithundiscoveredbythedesigner.
Formal approaches to verification of analog circuits are not yet introduced into in-
dustrial design flows and still subject to research. Formal verification proves speci-
fication conformance for all possible input conditions and all possible internal states
of a circuit. Automatically proving that a model of the circuit satisfies a declarative
machine-readablepropertyspecificationisreferredtoasmodelchecking. Equivalence
checkingprovestheequivalenceoftwocircuitimplementations.
Starting from the state of the art in modeling analog circuits for simulation-based
verification, discrete modelingofanalog circuits for state space-basedformal verifica-
tionmethodologiesismotivatedinthisthesis. Theuptonowmostcapableapproachto
discretemodelingpartitionsthestatespaceintoparaxialhyperboxesofhomogeneous
behavior of the state space dynamics. Due to the paraxial slicing, the non-paraxial
vectorfielddynamicsrepresentingthestatespacedynamicscannotbesufficientlycap-
tured. Hence,thehyperbox-approachisnotrotationinvariantwithrespecttothestruc-
ture ofthestate spacedynamicswhichresultsinamassiveover-approximation ofthe
successor relation of the discrete transition model. In order to improve the discrete
modeling of analog circuits, a new trajectory-directed partitioning algorithm was de-
veloped in the scope of this thesis. This new approach determines the partitioning of
the state space parallel or orthogonal to the trajectories of the state space dynamics.
iiiAbstract
Therewith,ahighaccuracyofthesuccessorrelationisachievedincombinationwitha
lower number of states necessary for a discrete model of equal accuracy compared to
thehyperbox-approach. Themappingofthepartitioningtoadiscreteanalogtransition
structure (DATS)enablestheapplicationofformalverification algorithms.
Formalpropertyspecificationfortheinitialapproachestomodelcheckingofanalog
circuits was strongly related to temporal logic specification approaches in the digital
domain. However, specification of analogproperties such asslew rate and oscillation
isfundamentallydifferentfrom digitalpropertiessuchasfairnessandliveness. Addi-
tionally, already in the digital domain, specification by using temporal logics such as
theComputation TreeLogic(CTL)wasconsiderednottobedesigner-friendly. Hence,
specifyinganalogpropertieswithCTLcannotbeconsideredassuitableforanalogde-
signers that, in general, do not have a background in computer science. By analyzing
digital specification concepts and the existing approaches to analog property specifi-
cation, the requirements for a new specification language for analog properties have
been discussed in this thesis. On the one hand, it shall meet the requirements for for-
mal specification of verification approaches applied to DATS models. On the other
hand, the language syntax shall be oriented on natural language phrases. By syn-
thesis of these requirements, the analog specification language (ASL) was developed
in the scope of this thesis. ASL includes a natural language encapsulation of tempo-
ral logic operations, advanced operations for determination of transition paths and
oscillations, as well as arithmetic calculations on state space variable values. Hence,
a combination of high expressiveness with a designer-oriented syntax was achieved.
An extended variable concept, parameterized macros and an assertion-layer allow to
develop reusable specifications for complex analog properties. The verification algo-
rithms for model checking, that were developed in combination with ASL for appli-
cation to DATS models generated with the new trajectory-directed approach, offer a
significantenhancementcomparedtothestateoftheart.
In order to prepare a transition of signal-based to state space-based verification
methodologies, an approach to transfer transient simulation results from non-formal
testbenchsimulationflowsintoapartialstatespacerepresentation informofaDATS
has been developed in the scope of this thesis. As has been demonstrated by exam-
ples, the same ASL specification that was developed for formal model checking on
complete discrete models could be evaluated without modifications on transient sim-
ulationwaveforms.
An approach to counterexample generation for the formal ASL model checking
methodology offers to generate transition sequencesfrom a defined starting state to a
specification-violatingstateforinspectionintransientsimulationenvironments. Based
onthiscounterexamplegeneration,anewformalverificationmethodologyusingcom-
pletestatespace-coveringinputstimuliwasdeveloped. OnaDATSmodeloftheana-
log circuit, an input stimulus is determined such that all reachable states and tran-
ivAbstract
sitions of the modeled circuit are visited at least once from a defined starting state.
The generated sequence of tuples of value and time for the input variables represent
piecewise linear input stimuli for each input of the circuit. By conducting a transient
simulation with these complete state space-covering input stimuli, the circuit adopts
every state and transition that were visited during stimulus generation. An alterna-
tive formal verification methodology is given by retransferring the transient simula-
tion responses to a DATS model and by applying the ASL verification algorithms in
combinationwithanASLpropertyspecification.
Moreover, the complete state space-covering input stimuli can be applied to de-
velop a formal equivalence checking methodology. The new approach introduced in
thescopeofthisthesisreplacestheuser-definedinputstimulifrom conventionalnon-
formal equivalence checking approaches with complete-coverage stimuli. Therewith,
the equivalence of two implementations can be proven for every inner state of both
systems by comparing the transient simulation responses to the complete-coverage
stimuliofbothcircuits.
Inordertovisuallyinspecttheresultsofthenewlyintroducedverificationmethod-
ologies,anapproachtodynamicstatespacevisualizationusingmulti-parallelparticle
simulation was developed. Due to the particles being randomly distributed over the
complete state space and moving corresponding to the state space dynamics, another
perspectivetothesystem’sbehaviorisprovidedthatcoversthestatespaceandhence
offersformalresults.
The prototypic implementations of the formal ver