HECTOR: C Formal System-Level To RTL Equivalence Checking .

ATG SoCHECTOR:Formal System-Level to RTLSystem-LevelEquivalence CheckingAlfred Koelbl, Sergey Berezin, Reily Jacoby,Jerry Burch, William Nicholls, Carl PixleyAdvanced Technology GroupSynopsys, Inc.June 2008

OutlineMotivationArchitecture of HectorFrontendNotions of equivalence and interfacespecificationProof procedureSolversDebuggingCustomer resultsAdditional applicationsConclusion

MOTIVATION

System-level designSome reasons for system-level design:Faster verification at the system-levelEasier architectural explorationNo need to worry about implementation detailsProductivity gain by using High-LevelSynthesisRTL Verification problems:Verification of RTL doesn’t get any easierBugs due to faulty specificationBugs due to wrong implementation

Functional equivalence checkingSystem ModelDataRTL! "! "# !# %Result? &'(ResultSystem-level model is a transaction/word level model for thehardwareSystem and RTL compute same outputs given same inputsEquivalence checking proves functional equivalenceTiming and internal structure can differ significantly, but theobservable results must be the same

Manual (Ad hoc) FlowArchitect creates C specificationRTL designer creates RTL implementationRTL contains much more implementationdetailsProblems:Designs often embedded in own simulationenvironment, need to specify input/outputmapping, notion of equivalenceSpecification and implementation can besignificantly differentConstraints are often in designer’s head, needto be formalizedInput/output differences sometimes difficult tocapture in a formal model

High-Level Synthesis FlowEquivalence checker proves correctness ofproduced RTLYou cannot sell a high level synthesis toolwithout a verification tool!!!Advantages:All information about constraints & interfacemappings / latency differences available from thesynthesis toolHints can significantly simplify proofPush-button solution possibleProblems:Every assumption given as hint must be proven byequivalence checkerHigh-level synthesis tool must be able to producethe information

HL-Synthesis integrationWaveformHigh-Level ProofDesign C/C /RTLTimeoutProof strategyConstraints

ARCHITECTURE

ComponentsC FrontendCFGFormal modelInterface ogVHDLCompilerFormal modelFormal modelConstrainedRandom SimulatorProof t-level solverWord-level solverWaveformViewer

Front-EndC FrontendCFGFormal modelInterface ogVHDLCompilerFormal modelFormal modelConstrainedRandom SimulatorProof t-level solverWord-level solverWaveformViewer

INTERFACESPECIFICATION

Interface specificationC FrontendCFGFormal modelInterface ogVHDLCompilerFormal modelFormal modelConstrainedRandom SimulatorProof t-level solverWord-level solverWaveformViewer

Notions of equivalenceWhat does equivalence mean for comparing system-levelmodels against RTL ?Depends on how abstract the system-level model isDifferent customers, different applicationsDifferent design stylesNo definite answer (yet)Identify commonly used notions:Combinational equivalenceCycle-accurate equivalencePipelined equivalenceStream-based equivalenceTransaction equivalence ?

How to deal with different notions ?Idea: Reduction to cycle-accurate equivalencecheckRule of thumb: If you can build randompattern testbench, checking outputs on thefly, you’re safe.

Verification wrapper generationUser (or synthesis tool) provides the followinginformation:Input/output mapping between C and RTLInput constraintsOutput don’t caresMemories / memory mappingsRegister mappingsNotion of equivalence (optional)Verification wrapper is automaticallygeneratedReduces problem to cycle-accuratesequential equivalence check

PROOF PROCEDURE

Proof procedureC FrontendCFGFormal modelInterface ogVHDLCompilerFormal modelFormal modelConstrainedRandom SimulatorProof t-level solverWord-level solverWaveformViewer

Verification approachConstrained Random simulator checks for easily detectablediscrepanciesBounded formal check for harder discrepanciesFormal proof (complete):Problem reduced to sequential equivalence checkingReachability analysis would be an approachBut: Most system-level designs are arithmetic heavy,reachability infeasibleInduction proofProof idea:Implementation and specification perform same computationsNot necessarily in the same number of cyclesUnroll for the duration of a transaction, prove that symbolicexpressions are the sameProof engines:Bit-level equivalence checkers (SAT, BDDs)Word-level rewriting engine for arithmetic (COMBAT)Hybrid (word & bit) engine for orchestrationPEP’s

Induction proofTransaction equivalenceAssume that designs start in valid state (superset ofreachable state set)Execute single transaction by unrolling ESL and RTLmodels for one transactionCheck outputs after transactionCheck state after transactionProof strategy: InductionNeeds state invariantsRegister mappingsMemory mappings & memory constraintsAdditional invariantsProve that resulting SAT formula is UNSAT

Transaction equivalenceIAOAESLMASAMBSBRTLOBIB

Transaction on TATransaction TBMBSBRTL0RTL1RTL2MB’SB’OBIB0IB1IB2

Transaction equivalenceIA0IA1OAESL0MASAESL1Valid starting state(superset of reachable state set)MBSBRTL0MA’SA’Outputs equivalent ?RTL1RTL2 MB’SB’OBIB0IB1IB2

Transaction equivalenceIA0IA1OAESL0MASAESL1MA’SA’ Register mappings State invariants Memory mappings Constraints on memoriesMBSBRTL0Valid end state ?RTL1RTL2MB’SB’OBIB0IB1IB2

Proof procedureAssumptionsa0 MM0(MA, MB) MM1(MA, MB)a1 c0(MA, MB) c1(MA, MB)a2 r0(SA, SB) r1(SA, SB)a3 i0(MA, MB, SA, SB)Proof obligationsa0 a1 a2a0 a1 a2a0 a1 a2a3a3a3MM0(M A, M B)c0(M A, M B)r0(S A, S B)a0 a1 a2a0 a1 a2a3a3i0(M A, M B, S A, S B)OA OBCheck model assumptions, e.g., that no array accesses areout-of-bounds

SOLVERS

SolversC FrontendCFGFormal modelInterface ogVHDLCompilerFormal modelFormal modelConstrainedRandom SimulatorProof t-level solverWord-level solverWaveformViewer

Decision ProceduresCore technology for formal reasoningFormulaDecisionProcedureSatisfying solution(Counter-example)Used for intermediate equivalencesUsed for output equivalencesWord-level solversUnsatisfiable(Proof)Good for equivalent arithmeticBad for producing counter-examplesBit-level solversGood for falsificationBad for arithmetic

Equivalence check of two DFGs1.2.3.4.Find potentially equivalent points (PEPs) (e.g. by simulation)Prove them equivalent using bit- and word-level enginesMerge equivalent points thereby increasing sharingProve outputs equivalentC Oa ?RTLOb

Equivalence check of two DFGs1.2.3.4.Find potentially equivalent points (PEPs) (e.g. by simulation)Prove them equivalent using bit- and word-level enginesMerge equivalent points thereby increasing sharingProve outputs equivalentC ? RTL

Word-level solversSMT solvers (SAT module theories)Reason about arithmeticTheories for linear arithmetic, bit-vectors,uninterpreted functions, arrays, real arithmeticNeed to be able to deal with finite word-sizesRe-writing enginesRe-write formulas into normal-formConvergence can be an issueCVCLite from StanfordLessons learned:Only Bit-Vector theory (and maybe theory of arraysif powerful enough) usefulMany abstraction techniques are only useful forproperty checkingFew solver techniques specifically targetequivalence checking problem

Bit-level solversConstruct Boolean circuit based on bit-levelrepresentation of operationsBDDsCanonical representation, very easy to check ifformula is unsatisfiableTendency to memory blowupGood for local intermediate equivalencesGood for XOR treesSATConvert circuit to Conjunctive Normal Form (CNF)Branch-and-bound searchEfficient optimizations (conflict analysis, nonchronological backtracking)ATPG / Circuit-based SATBranch-and-bound search directly on Booleancircuit

Solver technologyCompare word-level graphs modulo zeroextension / sign-extension and mergeintermediate equivalent points? 32cast324 32cast 32cast3in a3in b

Solver technologyCompare word-level graphs modulo zeroextension / sign-extension and mergeintermediate equivalent points324cast 3in a3in b

Solver technologyCompare word-level graphs moduloobservabilityo1c11c200Observable(a) - (a b)(c1 & c2) - (a b)a b

Solver technologyCompare word-level graphs moduloobservabilityo1c1c2100bReplace ‘a’ by ‘b’

Effectiveness comes from many techniques68 word (as opposed to bit) outputsSL – RTL : different data path architecturesDifferent multiplier implementationsDifferent adder tree structureDFG nodes: 14005 estration18 unsolved52 unsolved0 unsolved

The Algebraic Solver StrategySplit casesNormal formAlgebraicRewritesProof tsimplificationsSATsolverWhen all elsefails.{ (x *[32] y)[31:16] , x *[16] y } { (x *[32] y)[31:16] , (x *[32] y)[15:0] } x *[32] y

CUSTOMEREXPERIENCES

COMPANYB

Experience w. Company BAd Hoc (manual) design flowAll modules are parts of a router designCustomer wanted free consulting.ProblemsCustomer did not do block-level verificationConstraint/counterexample loopManager did not understand the idea of equivalencechecking—he thought Hector was a bug finderWe did the work but eventually the customer couldrun Hector by herselfC model not entirely complete: one case of twomodules in RTL and one in the C Abstracted away the simulation environmentmanually

Experience w. Company BCore algorithms improved greatly duringevaluationDeveloped different memory models, e.g.,TCAM.SuccessesWere able to conclusively compare all outputsThe D5 was not completed by customer

Hector experimental resultsDesign# lines ofcodeD1C50RTL6200D270D3# arrays #disc #bugs# rams repan foundciestimefinal 1 RTL1 C 4minprovenD4170075004/481 RTL1 C 1hprovenD54300670031 / 33 404 RTL43min62 proven,15 cex

COMPANYN

Experience w. Company NAd Hoc (manual) design flowAll modules were from an arithmetic unit: bothinteger and floating pointGPU designC models act as reference models to provideexpected/correct output valuesCoverage metrics help but not always reliablebugs missedCustomer was very experienced with formalmethods.

Experience w. Company NMany mismatches are foundReal design bugs were caughtmostly corner casesC model bugs were foundRaised questions on the definition of correctbehaviorSpecification documents clarified/modifiedSome instructions are proven automatically bythe tool without any human assistanceSome instructions are too complex or too largefor the tool to handleSeveral techniques for the user to try to assistthe toolThe main theme is divide-and-conquer

Experience w. Company NDue to the initial success in finding bugs andproving correctness, the use of high levelequivalence checking expands to several designsof company’s active GPU development project10 design blocks, 119 sessions set up and run, 107proven (some after fixes to bugs found by FV)Includes multiplication logicFocused on designs with a high probability ofsuccessdata transform with simple temporal behavior andinput constraintsA bug was found in a previous project that wouldhave been caught by running thisa special case only affects a single input value

Experience w. Company NHigh-level equivalence checking will becomepart of company’s verification planDemonstrated its value for suitable designsIncrease confidence and find difficult bugsmore quicklyWill not replace other forms of verification,complementary to existing methodology

COMPANYT

Experience w. Company TDesigns generated automatically from C bySynfora synthesis toolFour designs from four different encryptionalgorithms fir filterAll four had streamsDesigns were run entirely automatically!Put in scripting capability to toolSynfora gave Hector hints—all were checkedindependentlyHad to support many Synfora features such asstreams, bit width pragmas, loop unrollpragmas, memoriesHector can now handle loops withoutunrolling.

Behavioral synthesis resultSynfora Pico-Extreme synthesized designsEncryption designs for GSM/GPRS/UMTSprotocolsDesignDS1# lines ofcodeCRTL2935663DS2579DS3DS4# arrays #disc #bugs# rams repan foundciestimefinal 2/22021minproven931452744/42019minproven

ADDITIONALAPPLICATIONS