Verifying Programs with BDDsVerifying Programs with BDDsTopicsTopics Representing Boolean functions with Binary Decision Diagrams Application to program verificationclass-bdd.ppt15-213“The course that gives CMU its Zip!”15-213, F’08–2–Verification ExampleVerification ExampleDo these functions produce Do these functions produce identical results?identical results?How could you find out?How could you find out?How about exhaustive testing?How about exhaustive testing?int abs(int x) {int mask = x>>31;return (x ^ mask) + ~mask + 1;}int test_abs(int x) {return (x < 0) ? -x : x; }–3–More ExamplesMore Examplesint addXY(int x, int y){return x+y;}int addYX(int x, int y){return y+x;}?=int mulXY(int x, int y){return x*y;}int mulYX(int x, int y){return y*x;}?=–4–How Can We Verify Programs?How Can We Verify Programs?TestingTesting Exhaustive testing not generally feasible Currently, programs only tested over small fraction of possible casesFormal VerificationFormal Verification Mathematical “proof” that code is correct Did Pythagoras show that a2+ b2= c2by testing?abc–5–Bit-Level Program VerificationBit-Level Program Verification View computer word as 32 separate bit values Each output becomes Boolean function of inputsabsx0x1x2•••x31y0y1y2•••y31••••••x0x1x2•••x31•••yiabsiint abs(int x) {int mask = x>>31;return (x ^ mask) + ~mask + 1;}–6–Extracting Boolean RepresentationExtracting Boolean RepresentationDo these functions produce Do these functions produce identical results?identical results?int bitOr(int x, int y){return ~(~x & ~y);}int test_bitOr(int x, int y){return x | y;}yxv1 = ~xv2 = ~yv3 = v1 & v2v4 = ~v3v5 = x | yt = v4 == v5Straight-Line Evaluation–7–Tabular Function RepresentationTabular Function Representation List every possible function valueComplexityComplexity Function with n variables00001111001100110101010100010101x1x2x3f–8–Algebraic Function RepresentationAlgebraic Function Representation f(x1, x2, x3) = (x1+ x2) · x3 Boolean AlgebraComplexityComplexity Representation Determining properties of functionz E.g., deciding whether two expressions are equivalent00001111001100110101010100010101x1x2x3fx1·x3x2·x3–9–Tree RepresentationTree RepresentationTruth Table Decision Tree Vertex represents decision Follow green (dashed) line for value 0 Follow red (solid) line for value 1 Function value determined by leaf valueComplexityComplexity0 0x30 1x3x20 1x30 1x3x2x100001111001100110101010100010101x1x2x3f–10–Ordered Binary Decision DiagramsOrdered Binary Decision DiagramsInitial Tree Reduced GraphCanonical representation of Boolean functionCanonical representation of Boolean function Two functions equivalent if and only if graphs isomorphicz Can be tested in linear time Desirable property: simplest form is canonical.x20 1x3x10 0x30 1x3x20 1x30 1x3x2x1(x1+ x2) · x3–11–Example FunctionsExample FunctionsConstantsUnique unsatisfiable functionUnique tautology10VariableTreat variableas function0 1xOdd ParityLinearrepresentationx2x3x410x4x3x2x1Typical Functionx20 1x4x1 (x1 + x2) · x4 No vertex labeled x3 independent of x3 Many subgraphs shared –12–More Complex FunctionsMore Complex Functionsb3b3a3Coutb3b2b2a2b2b2a2b3a3S3b2b1b1a1b1b1a1b2a2S2b1a0a0b1a1S1b010b0a0S0FunctionsFunctions Add 4-bit words a and b Get 4-bit sum S Carry output bit CoutShared RepresentationShared Representation Graph with multiple roots 31 nodes for 4-bit adder 571 nodes for 64-bit adder Linear growth!–13–Symbolic ExecutionSymbolic Execution(3-bit word size)xx210x110x010yy210y110y010v1 = ~xx201x101x001v2 = ~yy201y101y001–14–Symbolic Execution (cont.)Symbolic Execution (cont.)v3 = v1 & v2x2y201x1y101x0y001v4 = ~v3x2y210x1y110x0y010v5 = x | yx2y210x1y110x0y010t = v4 == v51–15–Counterexample GenerationCounterexample GenerationFind values of Find values of xx& & yyfor which for which these programs produce these programs produce different resultsdifferent resultsint bitOr(int x, int y){return ~(~x & ~y);}int bitXor(int x, int y){return x ^ y;}yxv1 = ~xv2 = ~yv3 = v1 & v2v4 = ~v3v5 = x ^ yt = v4 == v5Straight-Line Evaluation–16–Symbolic ExecutionSymbolic Executionv4 = ~v3x2y210x1y110x0y010v5 = x ^ yx2y210y2x1y110y1x0y010y0t = v4 == v5x2y2x1y1x0y001x = 111y = 001–17–Performance: GoodPerformance: Goodint addXY(int x, int y){return x+y;}int addYX(int x, int y){return y+x;}010020030040050060070080090010000 8 16 24 32Word SizeSecondsEnumerateBDD–18–Performance: BadPerformance: Badint mulXY(int x, int y){return x*y;}int mulYX(int x, int y){return y*x;}010020030040050060070080090010000 8 16 24 32Word SizeSecondsEnumerateBDD–19–Why Is Multiplication Slow?Why Is Multiplication Slow?Multiplication function intractable for BDDsz Exponential growth, regardless of variable ordering1456041881552144MultMultAddAddBitsBitsMultiplication-4Add-4Node Counts–20–What if Multiplication were Easy?What if Multiplication were Easy?int factorK(int x, int y){int K = XXXX...X;int rangeOK =1 < x && x <= y;int factorOK =x*y == K;return!(rangeOK && factorOK);}int one(int x, int y){return 1;}–21–Dealing with ConditionalsDealing with ConditionalsDuring Evaluation, Keep Track of:During Evaluation, Keep Track of: Current Context: Under what condition would code be evaluated Definedness (for each variable)z Has it been assigned a valueint abs(int x){int r;if (x < 0)r = -x;elser = x;return r;}t1 = x<0xv1 = -xr = v1v2 = rr = x11t1t11!t1000t111000t1?v1:0t1?v1:xt1?v1:xContextrdefinedrvalue–22–Dealing with LoopsDealing with LoopsUnrollUnroll Turn into bounded sequence of conditionalsz Default limit = 33 Signal runtime error if don’t complete within limitint ilog2(unsigned x){int r = -1;while (x) {r++; x >>= 1;}return r;}int ilog2(unsigned x){int r = -1;if (x) {r++; x >>= 1;} else return r;if (x) {r++; x >>= 1;} else return r;. . .if (x) {r++; x >>= 1;} else return r;error();}Unrolled–23–EvaluationEvaluationStrengthsStrengths Provides 100% guarantee of correctness Performance very good for simple arithmetic functionsWeaknessesWeaknesses Important integer functions have exponential blowup Not practical for programs that build and operate on large data structures–24–Some HistorySome HistoryOriginsOrigins Lee 1959, Akers 1976z Idea of representing Boolean function as BDD Hopcroft, Fortune, Schmidt 1978z
View Full Document