1 Lectures Formal verification of SoC designs (targeting logic verification only) Masahiro Fujita VLSI Design and Education Center (VDEC) University of Tokyo [email protected] 2 Table of contents Introduction to SoC verification (Lecture 1) Backgrounds technology in formal verification: Methods for reasoning about mathematical models (Lecture 2) Basic formal verification techniques Boolean function (Propositional logic) SAT (Satisfiability checker) BDD (Binary Decision Diagrams) Use of first-order and higher-order logic Logic of uninterpreted functions with equality Theorem proving methods Equivalence checking (Lecture 3) Combinational Sequential Model (property) checking (Lecture 4) Explicit/implicit state based Bounded model checking Real formal verification tools Enhancing Formal Verification Capacity (Lecture 5) Abstraction-refinement Assume guarantee/Compositional Reasoning Approximation Symmetry reduction Partial Order Reduction Industrial and Research Tool Offerings Semi-formal verification techniques (Lecture 6) Advanced topics System level formal verification (Lecture 7) Synchronization verification Equivalence checking for C programs 3 Lecture 1: Introduction to SoC verification System-on-Chip (SOC) design Increase of design complexity Move to higher levels of abstraction Level Number of components 1E0 System level 1E2 1E3 RTL Gate 1E4 1E5 1E6 Transistor 1E7 Accuracy Algorithm Abstraction 1E1 4 System-on-Chip (SoC) design Specification to architecture and down to implementation Behavior (functional) to structure System level: system specification to system architecture RT/IS level: component behavior to component micro-architecture µProcessor Control IF FSM IP Netlist IP Comp. Memory Pipeline RAM State PC Interface Interface IR Control Bus Interface Processors IPs Memories Busses Interface Memory Registers ALUs/FUs Memories Gates State Datapath Mem RF IF FSM Memory State ALU Custom HW Specification + constraints System architecture + estimates RTL/IS Implementation + results 5 Verification challenge Simulation/Design Verification 51% Design Creation 32% Place & Route 32% Post Layout Optimization 26% Parasitic Extraction 17% System on Chip 17% Design Rule Checking 17% Static Timing Analysis 16% Synthesis 15% Delay Calculation 13% 0% 10% 20% 30% 40% 50% 60% Bottlenecks in Design Cycles: Survey of 545 engineers by EETIMES 2000 6 System-level design & verification System-level RTL Transistor level Bugs fix time 3 minutes delay 3 days delay 3 weeks delay Cost due to the delay/late time-to-market revenue loss Remove as many bugs as possible in the earlier stages Do not introduce new design errors when refining designs Formal verification in system-level designs: Property checking and equivalence checking 7 Design representation in higher level Super state: Need multiple cycles for executions Variables, functions: Boolean ⇒ Integer, Term rewriting Op1 PS1 Op2 PS2 SFSMD model Op4 a = 42; while (a<100) { b = b + a; if (b > 50) c = c + d; a = a + c; } PS3 Op1 S1 Op3 Op2 Op5 Op6 Op3 S2 Op4 S3 Op5 FSMD model Op6 Establish mapping Control circuits Datapath circuits 8 Verification methods: simulation/emulation Simulation Traditional, basic, and flexible technique Applicable at any design levels Difficulties in preparing “good” simulation patterns Getting harder to cover corner cases Emulation Can handle software simultaneously Cost and time for preparation: not ignorable Corner case problems still remain 9 Why formal verification? Traditional method (testing & simulation) Formal Verification Test properties Deadlock ... Test vectors Design Under Test Patterned vectors Cannot cover all possible cases Possibility of surviving subtle (corner case) bugs True or False Find counter-example System Model Test results Equivalent to simulating all cases in simulation No bug (according to the property) Property (model) checking and Equivalence checking 10 Formal verification “Prove” the correctness of designs Possible mathematical models Both design and spec must be represented with mathematical models Mathematical reasoning Equivalent to “all cases” simulations Boolean function (Propositional logic) How to represent and manipulate on computers First-order logic Need to represent “high level” designs Higher-order logic Theorem proving = Interactive method Front-end is also very important Often, it determines the total performance of the tools Spec Design Front-end tool Mathematical models Verification engines 11 Formal vs simulation based verification Example: Verification of Exclusive-OR circuits: z = ~x&y + x&~y ( ‘~’ means compliment) b x G2 a G4 G1 y G3 c z 12 Example: Formal vs simulation (Cont.) Verification of Exclusive-OR circuit with “simulation” z and ~x&y+x&~y are equal for all four cases Need to simulate 2**N cases where N is #ins x y 0 0 1 1 0 1 0 1 z ~x&y+x&~y 0 1 1 0 0 1 1 0 b x a y z c 13 Example: Formal vs simulation (Cont.) Verification of Exclusive-OR circuit with “formal verification” b z = ~b + ~c x b = ~x + ~a a c = ~a + ~y a = ~x + ~y z = ~b + ~c y c = ~(~x + ~a) + ~(~a + ~y) = a&x + a&y = (~x + ~y)&x + (~x + ~y)&y = x&~y + ~x&y Axiomatic and mathematical transformation of expressions to reach the specification This is a mathematical proof ! z RTL Simulation Semantics D delay model 4 valued logic is usually used (0, 1, X, Z) more complex logic possible e.g. std_logic_vector in VHDL Blocking and Non-blocking assignments using syntax each operation takes negligible time operations are scheduled in terms of clock boundaries explicitly specified delay may be used functional simulation may be different from later stage timing simulation blocking assignments are sequentially executed non blocking assignments are executed in parallel at end of a clock boundary Value Change Dump (VCD) file captures changes in values of variables with time Event-driven Simulation Event: change in logic value at a node, at a certain instant of time (V,T) Event-driven: only considers active nodes Performs both timing and functional verification Efficient All nodes are visible Glitches are detected Most heavily used and well-suited for all types of designs Event-driven Simulation 1 1 0 0 a c D=2 1 1 1 e D=1 b 0 0 3 4 6 d 1 0 5 e(4)=0 b(1)=1 d(5)=1 d(5)=1 c(3)=0 d(5)=1 d(5)=1 e(6)=1 Cycle-based Simulation Take advantage of the fact that most digital designs are largely synchronous L a t c h e s Boundary Node Internal Node L a t c h e s Synchronous circuit: state elements change value on active edge of clock Only boundary nodes are evaluated Compute steady-state response of the circuit at each clock cycle at each boundary node Simulation CAD Tools Event-driven simulators Synopsys VCS, Sirocco VCS is a fast Verilog simulator Sirocco is a VHDL simulator Cadence NCSim (VHDL, Verilog, mixed) Model Tech. Modelsim (VHDL, Verilog, mixed) Cycle-based simulators Quickturn SpeedSim (VHDL) Synopsys PureSpeed (Verilog) Cadence Cobra Debugging Tools VCD dump viewer e.g. Cadence Signalscan clk a b bus[0:3] time xxxx 0 10 5H 20 3H 30 40 50 Integrated debugging environment more sophisticated tool cross references code, VCD waveform viewer, coverage analysis etc. integrates software debug features and hardware debug features e.g. Novas Software Debussy Lecture 2: Backgrounds technology in formal verification Methods for reasoning about mathematical models Boolean function (Propositional logic) SAT (Satisfiability checker) BDD (Binary Decision Diagrams) First-order logic Logic of uninterpreted functions with equality Higher-order logic Theorem proving = Interactive method (skipped in this tutorial) Spec 20 Design Front-end tool Mathematical models Verification engines 21 SAT Problem definition Given a CNF formula, f : (a,b,c) A set of variables, V Conjunction of clauses (C1,C2,C3) Each clause: disjunction of literals over V Does there exist an assignment of Boolean values to the variables, V which sets at least one literal in each clause to ‘1’ ? Example : (a b c)( a c)( a b c) C1 C2 C3 a=b=c=1 22 DPLL algorithm for SAT [Davis, Putnam, Logemann, Loveland 1960,62] Given : CNF formula f(v1,v2,..,vk) , and an ordering function Next_Variable Example : 0 (a b)( a c)( a b) C1 C2 C3 CONFLICT! 0 b a 1 0 1 c 1 SAT! C1 C3 C2 23 DPLL algorithm: Unit clause rule Rule: Assign to true any single literal clauses. (a b c) = = c=1 0 0 Apply Iteratively: Boolean Constraint Propagation (BCP) a (a c)( b c)( a b c)( c e)( d e)( c d e) c(b c)( c e)( d e)( c d e) e( d e ) 24 Anatomy of a modern SAT solver DPLL Algorithm Clause database management Discard useless clauses (e.g. inactive or large clauses) Efficient BCP Search Restarts SAT Solver To correct for bad choices in variable ordering Restart algorithm “periodically” Efficient garbage collection Retain some/all recorded clauses Conflict-driven learning 25 Conflict driven search pruning (GRASP) Silva & Sakallah ‘95 x1 Non-chronological backtracking Conflict-clause recording x2 2 xj SAT xk-1 xk 1 26 Conflict analysis: An example Current Assignment: {x9 0 @1, x10 0 @ 3, x11 0 @ 3, x12 1@ 2, x13 1@ 2} Decision Assignment: ( x1 x 2) 2 ( x1 x 3 x 9) 3 ( x 2 x 3 x 4) 4 ( x 4 x 5 x10) {x1 1@ 6} 5 ( x 4 x 6 x11) 6 ( x 5 x 6) 7 ( x1 x 7 x12) 8 ( x1 x8) 9 ( x 7 x8 x13) 27 Example continued: Implication graph x2= [email protected] 1 x1= [email protected] 2 2 3 3 x3= [email protected] x9= [email protected] x10= [email protected] 4 4 x5= [email protected] 6 x4= [email protected] 5 6 5 x6= [email protected] x11= [email protected] c( ( x1 x 9 x10 x11) 28 Example continued…. x9= [email protected] x8= [email protected] 8 9 x1= [email protected] x10= [email protected] x11= [email protected] 7 7 x12= [email protected] ` 9 Decision Level 9 3 x13= [email protected] 5 x7= [email protected] x1 6 29 Variable ordering Significantly impacts size of search tree Ordering schemes can be static or dymamic Conventional wisdom (pre-chaff): Satisfy most number of clauses OR Maximize BCP e.g. DLIS, MOMs, BOHMs etc. 30 Variable ordering: New ideas New wisdom: Recorded clauses key in guiding search Conflict-driven variable ordering: Semi-static in nature, for efficiency Chaff (DAC’01): Pick var. appearing in most number of recent conflict clauses BerkMin (DATE’02): Pick var. involved in most number of recent conflicts Statistics updated on each conflict Side-effect: Better cache behavior 31 Efficient Boolean Constraint Propagation Observation: BCP almost 80% of compute time, under clause recording Traditional implementation: Each clause: Counter for #literals set to false Assgn. to variable ‘x’: Update all clauses having x, x New Idea: Only need to monitor event when # free literals in a clause goes from 2 to 1 Need to watch only 2 literals per clause : SATO (Zhang’97),Chaff (DAC’01) x1 … w1 … w2 … xk 32 SAT solvers today Capacity: Formulas upto a million variables and 3-4 million clauses can be solved in few hours Only for structured instances e.g. derived from real-world circuits & systems Tool offerings: Public domain GRASP : Univ. of Michigan SATO: Univ. of Iowa zChaff: Princeton University BerkMin: Cadence Berkeley Labs. Commercial PROVER: Prover Technologies 33 Binary Decision Diagram: Decision structures Truth Table x1 x2 x3 0 0 0 0 1 1 1 1 0 0 1 1 0 0 1 1 0 1 0 1 0 1 0 1 Decision Tree x1 f 0 0 0 1 0 1 0 1 x2 x3 0 x2 x3 0 0 x3 1 0 x3 1 0 1 Vertex represents decision Follow green (dashed) line for value 0 Follow red (solid) line for value 1 Function value determined by leaf value Source: Prof. Randal Bryant 34 Variable ordering Assign arbitrary total ordering to variables e.g. x1 < x2 < x3 Variables must appear in ascending order along all paths Not OK OK x1 x1 x1 x2 x2 x3 x3 x3 x1 x1 Properties No conflicting variable assignments along path Simplifies manipulation 35 Reducing OBDDs: Rule #1 Eliminate duplicate terminals 1 1 1 x1 x1 x2 x3 0 x2 x3 0 0 x2 x3 1 0 x3 1 0 x3 1 x2 x3 0 x3 x3 1 36 Reducing OBDDs: Rule #2 Merge isomorphic nodes, i.e. nodes that reference the same variable and point to the same successors a 0 1 0 a a 1 b c 0 b x1 x2 x3 0 c x1 x2 x3 1 x3 x3 1 x2 x2 x3 x3 0 1 37 Reducing OBDDs: Rule #3 Eliminate a node if its 0 and 1 edges lead to the same node a 0 1 b 0 b 0 1 1 x1 x1 x2 x2 x3 x3 0 1 x2 x3 0 1 38 Example OBDD Reduced Graph Initial Graph x1 x1 x2 x3 0 0 0 x2 x2 x3 x3 1 0 x3 x3 1 (x1 +x2 )· x3 0 1 0 1 Canonical representation of Boolean function For given variable ordering Two functions equivalent if and only if graphs isomorphic Can be tested in linear time Desirable property: simplest form is canonical. 39 From circuits to BDD X1 G2 G4 G1 X2 G3 X1 0 1 1 X2 0 0 X1 X1 1 0 X2 1 1 1 0 1 0 X2 0 0 1 0 X1 0 0 X2 1 1 1 0 X1 1 0 0 1 X2 X2 0 1 0 1 1 0 1 40 Effect of variable ordering (a1 b1) (a2 b2 ) (a3 b3 ) Good Ordering Bad Ordering a1 a1 b1 a2 a2 a3 a2 a3 a3 b2 b1 b1 b1 b1 a3 b2 b2 b3 0 a3 b3 1 Linear Growth 0 1 Exponential Growth 41 ROBDD sizes & variable ordering Bad News Good News Finding optimal variable ordering NP-Hard Some functions have exponential BDD size for all orders e.g. multiplier Many functions/tasks have reasonable size ROBDDs Algorithms remain practical up to 500,000 node OBDDs Heuristic ordering methods generally satisfactory What works in Practice Application-specific heuristics e.g. DFS-based ordering for combinational circuits Dynamic ordering based on variable sifting (R. Rudell) 42 Variants of decision diagrams Multiterminal BDDs (MTBDD) – Pseudo Boolean functions Bn N, terminal nodes are integers Ordered Kronecker FunctionalDecision Diagrams (OKFDD) – uses XOR in OBDDs Binary Moment Diagrams (BMD) – good for arithmetic operations and word-level representation Zero-suppressed BDD (ZDD) – good for representing sparse sets Partitioned OBDDs (POBDD) – highly compact representation which retains most of the features of ROBDDs BDD packages – CUDD from Univ. of Colorado, Boulder, CMU BDD package from Carnegie Mellon Univ. In addition, companies like Intel, Fujitsu, Motorola etc. have their own internal BDD packages 43 Symbolic logic Symbolic logic deals with the structure of reasoning It defines ways to deal with relationships between concepts Provides ways to compose proofs of statements Provides ways to express statements in a precise, compact and symbolic manner More precisely, a formal symbolic logic consists of A notation (symbols and syntax) A set of axioms (facts) A set of inference rules (deduction scheme) 44 Types of symbolic logic Propositional Logic – commonly known as Boolean algebra First Order Logic Variables in this algebra {0,1} Existential () and Universal () quantifiers over variables Higher Order Logic Existential and Universal quantification over sets and functions 45 Key features of a theory Expressiveness Completeness All valid formulas are provable Decidability What kind of statements can be written in the theory There exists an algorithm to deduce the truth of any formula in the theory Comparison of types of logic Propositional Least expressive, decidable, complete First Order Logic More expressive, decidable, not complete Higher Order Logic Most expressive, not decidable, not complete 46 First-order logic First-Order Logic theory in symbolic logic formalizes quantified statements E.g: “there exists an object such that…” or “for all objects, it is the case that…” Statements in first-order logic built using: Variables x, y Constants 0, C, Functions f (x ), x + y Predicates p (x ), x > y, x = y Boolean connectives , , , Quantifiers , 47 First-order theories A first-order theory a set of first-order statements about a related set of constants, functions, and predicates. Example: A theory of arithmetic might include the following statements about 0 and +: x. ( x + 0 = x ) x,y. (x + y = y + x ) 48 Validity of an expression in a theory Given A theory and an expression Using Building blocks of that theory If expression evaluates to true for every evaluation, then it is valid in the theory Example: X >= 0 is a valid expression in positive real arithmetic 49 Validity checking & undecidability Given a theory in first-order logic and an expression we wish to prove that is valid in Validity of in is written as |= Undecidability of FOL A well-known result states that in general it is undecidable whether a FOL formula is valid in a given first-order theory However with appropriate restrictions on and the theory can be made decidable and practical programs can be built around Many practical problems can be posed as formulas in a certain theory or a combination of theories A proof of validity of this formula results in a solution to the problem Example Scheduling of complex operations in a manufacturing plant 50 Proof system A formal proof in a theory Rewrite rules Deal with mechanical massaging of statements irrespective of the meaning of the statements Key requirement of a proof system A set of steps of statements A statement is derived from a previous statement using a set of defined inference rules Soundness : All provable formulas are logically true! A proof system need not be complete or decidable in order to be useful! 51 Automated vs. interactive theorem proving John Rushby, SRI, asserts “There are no fully automatic theorem provers”. For best performance most theorem provers require user guidance Variable ordering, weighting of literals, function symbols, strategy selection, orientation of equations, invention of ordering lemmas, induction hints Automation in certain domains Propositional logic using SAT solvers, BDDs Linear arithmetic – integer/linear programming Temporal logic – model checking Induction (Boyer-Moore heuristics) 52 Example theorem prover: PVS • Owre et al., 1992 at SRI System model PVS File Proofs Formulae To be proved • System model is translated either automatically or manually • Formulae to be proved are also translated from their native forms • Proofs are usually carried out interactively A 53 PVS Methodology Automate everything that is decidable Heuristic automation for obvious cases for other problems Propositional calculus, linear arithmetic, finitestate model checking Hashing conditional rewriter integrated with decision procedures Instantiation, induction Human control for things difficult to automate Sequent calculus presentation Tactic language for defining higher-level proof strategies 54 Stanford validity checker (SVC) Started with applications to processor verification [Burch and Dill ‘94] [Jones et al. ‘95] Applications since release Symbolic simulation [Su et al. ‘98] Software specification checking [Park et al. ‘98] Infinite-state model checking [Das and Dill ‘01] Theorem prover proof assistance [Heilmann ‘99] Integration into programming languages [Day et al. ‘99] 55 Overall flow of SVC Given an expression whose validity has to be checked Choose an atomic formula ƒ in the expression Case split on the atomic formula Create two subformulas, for ƒ = 0, and ƒ = 1 Simplify the two subformulas Iteratively check the validity of the two subformulas Example: ( x < y) (y < x) (x=y) Choose f = ( x < y ) Case split on f to get two subformulas ( true ) ( y < x ) Simplify ( false ) ( y < x ) ( x = y ) true Simplify (y < x) (x=y) 56 Example (continued) (y < x) (x=y) Choose f = ( y < x ) Case splitting gives two subformulas true ( x = y ) Simplify false ( x = y ) Simplify true (x=y) Case splitting on f = ( x = y ) gives two subformulas true and false The only false node is formula: (x y) (y x) (x y) If this formula can be proved unsatisfiable by theory then formula is a tautology Decision procedure for higher level designs: Uninterpreted functions with equality Ignore each functionality in the functions It is called Logic of Uninterpreted Functions Arithmetic operations are handled as symbols Fucntion returns a value If the arguments are the same, it returns the same value (a=b)(x=y) [f(a,x)=f(b,y)] x y 1 f c Y Y:= if c then x else f(x,y) 0 Very useful for analysis of symbolic simulation results Equivalence checking: Both send f(b) to x Design1: if a=b then x <- f(a) else x <- f(b) Design2: x<- f(b) Transform into formulae Design1: ((a=b)->(x’=f(a)))&((~(a=b)->(x’=f(b))) Design2: x’=f(b) Decision procedure similar to SAT confirms Design1=Design2 57 58 How is validity checking done? The validity checker is built on top of a core decision procedure for satisfiability in a theory of a set of literals in the theory A literal is an atomic formula or its negation The core decision procedure depends on the theory e.g. a Satisfiability Solver can be used for Propositional Logic SVC proposes use of several decision theories targeted to several theories gives the strongest decision procedure 59 Need for Multiple Theories Why are multiple theories needed? Most real-life problems when cast into a problem of proving validity of a formula span a set of theories Propositional logic Bit-vectors and arrays Real, linear arithmetic Uninterpreted functions & predicates A decision procedure is a combination of theories must be able to combine decision procedures that reason in each of these theories! 60 Basic formal verification techniques Equivalence checking: Basics and real tools (Lecture 3) Combinational Sequential Model (property) checking: Basics (Lecture 4) Explicit/implicit state based Bounded model checking Formal Equivalence Checking Given two designs, prove that for all possible input stimuli their corresponding outputs are equivalent Design A =? Yes/No Input Design B Product Machine 61 62 Formal equivalence checking: The targets Equivalence checking can be applied at or across various levels System Level Gate Level Device Level RTL 63 Combinational Equivalence Checking (CEC) Currently most practical and pervasive equivalence checking technology Nearly full automation possible Designs of up to several million gates verified in a few hours or minutes Hierarchical verification deployed Full chip verification possible Key methodology: Convert sequential equivalence checking to a CEC problem! Match Latches & extract comb. portions for EC CEC in Today’s ASIC Design Flow RTL Design Synthesis & optimization CEC Routing CEC DFT insertion CEC IO Insertion CEC Placement Clock tree synthesis 64 CEC CEC ECO 65 CIRCUIT 1 Solving Seq. EC as Comb. EC PI Comb. Logic PS1 PO NS1 PI MATCH LATCHES CIRCUIT 2 Combinational Equiv. Checking PS PS2 PI Comb. Logic NS2 PO PO Comb. Logic 1 NS Comb. Logic 2 NS ? PO = 66 CIRCUIT 1 Combinational EC with BDD and SAT PI Comb. Logic PS1 PO NS1 PI MATCH LATCHES CIRCUIT 2 Combinational Equiv. Checking PS PS2 PI Comb. Logic PO Comb. Logic 1 NS Comb. Logic 2 NS ? PO = NS2 PO Represent logic functions for this entire circuit with BDD or SAT 67 Methods for Latch Mapping Incomplete Methods Regular expression-based using latch names Using simulation (Cho & Pixley ‘97): Group latches with identical simulation signatures Group based on structural considerations e.g. cone of influence Incomplete run of complete method below (Anastasakis et al DAC ‘02) Complete Methods Functional fixed-point iteration based on Van Eijk’s algorithm (van Eijk ’95) Van Eijk’s Method for Latch Mapping Initial Latch Mapping Approximation PI Apply Latch Mapping Assumptions Iterate PS No Comb. Logic 1 NS Comb. Logic 2 NS ? = Fixed-point ? Yes Done !! Verify Latch Mapping Assumptions 68 69 If-Then-Else operation Concept Basic technique for building OBDD from logic network or formula. Arguments I, T, E I T, E I X T 1 M UX E 0 Functions over variables X Represented as OBDDs Result OBDD representing composite function (I T) (I E) 70 If-Then-Else execution example Argument I Argument T Argument E Recursive Calls 1 a B1 A1,B1 A1 a A2,B2 A2 b c A6 A3 d A4 0 A3,B2 B2 d 1 A5 A6,B2 A6,B5 c B5 B3 0 1 B4 A5,B2 A3,B4 A4,B3 A5,B4 Optimizations Dynamic programming Early termination rules Apply reduction rules bottom-up as return from recursive calls (Recursive calling structure implicitly defines unreduced BDD) 71 Derived algebraic operations Other operations can be expressed in terms of If-Then-Else If-Then-Else(F, G, 0) And(F, G) F G, 0 F F X X G 1 M UX G 0 0 If-Then-Else(F, 1, G) Or(F, G) F 1, G F F X X 1 1 M UX G G 0 72 Generating OBDD from network Task: Represent output functions of gate network as OBDDs. Evaluation A new_var ("a"); B new_var ("b"); C new_var ("c"); T1 And (A, 0, B); If-Then-Else(A, B, 0) T2 And (B, C); If-Then-Else(B,C, 0) Out Or (T1, T2); If-Then-Else(A, 1, B) Network A T1 B Out C T2 Out Resulting Graphs T1 0 A B C a b c 1 0 1 0 a b b 1 0 a T2 b c 1 0 b c 1 0 1 73 Solving circuit problems as SAT a b h f c d g i e Input Vector Assignment ? Primary Output ‘i’ to 1 ? 74 SAT formulas for simple gates a b c a c b ( c a )( c b )( c a b ) b a ( a b )( a b ) a b c ( c a )( c b )( c a b ) 75 Solving circuit problems as SAT Set of clauses representing function of each gate Unit literal clause asserting output to ‘1’ (b f )(c f )(b c f ) a b h f (d g )( e g )( d e g ) (a h )( f h )( a f h) c d e g i (h i )( g i )( h g i ) (i ) 76 CEC in Practice Key Observation: The circuits being verified usually have a number of internal equivalent functions f ’ x1’x ’ 2 f i1 i2 Check x1(i1, i2,…in) = x1’(i1, i2,…in) x2(i1, i2,…in) = x2’(i1, i2,…in) x k’ x1 x 2 To prove f (i1, i2,…in) = f’ (i1, i2,…in) xk xk(i1, i2,…in) = xk’(i1, i2,…in) in f(x1, x2,…xk) = f’(x1’, x2’,…xk’) 77 Internal Equiv. Based CEC Algorithm PI PS Comb. Logic 1 Comb. Logic 2 PO NS Random Simulation =? PO NS Gather PENs Combinational miter after latch mapping PENs: Potentially equivalent nodes, i.e. nodes with identical simulation signature Is there an unjustified PEN pair x,y ? No Done! Yes Refine PEN sets using counterexample No Is x=y? Yes Structurally merge x,y 78 Anatomy of Typical CEC Tools Circuit A Quick Synthesis Latch Mapper Circuit B Counter-example viewer Error Diagnosis Engine Structural methods Learning BDD SAT ATPG 79 Major Industrial Offerings of CEC Formality (Synopsys) Conformal Suite (Verplex, now Cadence) FormalPro (Mentor Graphics) Typical capabilities of these tools: Can handle circuits of up to several million gates flat in up to a few hours of runtime Comprehensive debug tool to pinpoint error-sources Counter-example display & cross-link of RTL and gatelevel netlists for easier debugging Ability to checkpoint verification process and restart from same point later What if capability (unique to FormalPro) 80 Reachability-based Equivalence Checking Inputs S0 M1 Outputs =? M2 S1 S0 S1 Product Machine Build product machine of M1 and M2 Traverse state-space of product machine starting from reset states S0, S1 Test equivalence of outputs in each state Can use any state-space traversal technique 81 Move to System-Level Design System-level design Manual effort Architecture exploration Barrier to adoption of System-level design Methodology! RTL Current design iterations Gate-level design System-Level Verification Property & Model Checking Manual effort Equivalence Checking RTL Gate-level design 82 83 System-level Synthesis System-level design Manual effort RTL Gate-level design Automatic Synthesis 84 Scope of Today’s EC Technology Re-encoding of state scheduling Sequential differences Serial vs parallel interfaces pipelining FFs match Combinational EC Data representation differences Identical data types Composite data types Bit-accurate Precision/rounding differences 85 Upcoming: Transaction-Based EC The states in RTL that correspond to states in system-level model (SLM), are referred to as synchronizing states Complete Verification SLM Refinement mapping or Sequential counterexample RTL Transient states 86 Transactions : State View SL transaction SLM Refinement mapping RTL transaction RTL Encapsulates one or more units of computation for the design being verified Self-contained since it brings the machine back to a synchronizing state Some EDA vendor is about to offer a formal verification tools that can deal with SLM, such as Calypto 87 Equivalence Checking: Conclusions Currently equivalence checking based on latch mapping+CEC Methodology premised on structural similarity of designs under comparison Efficient & scalable Maybe applicable to system-level problems More general sequential EC somewhat less explored Might be needed for system level equivalence checking 88 Model (property) checking: Basics (Lecture 4) Basic model checking algorthm States are explicitly represented States are “implicitly” represented Symbolic model checking with BDDs Model checking using SAT 89 Sequential logic circuit Y=c(ab) a AND OR b y c NOT XOR Combinational Circuit Logic Gates INPUTS a o c Present states b p Q D OUTPUTS Comb Logic LATCHES n Sequential Circuit Next States 90 Temporal logic model checking Verify Reactive Systems Construct state machine representation of reactive system Nondeterminism expresses range of possible behaviors “Product” of component state machines Express desired behavior as formula in temporal logic (TL) Determine whether or not property holds FSM rep. Traffic Light Controller Design True Property in some TL e.g. CTL, LTL “It is never possible to have a green light for both N-S and E-W.” Model Checker False + Counterexample 91 MoC: Finite State Machine (FSM) 0/0 INPUTS Present states Comb Logic OUTPUTS Next States LATCHES Mealy FSM: I, S, , S0, O, ) I: input alphabet S: finite, non-empty set of states : S I S, next-state function S0 S : set of initial (reset) states O: output alphabet : S I O , output function S1 1/1 1/1 0/0 S3 S2 1/0 0/0 State Transition Graph x=0 x=1 S1 S1,0 S2,1 S2 S1,0 S2,0 S3 S3,0 S1,1 State Transition Table 92 Classification of properties Safety properties “undesirable things never happen” “desirable things always happen” Examples: A bus arbiter never grants the requests to two masters Elevator does not reach a floor unless it is requested Message received is the message sent Liveness (progress) properties “desirable state repeatedly reached” “desirable state eventually reached” Examples: Every bus request is eventually granted A car at a traffic light is eventually allowed to pass 93 Fairness constraints In general, not every run in a state machine is a valid behavior But all runs are included in transition systems Fairness constraints rule out certain runs Fairness constraints can be expressed as CTL formulas Properties only checked for fair paths !! A fair path must satisfy each formula infinitely often Path quantifiers are restricted to only the fair paths Fairness examples An arbiter arbitrates each requestor infinitely often In a communication channel a continuously transmitted message is received infinitely often 94 Temporal logics Precise specification Amenable to symbolic manipulation Two kinds of temporal logics (TL) Linear Temporal Logic (LTL): Time is a linear sequence of events Branching time temporal logic (CTL, CTL*): Time is a tree of events CTL Formulae describe properties of computation trees Computation Trees are obtained by unwinding the transition system model Branching structure due to nondeterminism CTL* is more powerful, includes CTL and LTL 95 Syntax of CTL Every atomic proposition is a CTL formula If f and g are formulae then so are f, (f g), (f g), (f g), (f g) AG f - in all paths, in all state f (in all future, f) EG f - in some path, in all states f AF f - in all paths, in some state f (in every future f) EF f - in some future f A(f U g) - in all paths, f holds until g E(f U g) - in some path, f holds until g AX f - in every next state, f holds EX f - in some next state f holds Examples AG ¬ (EW_light_go NS_light_go) AG (car_at_intersection AF(light_green)) AG (EF Restart) EF (Start ¬Ready) 96 CTL model checking (Clarke and Emerson, Quielle and Sifakis) M╞ F M: Transition System, F: CTL formulae M defines a tree (unwind the transition system) F specifies existence of one or all paths satisfying some conditions Verification checks whether these conditions hold for the tree defined by M Specifically: Compute the set of states of M satisfying F M ╞ F iff initial states of M are in this set 97 CTL Model checking example 1 P Compute EFp EF p = p EX(p) EX(EX(p)) . . . STEP 1 STEP 2 P P Fixed Point !! STEP 3 P Computation terminates EF p Holds in all dark states Computation involves backward breadth first traversal Calculation of Strongly Connected Subgraphs (cycles) 98 CTL Model checking example 2 P P P Compute EG p EG p = p EX p EX(EX p) . . . STEP 2 Initial:STEP 1 P P P STEP 3 P P P P TERMINATION P P P P P 99 Checking safety conditions S0: Initial states Z : Bad states Start from S0 (Z) = set of initial (bad) states Perform forward (backward) reachability analysis to compute a reached state set R (B) Determine if R (B) intersects Z (S0) S S0 0 B R Z Forward Reachability Z Backward Reachability 100 Model checking approaches Explicit state model checking Requires explicit enumeration of states Impractical for circuits with large state spaces Useful tools exist: Murphi, SPIN, … Symbolic model checking Representation & manipulation in terms of ROBDDs or SAT solvers Core tasks: Represent state machine (transition relation) and sets of states Forward/backward reachability analysis Based on computing image/pre-image of set of states Fixed-point detection 101 Symbolic manipulation with OBDDs Strategy Represent data as set of OBDDs Identical variable orderings Express solution method as sequence of symbolic operations Implement each operation by OBDD manipulation Key Algorithmic Properties Arguments: OBDDs with identical variable orders Result is OBDD with same ordering Each step polynomial complexity 102 If-Then-Else operation Concept Basic technique for building OBDD from logic network or formula. Arguments I, T, E I T, E I X T 1 M UX E 0 Functions over variables X Represented as OBDDs Result OBDD representing composite function (I T) (I E) 103 If-Then-Else execution example Argument I Argument T Argument E Recursive Calls 1 a B1 A1,B1 A1 a A2,B2 A2 b c A6 A3 d A4 0 A3,B2 B2 d 1 A5 A6,B2 A6,B5 c B5 B3 0 1 B4 A5,B2 A3,B4 A4,B3 A5,B4 Optimizations Dynamic programming Early termination rules Apply reduction rules bottom-up as return from recursive calls (Recursive calling structure implicitly defines unreduced BDD) 104 Derived algebraic operations Other operations can be expressed in terms of If-Then-Else If-Then-Else(F, G, 0) And(F, G) F G, 0 F F X X G 1 M UX G 0 0 If-Then-Else(F, 1, G) Or(F, G) F 1, G F F X X 1 1 M UX G G 0 105 Generating OBDD from network Task: Represent output functions of gate network as OBDDs. Evaluation Network A A B C T1 T2 Out T1 B Out C T2 new_var ("a"); new_var ("b"); new_var ("c"); And (A, 0, B); And (B, C); Or (T1, T2); Out Resulting Graphs T1 0 A B C a b c 1 0 1 0 a b b 1 0 a T2 b c 1 0 b c 1 0 1 106 Characteristic functions Concept A {0,1}n Set of bit vectors of length n A Represent set A as Boolean function A of n variables 0 /1 X A if and only if A(X ) = 1 Set Operations Union Intersection A A B B 107 Symbolic FSM representation Nondeterministic FSM Symbolic Representation n1 00 n2 01 o1 10 o2 o2 0 1 Represent set of transitions as function (Old, New) 11 o1 ,o2 encoded old state n1 , n2 encoded new state Yields 1 if can have transition from state Old to state New Represent as Boolean function Over variables encoding states 108 Reachability analysis Task Compute set of states reachable from initial state Q0 Represent as Boolean function R(S) Never enumerate states explicitly Given old state Compute state 0/1 new state Initial R0 = Q0 R 0/1 109 Breadth-First reachability analysis 00 01 R R00 00 00 00 10 R R11 01 01 R R22 R3 10 10 11 Ri – set of states that can be reached in i transitions Reach fixed point when Rn = Rn+1 Guaranteed since finite state 110 Iterative computation Ri old new Ri +1 Ri R0 Q0 do R i 1( s ) R i ( s ) s ' [ R i ( s ' ) ( s ' , s )] i i 1 until R i R i 1 ALGORITHM 111 BDD-based MC: Current status Symbolic model checkers can analyze sequential circuits with ~200- 400 flip flops Challenges For specific circuit types, larger state spaces have been analyzed Memory/runtime bottlenecks Adoption of TLs for property specification Frontier constantly being pushed Abstraction & approximation techniques Symmetry reduction Compositional reasoning Advances in BDD technology … 112 Solving circuit problems as SAT a b h f c d g i e Input Vector Assignment ? Primary Output ‘i’ to 1 ? 113 SAT formulas for simple gates a b c a c b ( c a )( c b )( c a b ) b a ( a b )( a b ) a b c ( c a )( c b )( c a b ) 114 Solving circuit problems as SAT Set of clauses representing function of each gate Unit literal clause asserting output to ‘1’ (b f )(c f )(b c f ) a b h f (d g )( e g )( d e g ) (a h )( f h )( a f h) c d e g i (h i )( g i )( h g i ) (i ) 115 SAT-based unbounded MC SAT-based Inductive reasoning Exact image computation Use SAT solver just for fixed-point detection Image computation using SAT solver McMillan CAV’02, Kang & Park DAC’02 Approximate image computation Using Craig Interpolants (McMillan CAV’03) Abstraction refinement Discussed later in the tutorial 116 SAT-based reasoning on ILAs PI PO CL BMC work (Biere et al) NS PS Unroll k-Steps Popularized by the Current SAT solvers have shown good results LATCHES PI1 PI2 PI k PS1 CL1 PO1 NS1 PS2 CL2 PO2 NS2 NSk-1 PS3 PSk CLk POk NSk 117 SAT-based inductive reasoning I0 never satisfies ~ P Simple Induction UNSAT ‘1 ’ I0 Induction Step Base Case P P + AG P is TRUE UNSAT ‘1’ ‘1’ CLk+1 P ‘1 ’ If Ii never satisfies ~ P, then Ii+1 never satisfies ~P It is never the case that (I0 satisfies P) and (Ii+1 satisfies ~P) 118 SAT-based inductive reasoning P I0 Induction Step Base Case P CL1 P P CL2 CLk ‘1 ’ P ‘1’ P CL1 ‘1’ P ‘1’ CLk CLk+1 Induction with depth ‘k’ (Sheeran et al, Bjesse et al FMCAD 2000) P ‘1 ’ 119 SAT-based induction Can prove or disprove properties k-depth induction: Can check more properties for larger k Base case is simply k-length BMC But not complete ! Example: P Not k - depth inductive for any k ! P Unreachable state-space 120 SAT-based inductive reasoning Unique paths Induction: Restrict unrolled ILA to be loop-free Sheeran et al, Bjesse et al FMCAD’00 Unrolling upto recurrence diameter i.e. length of longest loop-free path Complete! Stronger induction methods can be expensive But, some properties very easy to prove by induction, very hard by state-space traversal Simple induction can be cheap, first step in verification flow 121 SAT-based image computation i 0 R 0 ( s ) Init do Issues: Function representation Quantification R i 1( s ' ) toProp ( s .Tr ( s , s ' ) R i ( s )) i i 1 i 1 i until R i( s ) P ( s ) or R k 0 k (s) R k (s) k 0 SAT Solver Bug found ! Fixed-point 122 Function Representation Representation of: Init, Ri(s), P(s), Tr(s,s’) Converted to CNF for SAT solving b x z y Reduced Boolean Circuit (RBC) Abdulla et al, TACAS 2000 b a 0 1 Boolean Expression Diagram (BED) Williams et al, CAV 2000 123 Quantification Apply definition of existential quantification: x . ( x ) ( x 0 ) ( x 1) Mitigate formula blow-up by: Inherent reduction rules of function rep. Special case quantification rules: Inlining: x .( x ) ( x ) ( ) where Scope Reduction: x . ( x ) ( x . ( x )) x Vars ( ) where x Vars ( ) x . ( x ) ( x ) ( x . ( x )) ( x . ( x )) Limitation: Suitable only when small number of variables to be quantified 124 Exact image computation using SAT McMillan, CAV 2002 CTL Model Checking procedure AG(p) Let Z = Q = p while Z 1 let Z = (W · pi/si)Q let Q = Q Z return Q Solve W · f Solution: Express f in CNF: fCNF Drop all wi literals from fCNF Core problem: Express a given formula f in CNF 125 Computing a CNF representation for f Basic Algorithm Create CNF(f) Solve SAT(CNF(f) vf) Compute blocking clause for each satisfying assignment Collect all blocking clauses fCNF Blocking Clauses Must: Contain only original vars. of f Be false under some sat. assgn. of CNF(f) vf Be implied by CNF(f) vf e.g. f = (ab)c a b vab vf c CNF(f) Blocking Clauses : (bc) , (ac) fCNF= (bc) (ac) 126 Some issues Issues: Blocking clauses expressed in terms of original variables of f Extracted from a separate implication graph Quantification of W vars. can be performed on each generated blocking clause: Combine both steps into one!! Conclusions: Technique promising where BDDs blow up BDDs superior as a general purpose technique Proposed technique needs more polishing 127 Lecture 5 Enhancing formal verification capacity Abstraction-refinement Assume guarantee/Compositional Reasoning Approximation Symmetry reduction Partial Order Reduction Industrial and research tool offerings 128 Abstraction Limitations of symbolic model checking Suffers from state explosion Concurrency Data domains Abstraction of state space Represent the state space using a smaller model Pay attention to preserving the checked properties. Do not affect the flow of control. 129 Example Use smaller data objects HDL Code: X:= f(m); Y:=g(n); if (X*Y>0) then … else … X, Y never used again. Assign values {-1, 0, 1} to X and Y. Based on the following connection: sgn(X) = 1 if X>0, 0 if X=0, and -1 if X<0. sgn(X)*sgn(Y)=sgn(X*Y). Change f and g to produce abstract values for X and Y 130 Abstraction vs. simplification Not every simplified system is an abstraction The key question is: If we prove or disprove a property of the simplified system, what have we learned about the original system? 131 Abstraction (Cont) Abstract transition relation is conservative Abstract next states must contain all concrete successors And possibly more states t RA s Abstract g g Concrete x y RC 132 Abstract counter-example If model checking fails an abstract counterexample is produced Concrete transitions are present for each pair of consecutive abstract states But concrete counter-example may not be present! Spurious Trace Abstract Concrete g g g y’ Real Trace x y’’ z 133 Abstraction refined Abstraction is refined by adding more states prevents previous spurious counter example Model checking is repeated on new abstraction iterate New Trace gi Abstract Concrete gi gi gi y1 Real Trace z x y’’ 134 Abstraction refinement algorithm Build abstract model Refinement spurious counterexample Model check abstract model true True on concrete model abstract counterexample abort Infeasible Check abstract counterexample on concrete model real counterexample False on concrete model 135 Assume-Guarantee Reasoning S and R are just too large to be verified at the same time Like to verify S and R separately ! Sender S || Receiver has R < Property 136 Assume-Guarantee Reasoning First try to find something intermediate, S’ and R’ between the designs and the specification, such that it is easy to verify that S’ and R’ satisfy the property S R < S’ R’ < 137 Assume-Guarantee Reasoning If we can verify individual cases separately, we are done ! R S S R < R’ < S’ < S’ R’ < 138 Assume-Guarantee Reasoning But normally we cannot due to unconstrained inputs Inputs are unconstrained S S < R’ Inputs are < unconstrained S’ R R < S R < 139 Assume-Guarantee Reasoning Use S’ and R’ to constrain inputs ! S’ R < R’ S R’ < S’ S R < S’ R’ < 140 Assume-Guarantee Reasoning This is a theorem !AG reasoning: Example S & R -> R S & R -> S S & R -> S & R 141 Symmetry reductions Idea: If state space is symmetric, explore only a symmetric “quotient” of the state space A permutation function f : S S is an automorphism if: ( x, z) ( f(x), f(z)) 0,0 0,1 1,0 e.g. f: f(0,0) = 1,1 f(1,1) = 0,0 f(0,1) = 0,1 f(1,0) = 1,0 The set of all automorphisms forms a group! Automorphism groups induce equivalence classes (orbits) over the state space 1,1 e.g. [ (0,0), (1,1) ] [ (0,1), (1,0) ] 142 Quotient machine 0,0 0,1 [ (0,0),(1,1) ] 1,0 [ (0,1), (1,0) ] 1,1 Map each state to its representative in the orbit Quotient machine Do model checking analysis on the quotient machine 143 Symmetry reductions Difficulty Solutions Identifying symmetry groups Computing function mapping states to representatives Ask user to tell you where the symmetries are Be satisfied with multiple representatives for each orbit Tools: Mur, Nitpick, RuleBase 144 Over-approximate reachability Exact reachability captures the exact reachable state-space Problem: BDD-blowup in many real designs Solution: Compute over-approximation of the reachable states R+ R2 I0 Error could be a false negative + R1+ R1 R2 Often sufficient to prove properties correct R Can trade off BDD-size and runtime with accuracy of approximation 145 Over-approx. reachability techniques Split FSM into submachines by partitioning statevars Perform (exact) reachability on each machine Cross-product of reached state spaces gives overapprox. for original FSM PI PS CL LATCHES X PO NS X 146 Over-approx: more issues Communicate between sub-FSMs to tighten approximation After each time-frame After least fixpoint computation for a sub-FSM Computing partitions Heuristic and/or manual Disjoint partitions (Cho et al) Overlapping partitions (Govindaraju et al) Can capture limited interaction among sub FSMs Tighter approximation May not increase BDD sizes much 147 Partial order reduction Factor out independent state transitions! (typical for asynchronous communication as in Software- and Protocol-Checking) May result in exponential reduction in the number of states Process A transition Process B transition One Relevant Trace of States Synchronization 148 Model Checkers - Research Tools SMV (CMU, Cadence) VIS (UC Berkeley) Mocha (UC Berkeley, compositional reasoning) Verisoft (AT&T, C-model checker) Bandera (Java model checker) 149 Industrial Model Checkers FormalCheck (Cadence) COSPAN (from Bell Labs) under the hood Support for arbitrary precision arithmetic Automatic bus-contention, multi-driver violation, tristate support fir high-impedance check Powerful design reduction techniques Removal of portions of design that do not affect the property being proven Constant & constraint propagation Iterative reduction guarantees that queries proven on the reduced design hold on the entire design 150 EDA Vendor Tool Offerings Verplex (Cadence) Blacktie IBM RuleBase @HDL - @Verifier Real Intent Verix works on Verilog RTL static assertion checks automatic property extraction clock domain synchronization errors slimilar to @Verifier Averant Solidify Jasper design automation Jasper Gold 151 Lecture 6: Semi-formal verification C o v e r a g e Existing Formal FV Augmented Simulation (Falsification) Verification Manual test w/ coverage 2K 20K FV + Complete coverage - Limited capacity 200K 2M FV Augmented Simulation + Good coverage + Good capacity Random simulation GATES Simulation +Unlimited capacity - Poor coverage 152 Section outline Symbolic simulation Symbolic trajectory evaluation (STE) SAT-based bounded model checking Sequential ATPG-based model checking Guided search Smart simulation 153 Symbolic simulation Conventional simulation: Input & outputs are constants (0,1,X,…) 1 a 0 b 1 c 1 a·b+b·c Problem: Too many constant input combinations to simulate !! Symbolic simulation: Symbolic expressions used for inputs Expressions propagated to compute outputs Equivalent to multiple constant simulations !! Ref: Prof. David Dill, CAV ’99c 154 Symbolic simulation (sequential case) a0 a0·b0 + b0 ·c a1 a1·b1+ b1·(a0·b0 + b0·c) b1 b0 Time frame 1 c Time frame 2 a0·b0 + b0·c a1 a0 b1 b0 c a1·b1+ b1·(a0·b0 + b0·c) Unrolled Circuit 155 Symbolic simulation Inputs can be constants 1 b+c b a a·b + b ·c b c c a+b Simulate certain set Input expressions of patterns b can be related Model signal correlations Can result in simpler output expressions b+c c 156 Symbolic simulation Use BDDs as the symbolic representation Work at gate and MOS transistor level Can exploit abstraction capabilities of ’X’ value Can be used to model unknown/don’t care values Common use in representing uninitialized state variables Boolean functions extended to work with {0,1,X} Two BDD (binary) variables used to represent each symbolic variable 157 Symbolic simulation Advantages Can handle larger designs than model checking Can use a large variety of circuit models Possibly more natural for non-formalists. Amenable to partial verification. Disadvantages Not good with state machines (possibly better with data paths). Does not support temporal logic Requires ingenuity to prove properties. 158 Practical deployment Systems: COSMOS [bryant et al], Voss[Seger et al Intel] Magellan [Synopsys] Innologic Exploiting hierarchy Symbolically encode circuit structure Based on hierarchy in circuit description Simulator operates directly on encoded circuit Use symbolic variables to encode both data values & circuit structure Implemented by Innologic, Synopsys (DAC ‘02) Greatest success in memory verification (Innologic) 159 High-level symbolic simulation Data Types: Boolean, bitvectors, int, reals, arrays Operations: logical, arithmetic, equality, uninterpreted functions Final expression contains variables and operators Coupled with Decision procedures to check correctness of final expression Final expressions can also be manually checked for unexpected terms/variables, flagging errors e.g. in JEM1 verification [Greve ‘98] 160 High-level symbolic simulation Manipulation of symbolic expressions done with Rewrite systems like in PVS Boolean and algebraic simplifiers along with theories of linear inequalities, equalities and uninterpreted functions Extensively used along with decision procedures in microprocessor verification Pipelined processors: DLX Superscalar processors: Torch (Stanford) Retirement logic of Pentium Pro Processors with out of order executions 161 Symbolic trajectory evaluation (STE) Trajectory : Sequence of values of system variables Example: c = AND (a, b) and delay is 1 A possible trajectory : (a,b,c) = (0, 1, X), (1, 1, 0), (1, 0, 1), (X, X, 0), (X, X, X),… Express behavior of system model as a set of trajectories I and desired property as a set of trajectories S Determine if I is inconsistent with S Inconsistent: I says 0 but S says 1 for a signal at time t Consistent: I says 0 but S says X or 0 for a signal at time t 162 STE: An example 4-Bit Shift Register Din Specification Dout Assert Din = a NNNN Dout = a If apply input a then 4 cycles later will get output a Din Din Din Din Din Ref: Prof. Randal Bryant, 2002 a X X X X X X a X X X X X X a X X X X X X a X X X X X X a a Din = a T=0 Dout T=1 Dout T=2 Dout T=3 Dout T=4 Dout NNNN Dout = a Check 163 STE: Pros, cons & u Advantage: Higher capacity than symbolic model checking Disadvantage: Properties checkable not as expressive as CTL Practical success of STE Verification of arrays (memories, TLBs etc.) in Power PC architecture x86 Instruction length decoder for Intel processor Intel FP adder Microprocessor verification 164 SAT-based bounded model checking Property F FSM M PI PO CL NS PS Example F: AG P P ? LATCHES Question: Does M have a counter-example to F within k transitions ? Biere et al (TACAS’99, DAC’99) 165 SAT-based bounded model checking P P P I0 CL1 CL2 CLk P ‘1 ’ Unroll M for k time-frames SAT CNF SAT Solver UNSAT Counter-example to AG P No Counterexample within k steps 166 SAT-based BMC Primarily used for finding bugs ! Verification complete if k > sequential depth of M Open Sequential depth computation or tight problem!! estimation intractable in practice Can express both safety and liveness properties (bounded semantics) All LTL formulas Unbounded fairness by detecting loops 167 SAT-based BMC: Pros & cons Advantages: SAT-BMC good at producing counter-examples upto medium depths (upto 50-60) SAT solvers less sensitive to size of design: SATBMC can handle larger designs SAT solvers require less parameter tuning: Productivity gain Drawbacks: Incomplete method: Cannot verify properties Ineffective at larger depths: Slow, CNF blow-up Cannot describe all CTL properties 168 Enhancements to basic SAT-BMC CNF generation for BMC Decision variable ordering Bounded cone-of-influence: Biere et al CAV’99 Circuit-graph compression: Ganai et al VLSID’02 Binary time-frame expansion: Fallah ICCAD’02 BMC-specific static ordering: Strichman CAV’00 Tuning VSIDS for BMC: Shacham et al MTV’02 Addition of clauses/constraints Sharing clauses across BMC runs: Strichman CHARME’01 Learning clauses from BDDs: Gupta et al DAC’03 Using BDD reachability over-approx: Cabodi et al DATE’03 169 Sequential ATPG for MC Proposed by Boppana, Rajan, Takayama & Fujita, CAV ‘99 e.g. AG p INPUT EF p INPUT AUTOMATA CIRCUIT from property CIRCUIT TEST NETWORK p stuck-at fault s-a-0 fault 170 Advantages of sequential ATPG-based MC vs SAT-BMC vs BDDs No explicit storage of states No need to build transition relation Good balance of DFS and BFS traversal of state-space Can model real-world primitives, e.g. tri-state buses, high impedence value No explicit unrolling of time-frames Uses circuit-based heuristics to guide or speed-up search 171 Sequential ATPG for BMC PROPERTY n Recent work stuck-at by Abraham fault TEST ORIGINAL MONITOR NETWORK CIRCUIT et al (ITC’02, VLSID’03) Model both p safety & p p p start p p liveness … n 2 0 1 n-1 properties Example: p (bounded) p EG p p 172 ATPG-MC: Current status Attempts to use simulation-based ATPG for falsification (Hsiao et al HLDVT’01, DAC’02) No research characterizing fragment of language (e.g. CTL, LTL) checkable through ATPG-based MC Some works report dramatic improvements of seq. ATPG-BMC vs. SAT-BMC Current efforts towards combining SAT solvers and sequential ATPG (SATORI ICCAD’03) 173 Guided search State-space search optimized for bugsearching (Yang & Dill, DAC 98) Use prioritized search Cost function to pick next state to search Hamming distance to error states Breadth-first Search Prioritized Search Error State Error State 174 Improving guided search Target enlargement also Yuan et al CAV 97 Without Target Enlargement Reset State Improved cost function Tracks Compute series of approximate preimages Use the approximate pre-image to estimate distance to enlarged target Guideposts Designer provided hints/necessary pre-conditions for assertion violation Bias search to explore search with those pre-conditions Error States Enlarged Error States 175 Smart simulation I : SIVA [Ganai, Aziz, Kuehlmann DAC ‘99] Combines random simulation with BDDs and combinational ATPG Identify targets Indicator variables, coverage goals, fail states etc. Lighthouses: Several per target “Sub-targets” to guide SIVA to reach a target At each state identify targets with constant simulation signature Advance simulation by visiting states which causes such targets to toggle value Search for such next state by ATPG/BDDs 176 SIVA - a run R1’ R1 R5000’ INITIAL R2 RANDOM R5000 BDD D1’ ATPG D1 D2 Key: Determination of appropriate targets, lighthouses etc. to guide the search 177 Smart simulation II: Magellan [Ho et al, ICCAD 2000 (Synopsys)] Coverage-driven test generation Test generation Identify few interesting signals (typically <64): coverage signals Goal: Maximize state-coverage on coverage signals Interleave random simulation with symbolic simulation & SAT-BMC Unreachability analysis (under-approx) Identify unreachable coverage states to reduce coverage target 178 Magellan methodology Initial state Symbolic simulation / SAT-BMC Random simulation Coverage state Random simulation: Deep narrow search SAT-BMC: Short-range exhaustive (wide) search (<10 steps) Symbolic simulation: Middle range exhaustive (wide) search (10-50 steps) 179 Smart simulation III: 0-in search Approach: Test amplification Identify “seed states” reached through simulation i.e. directed or random simulation Explore exhaustively behavior around seed states using formal methods SAT-BMC, BDDs, symbolic simulation + Formal = Simulation 0-In Search 180 Methodology: Assertion-based Verification Use checkers (written in HDL) to: Specify targets for simulation/formal methods Capturing buggy conditions Specify environment of a module Can be synthesized into constraints Specify interfaces between components Inserting checkers: From 0-in CheckerWare library (~60 checkers) Specified by the user in Verilog Created automatically from RTL directives By 0-in Check functional tool Suggested by 0-in Checklist while analyzing RTL A kind of sophisticated lint checking 181 0-in search: Tool flow Instrumented Verilog RTL Verilog Tests and Testbench Verilog Files with 0-in Checkers Standard Verilog Simulator Source: 0-in Design Automation Verification White-paper No firings in Verilog output Simulation Trace (Seed) Checker Control File 0-in Search 0-in Confirm Verilog simulator (Firing Replay) Firings Log 0-in View GUI Standard Waveform Tool Lecture 7: Formal verification in C-based (SpecC/SystemC) based design methodology 182 C based design descriptions from specification (functional) level down to RTL Incremental refinement on the C/C++ descriptions Equivalence checking between refinements Between sequential and parallel descriptions Between two same control structures E q u iv a le n ce ch e ck in g b e tw e e n tw o d e scrip tio n s M o d e l ch e ck in g o n e a ch d e scrip tio n R e fin e d d e scrip tio n fo r h a rd w a re p a rts S o ftw a re p a rts re m a in th e sa m e S p e cifica tio n in C R e m o va l o f p o in te r, re cu rsive ca llin g R e fin e d d e scrip tio n w ith co n cu rre n cy In tro d u ctio n o f co n cu rre n cy (S p e cC o r S yste m C m a y b e u se d h e re ) To RTL d e sig n : R e fin e m en t step F ig u re 1 . C -b a sed sy stem d esig n flo w Property checking on each refinement Please note that in system level designs, both SpecC and SystemC have similar description mechanisms 183 Execution semantics in SpecC Sequentiality rule: Tstart(B1) <= Tstart(a) < Tend(a) <= Tstart(b) < Tend(b) <= Tstart(c) < Tend(c) <= Tend(B1) Sequential execution within a thread Example behavior B1 { void main(void) { a.main(); b.main(); c.main(); } }; B1 a b c time 184 Execution semantics in SpecC (cont.) Sequentiality rule: Tstart(B) <= Tstart(a) < Tend(a) <= Tstart(b) < Tend(b) <= Tstart(c) < Tend(c) <= Tend(B) Tstart(B) <= Tstart(d) < Tend(d) <= Tstart(e) < Tend(e) <= Tstart(f) < Tend(f) <= Tend(B) Example: concurrency/pallalelism behavior B { void main(void) { par { b1.main(); b2.main();} }}; behavior B1 { void main(void) { a.main(); b.main(); c.main();} }; behavior B2 { void main(void) { d.main(); e.main(); f.main();} }; Possible Schedule B d e a f b c time 185 Synchronization semantics wait/notify rule in time-interval formalism: wait cannot proceed until it receives a notified event notified event is valid until a wait or waitfor statement is reached behavior A: a.main(); wait e1; b.main(); behavior B: c.main(); notify e1; d.main(); Example: Notify-wait rule derives: Tend(w) >= Tend(n) wait cannot proceed until it receives notified event ‘wait e1’ starts thread A a ‘wait e1’ succeeds w b this order is guaranteed! B c n ‘notify e1’ done d time 186 Incremental refinement steps Starting with a functional model, make each part more detailed A1, B1, and C1 are refinement of A, B, and C respectively void A() { A } void B() { void A1() { } void B1() { B } void C() { } void main() { A(); B(); C(); } A1 B1 } void C1() { C } void main() { A1(); B1(); C1(); } C1 187 Incremental refinement steps Change of control structures IF-THEN-ELSE Sequential to parallel void A1() { A1 void A1() { A1 } void B1() { } void B1() { B1 } void C1() { } void main() { A1(); B1(); C1(); } } void C1() { C1 } void main() { par{ A1.main(); B1.main(); } C1.main(); } B1 notify wait C1 188 Incremental refinement steps Again make each part more detailed A2, B2, and C2 are refinement of A1, B1, and C1 respectively void A1() { void A1() { A1 } void B1() { } void C1() { } void main() { par{ A1.main(); B1.main(); } C1.main(); } B1 notify wait C1 A2 B2 } void B1() { notify } void C1() { } void main() { par{ A1.main(); B1.main(); } C1.main(); } wait C2 Equivalence checking of two descriptions with same control 189 If A and A1, B and B1, C and C1 are equivalent, then entire descriptions are equivalent Comparison of two “similar” descriptions void A() { void A1() { A } void B() { } void C() { } void main() { par{ A.main(); B.main(); } C.main(); } B notify wait C A1 } void B1() { } void C1() { } void main() { par{ A1.main(); B1.main(); } C1.main(); } B1 notify wait C1 Equivalence checking between sequential and parallel versions 190 Based on synchronization verification, prove equivalence Extraction of synchronization and dependency analysis void A() { A void A() { A } void B() { } void B() { B notify wait B } void C() { } void main() { A(); B(); C(); } } void C() { C } void main() { par{ A.main(); B.main(); } C.main(); } C notify-wait pair are supposed to communicate ! Symbolic simulation in higher-level designs Symbolic execution of designs All variables and operations are expressed as symbols Expressions among them are also symbols Efficient simulation for all possible input patterns A symbol expression (a + b) requires many patterns in conventional Boolean level symbolic simulation 256 * 256 patterns when a, b are 8-bit variables 191 192 Symbolic simulation example Example of equivalence checking based on symbolic simulation Checking (add1 == add2) , when v1, v2 are equivalent in both designs Equivalent variables are collected into EqvClass a = v1; b = v2; add1 = a + b; Description 1 add2 = v1 + v2; Description 2 Symbolic simulation EqvClass We are going to check the equivalence between add1 and add2 193 Symbolic simulation example Example of equivalence checking based on symbolic simulation Checking (add1 == add2) , when v1, v2 are equivalent in both designs Equivalent variables are collected into EqvClass a = v1; b = v2; add1 = a + b; Description 1 Symbolic simulation E1 (a, v1) E2 (b, v2) E3 (add1, a+b) add2 = v1 + v2; EqvClass Description 2 Description1 is simulated 194 Symbolic simulation example Example of equivalence checking based on symbolic simulation Checking (add1 == add2) , when v1, v2 are equivalent in both designs Equivalent variables are collected into EqvClass a = v1; b = v2; add1 = a + b; Description 1 Symbolic simulation E1 E2 E3 E4 (a, v1) (b, v2) (add1, a+b) (add2, v1+v2) add2 = v1 + v2; EqvClass Description 2 Description2 is simulated 195 Symbolic simulation example Example of equivalence checking based on symbolic simulation Checking (add1 == add2) , when v1, v2 are equivalent in both designs Equivalent variables are collected into EqvClass a = v1; b = v2; add1 = a + b; Description 1 add2 = v1 + v2; Description 2 Symbolic simulation E1 E2 E3 E4 (a, v1) (b, v2) (add1, a+b) (add2, v1+v2) EqvClass Due to the equivalences in E1, E2 196 Symbolic simulation example Example of equivalence checking based on symbolic simulation Checking (add1 == add2) , when v1, v2 are equivalent in both designs Equivalent variables are collected into EqvClass a = v1; b = v2; add1 = a + b; Description 1 add2 = v1 + v2; Description 2 Symbolic simulation E1 (a, v1) E2 (b, v2) E3’ (add1, a+b, add2, v1+v2) EqvClass E3 & E4 are merged into E3’ 197 Program slicing for SpecC/C++ Program slicing Two types of slicing Can extract a portion of a program based on dependence analysis Can be applied to formal methods, since it can reduce problems to be analyzed Backward slicing … extracting the portion that can affect a variable at a certain line of codes Forward slicing … extracting the portion that can be affected by a variable at a certain line of codes Based on C/C++ slicer, SpecC/SystemC/VHDL slicer can be developed [Shankar et al.] Since they are similar to C/C++, a little bit of extension is sufficient 198 Backward slicing Backward slicing for a variable v extracts all codes that affect the variable v Backward slicing a = 2; a = 2; b = 3; b = 3; c = 5; c = 5; a = a + 10; a = a + 10; b = a * c; /start/ b = a * c; /start/ c = c + a; c = c + a; a = a * b; a = a * b; 199 Forward slicing Forward slicing for a variable v extracts all codes that are affected by the variable v Forward slicing a = 2; a = 2; b = 3; b = 3; c = 5; c = 5; a = a + 10; a = a + 10; b = a * c; /start/ b = a * c; /start/ c = c + a; c = c + a; a = a * b; a = a * b; Example : Interprocedural slicing with summary edge 200 main() int sq(int x){ return(x*x); } void main(void){ int a,b,c,d; a=1; b=sq(a); c=3; d=sq(c); write(d); } a=1 call sq() c=1 b=sq$result call sq() A_In x d=sq$result A_Out sq$result A_In x write(d) A_Out sq$result sq() F_In x x*x F_Out sq$result Control Dependence Data Dependence Summary Edge Call Edge param in/out Source code Dependence graph Example : Interprocedural slicing with summary edge 201 main() int sq(int x){ return(x*x); } void main(void){ int a,b,c,d; a=1; b=sq(a); c=3; d=sq(c); write(d); } 1st stage a=1 call sq() c=1 b=sq$result call sq() A_In x d=sq$result A_Out sq$result A_In x write(d) A_Out sq$result sq() F_In x x*x F_Out sq$result Control Dependence Data Dependence Summary Edge Call Edge param in/out Source code Dependence graph Example : Interprocedural slicing with summary edge 202 main() int sq(int x){ return(x*x); } void main(void){ int a,b,c,d; a=1; b=sq(a); c=3; d=sq(c); write(d); } 2nd stage a=1 call sq() c=1 b=sq$result call sq() A_In x d=sq$result A_Out sq$result A_In x write(d) A_Out sq$result sq() F_In x x*x F_Out sq$result Control Dependence Data Dependence Summary Edge Call Edge param in/out Source code Dependence graph Dependence graph gives all dependency informations on the programs and is used here Equivalence checking of C descriptions based on symbolic simulation 203 Problem Symbolic simulation of a whole design takes a very long time, when the design is large Computational efforts exponentially increase with the numbers of conditional branches Solution Reducing areas to be simulated symbolically Based on difference between descriptions See the following slide for intuitive explanation Textual differences may become a good hint to identify which portions of programs are different 204 Efficient equivalence checking in SpecC/C++ Comparison of two similar design descriptions Extract textual differences Dependence analysis by program slicing type techniques Symbolically simulate the real difference and analyze the results : textual differences return a; Description1 return a; Description2 return a; Description1 return a; Description2 205 Verification flow Desc. 1 Desc. 2 Definition of Input/Output Variables and Program Slicing Identification of the Textual Differences & Extracting Functions to be Checked Symbolic Simulation Report of Results A Naïve way is to simulate both descriptions separately. Following slide introduces a more efficient simulation method 206 More efficient simulation method A lot of internal equivalence checking are carried out during verification Most of them do not directly contribute to prove output equivalence More efficient simulation method Do not simulate the descriptions separately Both descriptions are simulated in parallel Utilizing textual correspondence Only checking equivalence of corresponding statements Utilizing textual difference Equivalence checking can be skipped if two statements are obviously equivalent 207 An example of verification a_1 = 3 * in2_1; b_1 = 360 + in1_1; c_1 = 2408 * (in1_1 + in2_1); d_1 = c_1 – 4017 * b_1; e_1 = 1108 * (a_1 + b_1); out_1 = (d_1 + e_1) >> 8; D E E E E E a_2 = in1_2 * in2_2; b_2 = 360 + in1_2; c_2 = 2408 * (in1_2 + in2_2); d_2 = c_2 – 4017 * b_2; e_2 = 1108 * (a_2 + b_2); out_2 = (d_2 + e_2) >> 8; 1st line: textually different Note: Input: in1, in2 Output: out Create 2 EqvClasses separately E1 (a_1, 3 * in2_1) E2 (a_2, in1_2 * in2_2) Check their equivalence … nonequivalent Identify the statements affected by a_1 or a_2 5th line is identified 208 An example of verification a_1 = 3 * in2_1; b_1 = 360 + in1_1; c_1 = 2408 * (in1_1 + in2_1); d_1 = c_1 – 4017 * b_1; e_1 = 1108 * (a_1 + b_1); out_1 = (d_1 + e_1) >> 8; D E E E E E a_2 = in1_2 * in2_2; b_2 = 360 + in1_2; c_2 = 2408 * (in1_2 + in2_2); d_2 = c_2 – 4017 * b_2; e_2 = 1108 * (a_2 + b_2); out_2 = (d_2 + e_2) >> 8; 2nd, 3rd, 4th line: textually equivalent and not affected by nonequivalent variables These pairs are clearly equivalent can skip checking Simply create an EqvClass for each pair E3 (b_1, b_2, 360 + in1_1, 360 + in1_2) E4 (c_1, c_2, 2408 * (in1_1 + in2_1), 2408 * (in2_1 + in2_2)) E5 (d_1, d_2, c_1 – 4017 * b_1, c_2 – 4017 * b_2) 209 An example of verification a_1 = 3 * in2_1; b_1 = 360 + in1_1; c_1 = 2408 * (in1_1 + in2_1); d_1 = c_1 – 4017 * b_1; e_1 = 1108 * (a_1 + b_1); out_1 = (d_1 + e_1) >> 8; D E E E E E a_2 = in1_2 * in2_2; b_2 = 360 + in1_2; c_2 = 2408 * (in1_2 + in2_2); d_2 = c_2 – 4017 * b_2; e_2 = 1108 * (a_2 + b_2); out_2 = (d_2 + e_2) >> 8; 5th line: affected by nonequivalent variable a_1 and a_2 Create 2 EqvClasses separately E6 (e_1, 1108 * (a_1 + b_1)) E7 (e_2, 1108 * (a_2 + b_2)) Check their equivalence … nonequivalent Identify the statements affected by e_1 or e_2 6th line is identified 210 An example of verification a_1 = 3 * in2_1; b_1 = 360 + in1_1; c_1 = 2408 * (in1_1 + in2_1); d_1 = c_1 – 4017 * b_1; e_1 = 1108 * (a_1 + b_1); out_1 = (d_1 + e_1) >> 8; D E E E E E a_2 = in1_2 * in2_2; b_2 = 360 + in1_2; c_2 = 2408 * (in1_2 + in2_2); d_2 = c_2 – 4017 * b_2; e_2 = 1108 * (a_2 + b_2); out_2 = (d_2 + e_2) >> 8; 6th line: textually equivalent, but affected by nonequivalent variables e_1 and e_2 Create 2 EqvClasses separately E8 (out_1, (d_1 + e_1) >> 8) E9 (out_2, (d_2 + e_2) >> 8) Check their equivalence … nonequivalent Terminate with the results “nonequivalent” 211 Experiments (MPEG4) Optimization of IDCT functions (idct_row & idct_col) in MPEG4 Sizes Whole MPEG4 program … more than 17k lines Target IDCT functions … about 50 lines Note 9 lines are different between descriptions (of each function) Each function has 8 conditional branches (i.e. 256 execution paths have to be proved) functions were unrolled 8 times 212 Experiments (MPEG4) An example of different parts (below) Results Each pair of functions was proved to be equivalent idct_row … 680 sec idct_col … 2190 sec tmp = x6; x6 = W3 * x7 + W5 * tmp; x7 = W3 * tmp – W5 * x7; x8 = x0 + x1; Description 1 x8 x6 x7 x8 Optimization = = = = W3 * (x6 + x7); x8 – (W3 – W5) * x6; x8 – (W3 + W5) * x7; x0 + x1; Desciption 2 213 Experiments (AES) Changes in AES (American Encryption Standard) Target: Encryption function in Rijndael Rijndael is an implementation of AES Size: 120 lines Case 1 (equivalent changes) 4 different parts were inserted Result … equivalent, Verification time … 6 sec Case 2 (not equivalent changes) 8 different parts were inserted Result … not equivalent, Verification time … 344 sec Case 2 took longer time because many statements were affected by nonequivalent variables 214 Synchronization verification: Overview In system-level design… Communication among parallel processes is necessary To operate properly, those parallel processes must be correctly scheduled/synchronized Synchronization verification Guarantee the order of execution of statements as designers’ intended Problem size can be significantly reduced (focus on some, not all, parts of the design) More confident when “SV” and “property checking” than “property checking” alone 215 Par statement in SpecC C Language void A() { A SpecC Language void A() { A } void B() { B } void B() { B } void C() { } void main() { A(); B(); C(); } } void C() { C } void main() { par{ A.main(); B.main(); } C.main(); } C 216 Synchronization in SpecC Add notify/wait of event e for sync. ‘wait’ will stop process until it is ‘notify’ void A() { A notify e1; wait e2; B Process B stops and wait until e1 is notified } void B() { wait e1; notify e2; } void main() { par { A.main(); B.main(); } } notify e1 Process A stops and wait until e2 is notified A resumes wait e2 wait e1 notify e2 B resumes 217 Synchronization in SpecC a . mSynchronization ain() by m maaiinn(()) {{ ppaarr{{ aa..mm aa ii n( n )(;) ; b.main(); }} St2 a.main() b.main(); }} behavior a { b e hmaaviino(r) a{ {x = 1 0 ; m a i n ( ) { yx = +1100;; =x = ixf+y1 0e;; ny ot Notify/wait St1 St1 St2 b.main() /*st1*/ t /1 * / / */ s* ts 2* 2 *}/ } } / */N* es wt * /} b . m aSitn3( ) St3 tim e tim e b beehhaavviioorr bb {{ mmaaiinn(()) {{ w x ai = t2 0e;; x=20; Tas T1s / */N* es wt */ 3*/ }} /*st3*/ }} Tas T1s Tbs Tbs Ambiguous results on y causing from x = 10; /*st1*/ x = 20; /*st3*/ T1e T2s T1e T2s T3s T2e Tae T2e T3e T3s y = 20 (always) Tae Tbe T3e Tbe 218 Synchronization in SpecC (cont.) Synchronization by Notify/wait main() { par{ a.main(); b.main(); }} a.main() St1 behavior a { main() { x=10; y=x+10; notify e; St2 /*st1*/ /*st2*/ / * N e w * /} } b.main() St3 tim e behavior b { main() { wait e; x=20; /*New*/ /*st3*/ }} Tas T1s T1e T2s Tbs Tas=Tbs, Tae=Tbe Tas<=T1s<T1e<=T2s<T2e<=Tas Tbs<=T3s<T3e<=Tbe T2e<=T3s y = 20 (always) T2e T3s Tae T3e Tbe Synchronization verification for two concurrent processes (1) 219 Check if wait/notify can acutually communicate in while loops (or nested loops) First approach: Delete while loop In each iteration notify/wait must communicate while (1) { if stmnt switch stmnt notify e1 while (1) { if stmnt switch stmnt wait e1 while (1) { if stmnt switch stmnt notify e1 notify e2 wait e1 notify e2 wait e2 wait e2 } while (1) { if stmnt switch stmnt } } } Synchronization verification for two concurrent processes (2) 220 Unfold by N and M times N is 1 to n, M is 1 to m, any combinations while (1) { if stmnt switch stmnt wait e1 notify e2 while (1) { if stmnt switch stmnt notify e1 while (1) { if stmnt switch stmnt wait e1 notify e2 wait e2 while (1) { if stmnt switch stmnt notify e1 wait e2 } while (1) { if stmnt switch stmnt notify e1 wait e2 } } } } while (1) { if stmnt switch stmnt wait e1 notify e2 } while (1) { if stmnt switch stmnt wait e1 notify e2 } Synchronization verification for two concurrent processes (3) 221 While loops are converted into FSM (nested loops can be treated in the same way) Basically need regular model checking while (1) { if stmnt switch stmnt notify e1 while (1) { if stmnt switch stmnt wait e1 notify e2 wait e2 } if stmnt notify e1 switch stmnt wait e2 } switch stmnt wait e1 notify e2 if stmnt 222 Example(1) Par notify e1 a wait e2 c notify e2 behavior1 {notify e1; a; wait e2; b} wait e1 Behavior2 {wait e1; c; notify e2; d} e1 < a, a < e2, e2 < b, e1 < c, c < e2, e2 < d a, b, c, d, e1, e2 > 0 are satisfied ? → Yes, so the description is correct Par wait e2 a notify e1 b d b c notify e2 d behavior1 {wait e2; a; notify e1; b} wait e1 Behavior2 {wait e1; c; notify e2; d} e2 < a, a < e1, e1 < b, e1 < c, c < e2, e2 < d a, b, c, d, e1, e2 > 0 are satisfied ? → No, since a < c and c < a. This means a deadlock ! 223 Example(2) Par notify e1 a wait e1 ｗaitfor(10) ｗaitfor(10) c wait e2 b notify e2 d behavior1 {notify e1; a; waitfor(10); wait e2; b} Behavior2 {wait e1; waitfor(10); c; notify e2; d} e1 < a, a + 10 < e2, e2 < b, e1 + 10 < c, c < e2, e2 < d a, b, c, d, e1, e2 > 0 are satisfied ? → Yes, the design is correct Moreover, b<c is satisfied ? → No, the result says c<b Par notify e1 a wait e2 wait e1 ｗaitfor(10) c ｗaitfor(10) b notify e2 d behavior1 {notify e1; a; wait e2; waitfor(10); b} Behavior2 {wait e1; waitfor(10); c; notify e2; d} e1 < a, a < e2, e2 + 10 < b, e1 + 10 < c, c < e2, e2 < d a, b, c, d, e1, e2 > 0 are satisfied ? → Yes, the design is correct Moreover, b – e1 < 20 is satisfied ? → No, this is not satisfied 224 Verification flows Goals: Check whether given SpecC codes (with ‘par’, ‘notify/wait’) are properly synchronized If checking fails, counter-examples should be generated (trace to source of errors) Based on: Boolean SpecC, a little theorem prover, SVC/CVC, Program Slicing, ... 225 Verification Flows Refining SpecC behavior A(out event e, inout int x, inout int y) { void main(){ if (x > 1) { notify e; y = x - 1; } if (y > 3) { . . Boolean SpecC Abstraction behavior A() { void main(){ if (C0) { notify e ... } if (C1) { . . Correct Verify with a theorem prover Abstraction refinement Error-trace 226 Boolean Program Proposed by Ball and Rajamani under SLAM project at Microsoft Research Think of SW like a model (like FSM in HW) and verify it by first abstracting away unnecessary statements with userdefined predicates BP abstracts the original program: if properties on BP hold, so as original one 227 Our Boolean SpecC is a subset of original SpecC program ‘if-else’ conditions are replaced by propositional vars. e.g. if(x<y) -> if(c0) Statements other than ‘notify/wait’ and ‘if’, (ones that don’t effect the sync.) are abstracted away (abstract unnecessary info.) Only for verification of synchronization 228 Abstraction refinement Refining SpecC Boolean SpecC behavior A(out event e, inout int x, inout int y) { void main(){ if (x > 1) { notify e; y = x - 1; } if (y > 3) { . . Abstraction behavior A() { void main(){ if (C0) { notify e ... } if (C1) { . . Correct Verify with a theorem prover Error-trace Constructing Control Flow Graph (CFG) Entry barber while numCustomer if numCustomer = 0 DayDreaming KeepCutting chairOccupied call if numCustomer != 0 if chairOccupied = T chairOccupied = F Find & Modify Predicates if chairOccupied = F notify call chairOccupied = T Abstraction refinement Check validity Symbolic sim & theorem prover 229 Abstraction refinement 1. 2. 3. SpecC => boolean SpecC & build Control Flow Graph (CFG) Verify with theorem provers. If result is satisfied, terminate, else go to next step Use CFG to find related path and symbolically simulate along the path 4. 5. Use theorem provers on the validity of the path If not a feasible path, analyze and generate conditions on Boolean program variables using SpecC program slicing Use those conditions and modify boolean SpecC Go to 2 230 Example: Sleeping barber problem barber customer empty chair • • • • • barber chair barber: finished cutting->call customer barber: no customer->wait customer: barber wait->has hair cut customer: chairs occupied->come again customer: a chair empty->wait par statement barber customer if no-customer T Day dreaming if no-customer F F Cutting Go back T Enter barber F if finish cut Wait for ‘Call’ T ‘Call’ next customer Sit & had a hair cut Customer leave Leave 231 Example behavior Main () { void main() { par { barber.main(); customer.main(); } } }; behavior barber (inout event call, inout bool chairOccupied, inout bool waitCustomer) { void main() { behavior customer (inout event call, inout bool chairOccupied, inout bool waitCustomer) { void main() { while(1) { while(1) { if (waitCustomer == false) if (waitCustomer == false) DayDreaming(); waitCustomer = true; else { else { if (chairOccupied == true) { waitCustomer = false KeepCutting(); if (chairOccupied == false) chairOccupied = false; wait call; } } else { notify call; chairOccupied = true; }; } } }; 232 Abstract /* Barber */ /* Barber */ void main() { void main() { while(1) { while(a0) { if (!waitCustomer) DayDreaming(); if (a1) (A1) ... else { else { if (chairOccupied) { if (a2) { KeepCutting(); (A2) ... chairOccupied = false; (A3) ... Construct model + Verify } } else { else { notify call; (A4) notify call; chairOccupied = true; (A5) ... } } }; }; /* Customer */ /* Customer */ void main() { void main() { while(1) { while(b0) { if (!waitCustomer) waitCustomer = true; if (b1) (B1) ... else { waitCustomer = false; else { (B2) ... if (!chairOccupied) wait call; if (b2) (B3) wait call; } }; } }; Property to be verified: ‘notify’ is not reached, ‘wait’ is reached, then Synchronization error! A4 is not reached and B3 is reached Error!!! (Deadlock) a2 chairOccupied==true a1 waitCustomer==false 233 /* Barber */ /* Barber */ /* Barber */ /* Barber */ void main() { void main() { void main() { void main() { while(1) { while(1) { while(1) { while(1) { if (!waitCustomer) if (a1) if (a1) if (a1) DayDreaming(); ... ... ... else { else { if (chairOccupied) { else { if (a2) { else { if (a2) { if (a2) { KeepCutting(); ... ... ... chairOccupied = false; ... !a2 !a2 } } } } else { else { else { else { notify call; notify call; notify call; notify call; chairOccupied = true; ... a2 a2 } } } } }; }; }; }; /* Customer */ /* Customer */ /* Customer */ /* Customer */ void main() { void main() { void main() { void main() { while(1) { while(1) { if (!waitCustomer) if (b1) if (a1) ... ... !a1 else { else { else { waitCustomer = false; ... ... a1 if (!chairOccupied) if (b2) if (!a2) if (!a2) wait call; wait call; } }; while(1) { if (b1) waitCustomer = true; else { while(1) { } }; wait call; } }; wait call; } }; Evaluation of the synchronization verification methods(1) We injected ‘wait’ statements into the original SpecC descriptions (to cause deadlock, and verify it) Focusing only synchronization (notify/wait under par{ }), problem size can be significantly reduced Running on Linux machine, P3 1.1GHz & 2GB RAM, deadlock can be detected within few minutes 234 235 How to deal with loops ? Loops that create numbers of ‘notify/wait’ have to be unwound to get the equal numbers of notify and wait (analysis on loops of ‘notify/wait’ can be considered as another interesting research topic) This loop creates infinite numbers of notify(clk16) behavior gen_clk16() { void main() { while(1) { waitfor(10); notify(clk16); } } }; This loop creates infinite numbers of wait(clk16) With multiple of 16 ‘wait(clk16)’ each time behavior tx_clk() { void main() { while(1) { for(i = 0; i < 16; i++) wait(clk16); notify(bit_event); } } }; 236 Experimental results FIFO example Point-to-point protocol ~850 lines 5 behaviors have sync. semantic, 12 behaviors total Elevator control system ~260 lines 3 behaviors and 2 interfaces ~2000 lines 3 behaviors have sync. semantic, 13 behaviors total MPEG4 ~48,000 lines 3 behaviors have sync. semantic, XX behaviors total 237 Experimental results Properties: checking for deadlock # o f lines V erificatio n T im e (seco nds) O riginal S ync. V er. P ro perty1 P ro perty2 P ro perty3 F IF O 260 240 3.83 3.89 3.85 P o int-to -P o int P ro to co l 850 500 12.34 12.42 13.2 E levato r C o ntro l S ystem 2000 800 30.67 29.82 29.9 48000 800 27.79 27.66 28.11 M P EG 4 When consider only parallel behaviors Problem size (# of lines) can be reduced 238 C Bounded Model Checking CBMC Developed at CMU, 2003 [1] Hardware Verification using ANSI-C Programs as a Reference (Proc. of ASPDAC’03) Characteristics Modeling … C program -> Bit vector equation Specifying properties … inserting assertions in C programs C program Verification … using SAT solver Modeling Bit Vector Equation Specifying properties Verification using SAT solver Result 239 What does CBMC do? CBMC checks if or not C programs satisfy the properties the user specify Input … C Program with assertions as properties Output … Result (Success/Fail). If fails, a counter example is reported char a, b; int c; if (a < b) c = b – a; else c = a – b; assert (c >= 0); char a, b; int c; if (a < b) c = b – a; else c = a – b; assert (c != 0); Success Fail Counter example (a = 39, b = 39) 240 Bounded Model Checking (BMC) A kind of Model Checking techniques Checking whether the design satisfies the property up to certain finite numbers of execution cycles (bound) on the system Correctness of the design is guaranteed only up to the bound BMC is useful when the design is too large to handle for other formal methods BMC can detect many bugs although it only guarantees that there is no counter examples up to the bound number of execution cycles 241 BMC for C Programs What does “bound” mean in C program? Input In C programs, cycle is not explicit “bound” means the number of loop unwinding Combinational circuit Combinational circuit Combinational circuit Output Satisfies given properties? BMC in RTL (behavior of only 3 cycles are verified) Loop Unwinding Loop Loop BMC of a loop in C program Loop 242 Process of CBMC x x y; if ( x! 1) else C : ( x 1 x 0 y 0 ) x 2; x ; assert ( x 3 ); ( x 2 (( x1 1) ? 2 : x1 )) Modeling Given C program & properties ( x 3 (( x1 1) ? x 2 1 : x 2 ) P : x 3 3 Bit vector equation Generating SAT formula Result (success/fail) counter example SAT solver (Chaff) 243 Transforming ANSI-C (1) Renaming v v After renaming, each variable appears only once in the left hand side of assignments α is the number of assignments made to variable v x1 x 0 y 0 ; x x y; if ( x! 1) else x 2; x ; assert ( x 3 ); if ( x1 ! 1) else x 2 2; x 3 x 2 1; assert ( x 3 3 ); 244 Renaming x x y; x x y; if ( x! 1) else x 2; x ; assert ( x 3 ); x1 x 0 y 0 ; if ( x1 ! 1) else x 2 2; x 3 x 2 1; assert ( x 3 3 ); x1 x 0 y 0 ; x, y in right hand are not assigned yet x in left hand is assigned at the 1st time if ( x! 1) if ( x1 ! 1) This x is equivalent to the x after the 1st assignment x 2; x 2 2; This x is assigned at the 2nd time ・・・ 245 Transforming ANSI-C (2) Transformation into bit vector equation Formula C describes the Constraint of the verification Formula P describes the Property to be verified Checking if or not “C -> P” is always true x1 x 0 y 0 ; if ( x1 ! 1) else x 2 2; x 3 x 2 1; assert ( x 3 3 ); C : ( x 1 x 0 y 0 ) ( x 2 (( x1 1) ? 2 : x1 )) ( x 3 (( x1 1) ? x 2 1 : x 2 ) P : x 3 3 Formal definition of transformation from C into bit vector equation x1 x 0 y 0 ; if ( x1 ! 1) else x 2 2; x 3 x 2 1; assert ( x 3 3 ); C : ( x 1 x 0 y 0 ) ( x 2 (( x1 1) ? 2 : x1 )) ( x 3 (( x1 1) ? x 2 1 : x 2 ) P : x 3 3 C(p, g) and P(p, g) C(p,g) computes the assignments P(p,g) computes the properties p … program block g … guard (condition that p is operated) 246 247 Example of transformation x1 x 0 y 0 ; if ( x1 ! 1) else S … assignment x 2 2; x 3 x 2 1; S’ … conditional branch assert ( x 3 3 ); If the program is a sequential composition, C (p, g) is split by using ∧ operator Apply this rule C C (S ; S ' , true ) C ( S , true ) C ( S ' , true ) ※At the start of the program, “guard” is always “true” 248 Example of transformation x1 x 0 y 0 ; if ( x1 ! 1) else S … assignment x 2 2; x 3 x 2 1; S’ … conditional branch assert ( x 3 3 ); If program is an assignment v = e, C (p, g) is generally described as C ( v e , g ) : v g ? e : v 1 Apply this rule C C ( S , true ) C ( S ' , true ) ( x1 x 0 y 0 ) C ( I , true ) 249 Example of transformation x1 x 0 y 0 ; if ( x1 ! 1) else S … assignment x 2 2; S’ … conditional branch x 3 x 2 1; assert ( x 3 3 ); If program is a conditional branch if(c) I; else I’;, C (p, g) is generally described as C ( if ( c ) I else I , g ) : C ( I , g c ) C ( I , g c ) Apply this rule C ( x1 x 0 y 0 ) C ( S ' , true ) ( x1 x 0 y 0 ) C ( x 2 2 , x1 1) C ( x 3 x 2 1, x1 1) ( x 1 x 0 y 0 ) ( x 2 ( x 1 1 ) ? 2 : x 1 ) ( x 3 ( x 1 1) ? x 2 1 : x 2 ) 250 Example of transformation x1 x 0 y 0 ; if ( x1 ! 1) else x 2 2; x 3 x 2 1; Assertion assert ( x 3 3 ); Computation of P formula from assertions P ( assert ( a ), g ) : g a Apply this rule P ( x 3 3 ) ※ In this case, guard is true 251 Loop unwinding CBMC makes loops unwind finite times Because “Bounded” Model Checking Only the finite number of statements are verified The number of unwinding can be determined by the user Unwinding process Do loop unwinding n times by the following transformation while (e) inst; → if (e) { inst; while (e) inst; } The last while loop is replaced by assert(!e); (“unwinding assertion”) If “unwinding assertion” is satisfied, the number of unwinding is sufficient 252 Unwinding assertion while (e) inst; Unwinding n times Original loop Verification Is “unwinding assertion” violated? no yes Need to unwind more if (e) { inst; if (e) { inst; if (e) { inst; assert(!e); } } } Unwinding is Unwound loop sufficient unwinding assertion 253 Removing pointers Pointer dereferences are removed in the process of transformation Example. if (x) p = &a; else p = &b; *p =1; x = true -> *p = a x = false -> *p = b What does this pointer dereference? How do we remove pointers automatically? Introducing the φ function to analyze pointer dereferences Removing pointers by using the φ function Definition * e ( e , g ,0 ) e[ o ] ( e , g , o ) e … sub-expression to be dereferenced g … guard (condition that the dereference is operated) o … offset p & a; if ( x ) else p & b; * p 1; * p2 p1 & a 0 ; if ( x 0 ) Renaming else p 2 & b0 ; * p 2 1; ( p 2 , true , 0 ) ...( many processes )... x 0 ? a 0 : b0 254 255 Verification with SAT Solver Satisfiability Problem (SAT Problem) Formula F is satisfiable if there is more than one input pattern that makes F true Ex. F1 = a ∧ b … satisfiable (when a = true, b = true) Ex. F2 = a ∧ ￢a … not satisfiable C : ( x 1 x 0 y 0 ) x 2 (( x1 1) ? 2 : x1 ) x3 If (C -> P) is always true, ￢（C -> P） is not satisfiable (( x1 1 z 0 ) ? x 2 1 : x 2 ) P : x 3 3 Bit vector equation from C program Verification with SAT solver (Chaff) 256 Checking over bound access to array int exam () { int array[3], i, sum=0; for (i=0; i<=3; i++) { array[i] = input(); sum = sum + array[i]; } return sum; } CBMC can detect the over bound access to array indices This means the value is input at this point This program is faulty since array[3] is accessed when i = 3 If (i <= 3) is replaced by (i < 3), this program becomes correct 257 Assertion checking int main () { unsigned char a, b; unsigned char ai, bi; unsigned int result = 0, i; a = input; b = input; for (i = 0; i < 8; i++) { bi = (b>>i); ai = (a<<i); if ( bi & 1) result += ai; } assert (result == a * b); } CBMC can verify datadominant properties <-> control-dominant properties as “safety properties” Suppose i=1 101 (a) × 1010 (b) bi = 1 ai = 10100 This corresponds to the sub-product of (a) * (2nd digit of b) 258 Experimental results Using CBMC, the behavioral consistency of C and Verilog programs can be checked Behavioral consistent? Verilog C Some experimental results are reported below* PS/2 interface 700 lines of Verilog, unwinding bound 48, run time 51 sec. DLX processor Verilog design with 1219 latches, 550 lines of C, run time 97 sec., detected a counter example of length 5 cycles *: Behavioral Consistency of C and Verilog Using Bounded Model Checking (Proc. of DAC’03) 259 Final remarks: Verification directions Driven by design flow Higher levels of abstraction Formal specification languages Mapping verification problems to lower level engines Design reuse Interface verification System level verification Tackling larger designs in formal verification Efficient formal engines Sequential equivalence checkers Filter based techniques Using multiple engines Hybrid engines E.g. BDD/SAT/ATPG combination Higher level reasoning Need to automate 260 Final remarks: Research issues Design and verification at high levels of abstraction New modeling issues Eg: what if Spec is in UML How to generate problem, map problem Faster engines More efficient BDDs Efficient and automatic abstraction-refinement Faster SAT solvers Better learning and pruning techniques Combining engines ATPG/SAT combination BDD/SAT combination Use of higher level information to guide search Methodology issues Interface specification and verification Automatic static checks 261 Bibliography on verification 262 Books B. Berard et. al., “Systems and Software Verification: Model Checking Techniques and Tools”, Springer Verlag, 2001. J. Bergeron, “Writing Testbenches: Functional Verification of HDL Models”, Kluwer Academic Publishers, Boston, 2000. D.D. Gajski et. al., “SpecC: Specification Language and Methodology”, Kluwer Academic Publishers, Boston, 2000. J. Bhasker, “ A SystemC Primer ”, Star Galaxy Press, Allentown, 2002. M. Suart and D. Dempster, “ Verification Methodology Manual for Code Coverage in HDL Designs”, Teamwork International, Hampshire, UK, 2000. K. L. McMillan, ``Symbolic Model Checking'', Kluwer Academic Publishers, 1993. Z. Manna and A. Pnueli, “Temporal Specification and Verification of Reactive Systems” Vol. I and II, Springer 1995. Ching-Tsun Chou, "The Mathematical Foundation of Symbolic Trajectory Evaluation", Springer-Verlag 1999. Thomas Kropf: "Introduction to Formal Hardware Verification", (Springer Verlag; ISBN: 3540654453, 299 pages, January 2000) E. M. Clarke, O. Grumberg and D. Peled, "Model Checking", (MIT Press; ISBN: 0262032708; 330 pages; January 2000) G. J. Holzmann, “Design and Validation of Computer Protocols”, Prentice Hall, 1991. M. P. Fourman, “Formal System Design”, Formal Methods for VLSI Design, IFIP, 1990, North-Holland. C. Meinel and T. Theobald, “Algorithms and Data Structures in VLSI Design”, Springer-Verlag, 1998. Hassan Gomaa, “Designing Concurrent, Distributed and Real-Time Applications with UML”, Addison-Wesley, July 2000. 263 Books L. Bening and H. Foster, “Principles of Verifiable RTL Design: Functional Coding Style Supporting Verification Processes in Verilog”, published by Kluwer Academic Publishers, 2000. R. P. Kurshan, “Computer Aided Verification of Coordinating Processes”, Princeton University Press, 1994. Robert B. Jones, “Symbolic Simulation Methods for Industrial Formal Verification”, Kluwer Academic Publishers, Boston, 2002. M. Yoeli, "Formal Verification of Hardware Design", IEEE Computer Society Press, 1991. (Book containing a collection of papers) R. P. Kurshan, “Computer Aided Verification of Coordinating Processes”, Princeton University Press, 1994. G. J. Holzmann, “Design and Validation of Computer Protocols”, Prentice Hall, 1991. M. P. Fourman, “Formal System Design”, Formal Methods for VLSI Design, IFIP, 1990, NorthHolland. C. Meinel and T. Theobald, “Algorithms and Data Structures in VLSI Design”, Springer-Verlag, 1998. M. Kaufmann, P. Manolios, and J S. Moore, "Computer-Aided Reasoning: An Approach", (Kluwer Academic Publishers, June 2000; ISBN 0792377443) Robert B. Jones, Symbolic Simulation Methods for Industrial Formal Verification, Kluwer Academic Publishers, Boston, 2002. M. Yoeli, "Formal Verification of Hardware Design", IEEE Computer Society Press, 1991. (Book containing a collection of papers) M. Kaufmann, P. Manolios, and J S. Moore, "Computer-Aided Reasoning: An Approach", (Kluwer Academic Publishers, June 2000; ISBN 0792377443) M. Keating and P. Bricaud “Reuse Methodology Manual for System-On-A-Chip Designs,” Kluwer Academic Publishers, June 1998. 264 Papers High Level Design and Verification Modeling D. D. Gajski, ``IP-Based Design Methodology'', Proc. of the 36th Design Automation Conference, pp. 43, New Orleans, June 1999. D. Kroening and E. Clarke, “Behavioral consistency of C and Verilog programs using bounded model checking,” in Proc. DAC, June 2003. T. Sakunkonchak and M. Fujita, “Verification of synchronization in SpecC description with the use of difference decision diagram,” IEICE Trans. Fundamentals, Vol. E85-A, Jan 2002. T. Matsumoto and M. Fujita, “Equivalence checking of C-based hardware descriptions by using symbolic simulation and program slicer,” in Proc. IWLS, May 2003. T. Ball and S. Rajamani, “Checking Temporal Properties of Software with Boolean Programs”, in Proc. Computer Aided Verification 2000, [Microsoft SLAM project] R. Bryant et . al. “Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic” in ACM Trans. on Computational Logic, Vol 2., 2001. S. Singh, “Design and Verification of CoreConnectTM IP using Esterel,” in Proc CHARME 2003 S. Sutherland, “System Verilog 3.1 Its what the DAVEs in you company asked for”. in Proc. DVCON 2003 S. Abdi, D. Shin and D. Gajski, "Automatic Communication Refinement for System Level Design,” Proceedings of Design Automation Conference, Anaheim, CA, June 2003. W. Mueller, R. Dömer, A. Gerstlauer, "The Formal Execution Semantics of SpecC," in Proceedings of International Symposium on System Synthesis, October 2002. 265 Papers Theorem Proving & Decision Procedures S. Owre and S. Rajan and J.M. Rushby and N. Shankar and M.K. Srivas, “PVS: Combining Specification, Proof Checking, and Model Checking”, 411-414, CAV96. S. Owre and S. Rajan and J.M. Rushby and N. Shankar and M.K. Srivas, “PVS: Combining Specification, Proof Checking, and Model Checking”, 411-414, CAV96. D. Cyrluk, S. Rajan, N. Shankar and M. K. Srivas, “Effective Theorem Proving for Hardware Verification”, pp. 287-305, TPCD94. S. J. Garland and J. V. Guttag, “An Overview of LP: the Larch Prover”, Proceedings of the Third International Conference on Rewriting Techniques and Applications, 1989, Springer-Verlag. J. Staunstrup and M. Greenstreet, “Synchronized Transitions”, Formal Methods for VLSI Design, 1990, IFIP, North-Holland. R. Vemuri, “How to Prove the Completeness of a Set of Register Level Design Transformations”, Proceedings of the 27th ACM/IEEE Design Automation Conference, 1990, 207—212. D. Cyrluk, S. Rajan, N. Shankar and M. K. Srivas, “Effective Theorem Proving for Hardware Verification”, pp. 287-305, TPCD94. S. J. Garland and J. V. Guttag, “An Overview of LP: the Larch Prover”, Proceedings of the Third International Conference on Rewriting Techniques and Applications, 1989, Springer-Verlag. J. Staunstrup and M. Greenstreet, “Synchronized Transitions”, Formal Methods for VLSI Design, 1990, IFIP, North-Holland. C. M. Angelo, “Formal Hardware Verification ina Silicon Compilation Environment by means of Theorem Proving”, Ph.D. Dissertation, Katholieke Universiteit Leuven (February, 1994). 266 Papers R. Vemuri, “How to Prove the Completeness of a Set of Register Level Design Transformations”, Proceedings of the 27th ACM/IEEE Design Automation Conference, 1990, 207—212. Jeffrey J. Joyce and Carl-Johan H. Seger, “Linking Bdd Based Symbolic Evaluation to Interactive Theorem Proving”, Proceedings of the 30th Design Automation Conference, 1993. S. P. Rajan, N. Shankar and M. Srivas, “An Integration of Model-Checking with Automated Proof Checking”, 7th Conference on Computer-Aided Verification, July, 1995. M.D. Aagard, R.B. Jones and C.-J.H. Seger, “Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment”, Proceedings of DAC 1998, pp. 538-541 C.W. Barrett, D.L. Dill and J.R. Levitt, “A Decision Procedure for Bit-Vector Arithmetic”, Proceedings of DAC 1998 J.R. Burch and D.L. Dill, “Automatic Verification of Pipelined Microprocessor Control”, Proceedings of CAV 1994 J.X. Su, D.L. Dill and C.W. Barrett, “Automatic Generation of Invariants in Processor Verification”, Proceedings of FMCAD 1996 M. Aagaard, M. E. Leeser, and P. J. Windley, “Toward a Super Duper Hardware Tactic”, in Higher Order Logic Theorem Proving and its Applications: 6th International Workshop, HUG'93, Vancouver, B.C., August 11-13 1993: Proceedings, edited by J. J. Joyce and C.-J. H. Seger, Lecture Notes in Computer Science, vol. 780 (SpringerVerlag, 1994), pp. 399-412. F. Andersen, K. D. Petersen, and J. S. Pettersson, `A Graphical Tool for Proving UNITY Progress', in Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop, Valletta, Malta, September 1994: Proceedings, edited by T. F. Melham and J. Camilleri, Lecture Notes in Computer Science, Volume 859 (SpringerVerlag, 1994), pp. 17-32. 267 Papers S. Agerholm, `Domain Theory in HOL', in Higher Order Logic Theorem Proving and its Applications: 6th International Workshop, HUG'93, Vancouver, B.C., August 11-13 1993: Proceedings, edited by J. J. Joyce and C.-J. H. Seger, Lecture Notes in Computer Science, vol. 780 (Springer-Verlag, 1994), pp. 295-310. S. Agerholm, `Formalising a Model of the lambda-calculus in HOL-ST' Technical Report Number 354, University of Cambridge Computer Laboratory (1994). S. Agerholm, “A HOL Basis for Reasoning about Functional Programs”, Ph.D. Dissertation, BRICS Technical Report RS-94-44, Department of Computer Science, University of Aarhus (December 1994). S. Agerholm, “LCF Examples in HOL”, The Computer Journal, vol. 38, no. 2 (July 1995), pp. 121-130. S. Agerholm, `Mechanizing Program Verification in HOL', in Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1991, edited by M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley (IEEE Computer Society Press, 1992), pp. 208-222. S. Agerholm, `Mechanizing Program Verification in HOL', M.Sc. Dissertation, DAIMI Report Number IR-111, Department of Computer Science, University of Aarhus (April 1992). S. Agerholm “Non-Primitive Recursion Function Definition”, in Higher Order Logic Theorem Proving and Its Applications: 8th International Workshop, Aspen Grove, Utah, September 1995: Proceedings, edited by E. T. Schubert, P. J. Windley, and J. Alves-Foss, Lecture Notes in Computer Science, Volume 971 (Springer-Verlag, 1995), pp. 17-31. F. Andersen and K. D. Petersen, `Recursive Boolean Functions in HOL', in Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1991, edited by M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley (IEEE Computer Society Press, 1992), pp. 367-377. Papers C. M. Angelo, L. Claesen, and H. De Man, “Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL”, in Higher Order Logic Theorem Proving and its Applications: 6th International Workshop, HUG'93, Vancouver, B.C., August 11-13 1993: Proceedings, edited by J. J. Joyce and C.-J. H. Seger, Lecture Notes in Computer Science, vol. 780 (Springer-Verlag, 1994), pp. 89-100. C. M. Angelo, L. Claesen, and H. De Man, `The Formal Semantics Definition of a MultiRate DSP Specification Language in HOL', in Higher Order Logic Theorem Proving and its Applications: Proceedings of the IFIP TC10/WG10.2 International Workshop, Leuven, September 1992, edited by L. J. M. Claesen and M. J. C. Gordon, IFIP Transactions A-20 (North-Holland, 1993), pp. 375-394. C. M. Angelo, L. Claesen, and H. De Man, “Modeling Multi-rate DSP Specifiction Semantics for Formal Transformational Design in HOL”, Formal Methods in System Design, vol. 5, nos. 1/2 (July 1994), pp. 61-94. R. J. R. Back and J. von Wright, `Predicate Transformers and Higher Order Logic', in Semantics: Foundations and Applications: REX Workshop, Beekbergen, June 1992, edited by J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, Lecture Notes in Computer Science, Volume 666 (Springer-Verlag, 1993), pp. 1-20. R. J. R. Back and J. von Wright, `Refinement Concepts Formalised in Higher Order Logic', Formal Aspects of Computing, Vol. 2, No. 3 (July-September 1990), pp. 247-272. S. Bainbridge, A. Camilleri, and R. Fleming, `Industrial Application of Theorem Proving to System Level Design', in Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1991, edited by M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley (IEEE Computer Society Press, 1992), pp. 130-142. F. Andersen, K. D. Petersen, and J. S. Pettersson, `Program Verification using HOLUNITY', in Higher Order Logic Theorem Proving and its Applications: 6th International Workshop, HUG'93, Vancouver, B.C., August 11-13 1993: Proceedings, edited by J. J. Joyce and C.-J. H. Seger, Lecture Notes in Computer Science, vol. 780 (SpringerVerlag, 1994), pp. 1-15. 268 269 Papers R. H. Beers and P. J. Windley, `Abstracting Signals: The waveform Library', in Supplementary Proceedings of the 9th International Conference on Theorem Proving in Higher Order LogicsL TPHOLs ’96, edited by J. von Wright, J. Grundy, and J. Harrison, TUCS General Publication No 1, Turku Centre for Computer Science (August, 1996), pp. 1-13. G. Birtwistle and B. Graham, `Verifying SECD in HOL', in Formal Methods for VLSI Design: IFIP WG 10.2 Lecture Notes, edited by J. Staunstrup (North-Holland, 1990), pp. 129-177. G. Birtwistle, B. Graham, and S.-K. Chin, “New theory HOL: An Introduction to Hardware Verification in Higher Order Logic”, (August 1994). [Published electronically.] R. Boulton, `Boyer-Moore Automation for the HOL System', in Higher Order Logic Theorem Proving and its Applications: Proceedings of the IFIP TC10/WG10.2 International Workshop, Leuven, September 1992, edited by L. J. M. Claesen and M. J. C. Gordon, IFIP Transactions A-20 (North-Holland, 1993), pp. 133-142. R. Boulton, “Combining Decision Procedures in the HOL System”, in Higher Order Logic Theorem Proving and Its Applications: 8th International Workshop, Aspen Grove, Utah, September 1995: Proceedings, edited by E. T. Schubert, P. J. Windley, and J. Alves-Foss, Lecture Notes in Computer Science, Volume 971 (Springer-Verlag, 1995), pp. 75-89. R. J. Boulton, “Efficiency in a Fully-Expansive Theorem Prover”, Ph.D. Dissertation, Technical Report Number 337, University of Cambridge Computer Laboratory (May 1994). 270 Papers Formal Verification: SAT Solvers J. Marques-Silva and K. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability”, IEEE Transactions on Computers, 48(5):506-521, May 1999 M. Sheeran and G. Stalmarck, “A tutorial on Stalmarck’s proof procedure for propositional logic”, Formal Methods in System Design, 16(1):23-58, January 2000 M.H. Moskewicz et. al., “Chaff: engineering an efficient SAT solver,” in Proc. Design Automation Conf., June 2001. E. Goldberg and Y. Novikov, “BerkMin: a Fast and Robust Sat-Solver”, Proceedings of Design Automation and Test in Europe, pp.142-149, March 2002. Formal Verification: BDDs R. E. Bryant, “Graph Based Algorithms for Boolean Function Manipulation”, IEEE Transactions on Computers, Vol. C-35-8, pp. 677- 691, August 1986 R. Rudell, “Dynamic Variable Ordering for Ordered Binary Decision Diagrams”, Proceedings of ICCAD 1993, pp. 42- 45 R. E. Bryant, “On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication”, IEEE Transactions on Computers, Vol. 40, No. 2, pp, 205-213, February 1991 B. Bollig and I. Wegener, “Improving the variable ordering for OBDDs is NP-complete”, IEEE Transactions on Computers, Vol. 45, No. 9, pp. 993-1002, September 1996 M. Fujita, H. Fujitsawa and Y. Matsunaga, “Variable Ordering Algorithms for Ordered Binary Decision Diagrams and their Evaluation”, IEEE Transactions on ComputerAided Design of Integrated Circuits and Systems, Vol. 12, No. 1, pp. 6- 12, January 1993 R. Bryant, “Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams”, slides from a presentation by Prof. Bryant in August 1999 271 Papers Formal Verification: Symbolic Model Checking (BDDs) D. L. Dill, “The Mur Verification System”, 390-393, CAV96. R. Bryant, E. Clarke, K. McMillan and A. Emerson, “Binary Decision Diagrams and Symbolic Model Checking”, slides from a presentation at Symposium on Algorithms in the Real World, May, 2000 E. M. Clarke, E. A. Emerson and A. P. Sistla, ``Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications'', ACM Trans. on Programming Language and Systems, Vol.8, No.2, pp 244-263, April 1986. J. Burch, E. Clarke, D. Long, K. McMillan, D. Dill, “Symbolic Model Checking for Sequential Circuit Verification”, IEEE Trans. Computer Aided Design, 13, 1994, 401424. C. Kern and M. Greenstreet, "Formal Verification in Hardware Design: A Survey", ACM Transactions on Design Automation of E. Systems, Vol. 4, April 1999, pp. 123-193. H. Iwashita and T. Nakata, `` Forward Model Checking Techniques Oriented to Buggy Designs'', Proceedings of ICCAD, pp. 400-404, 1997. K. Takayama, T. Satoh, T. Nakata, and F. Hirose, ``An approach to Verify a Large Scale System-on-a-chip Using Symbolic Model Checking'', Proceedings of ICCD, 1998. A. J. Hu, “Formal Hardware Verification with BDDs : An Introduction”, ACM Transactions on Programming Languages and Systems, 1997. M. Kaufmann, A. Martin, and C. Pixley, "Design Constraints in Symbolic Model Checking", Proc. CAV-98, pp. 477-487, 1998. K. L. McMillan, "Fitting formal methods into the design cycle", Proceedings of the 31st Design Automation Conference, pp. 314-19, 1994 272 Papers Formal Verification with SAT solvers P. Abdulla, P. Bjesse and N. Een, “Symbolic Reachability Analysis Based on SAT Solvers”, Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 41-425, March 2000 P. Williams et al, “Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking”, Proc. of the 12th CAV, pp. 124-138, July 2000 M. Sheeran, S. Singh and G. Stalmarck, “Checking Safety Properties Using Induction and a SAT Solver”, Proc. of the 3rd Intl. Conference on Formal Methods in CAD (FMCAD), pp. 208-125, Nov. 2000 P. Bjesse and K. Claessen, “SAT-based Verification without State Space Traversal”, Proc. of the 3rd FMCAD, pp. 372-389, Nov. 2000 K.L. McMillan, “Applying SAT Methods in Unbounded Model Checking”, Proc. of the 14th CAV, pp. 250-264, July 2002 K.L. McMillan, “Interpolation and SAT-based Model Checking”, Proc. of the 15th CAV, July 2003 I. Park and H. Kang, “SAT-based unbounded symbolic model checking”, Proceedings of DAC, pp. 840-843, June 2003 273 Papers Equivalence Checking D. Brand, “Verification of Large Synthesized Designs”, Proceedings of ICCAD, November 1993, pp. 534-537 A. Kuehlmann and F. Krohm, “Equivalence Checking using Cuts and Heaps”, Proceedings of DAC 1997, pp. 263-268 Y. Matsunaga, “An Efficient Equivalence Checker for Combinational Circuits”, Proceedings of DAC 1996, pp. 629-634 R. Mukherjee, J. Jain, K. Takayama, M. Fujita, J. Abraham and D. Fussell, “An Efficient Filter Based Approach for Combinational Verification”, in IEEE Transactions on CAD, 18:1542-1557, Nov. 1999 H. Cho and C. Pixley, “Apparatus and Method for deriving correspondences between storage elements of a first circuit model and storage elements of a second circuit model”, U.S. Patent 5,638,381, June 1997 K. Ng, M. Prasad, R. Mukherjee and J. Jain, “Solving the Latch Mapping Problem in an Industrial Setting”, Proceedings of DAC 2003, pp. 442-447 C.A.J. van Eijk, “Sequential Equivalence Checking Based on Structural Similarities”, IEEE Transactions on CAD, 19(7):814-819, July 2000 S.-Y. Huang, K.-T. Cheng, K.-C. Chen and F. Brewer, “AQUILA: An Equivalence Checking System for Large Sequential Circuits”, IEEE Transactions on Computers, 49(5), May 2000 274 Papers Semi-Formal Verification R. E. Bryant, “Symbolic Simulation -- Techniques and Applications”, Proceedings of DAC 1990 R.B. Jones, “Applications of Symbolic Simulation to the Formal Verification of Microprocessors”, Ph.D. Thesis, Computer Systems Laboratory, Stanford University, August 1999 R.E. Bryant and C.J.H. Seger, “Formal hardware verification by symbolic trajectory evaluation,” in Proc. Design Automation Conf., June 1991. C.-J.H. Seger and R.E. Bryant, “Formal Verification by Symbolic Evaluation of Partially Ordered Trajectories”, Formal Methods in System Design, Vol. 6, No. 2, pp. 147-190, 1995 E. Clarke, A Biere, R. Raimi and Y. Zhu, “Bounded Model Checking Using Satisfiability Solving”, in Formal Methods in System Design, 19(1): 7-34, July 2001, Kluwer Academic Publishers O. Shtrichman, “Tuning SAT Checkers for bounded model checking,” in Proc. Int. Conf. on Computer-Aided Verification, July 2000. F. Fallah, “Binary Time-Frame Expansion”, Proc. of ICCAD, pp. 458-464, Nov. 2002 A. Gupta et al, “Learning from BDDs in SAT-based bounded model checking,” in Proc. Design Automation Conf., June 2003. V. Boppana, S. Rajan, K. Takayama and M. Fujita, “Model Checking Based on Sequential ATPG”, Proceedings of CAV, pp. 418-430, July 1999. J. Abraham, V. Vedula and D. Saab, “Verifying Properties Using Sequential ATPG”, Proceedings of International Test Conference, October 2002 275 Papers D. Dill and S. Tasiran, "Simulation meets Formal Verification?", slides from a presentation at ICCAD'99. D. Dill, "Alternative Approaches to Formal Verification (Symbolic Simulation)", slides from a presentation at CAV 1999. C. H. Yang and D. L. Dill, “Validation with Guided Search of the State Space”, Proceedings of DAC 1998 M. Ganai et al, “SIVA: A System for Coverage Directed State Space Search”, In Journal of Electronic Testing: Theory and Applications (JETTA), February 2001 P.-H. Ho et al, “Smart Simulation Using Collaborative Formal and Simulation Engines”, Proceedings of ICCAD, pp. 120-126, November 2000 Y. Hoskote, T. Kam, P. Ho and X. Zhao, ``Coverage Estimation for Symbolic Model Checking'', Proc. of the 36th Design Automation Conference, New Orleans, June 1999. S. Katz, O. Grumberg and D. Geist, ``Have I written enough properties? - A method of comparison between specification and implementation'', Technical Report, IBM Haifa Research Laboratory, Haifa, Israel, 1999. Model Checking in Practice S. Berezin, S. Campos and E. M. Clarke, ``Compositional Reasoning in Model Checking'', Technical Report - CMU-CS-98-106, School of Computer Science, Carnegie Mellon University, February, 1998. Papers K. L. McMillan, "A compositional rule for hardware design refinement", Computer Aided Verification (CAV97), O. Grumberg (Ed.), Haifa, Israel, pp. 24-35, 1997. T.A.Henzinger, S. Qadeer, and S.K.Rajamani, "You assume, We guarantee : Methodology and Case Studies" CAV98: Computer Aided Verification, Lecture Notes in Computer Science, Springer-Verlag, pp. 440-451, 1998. G. Mosensoson, “Practical Approaches to SoC Verification”, DATE 2000. J. L. Nielsen, H. R. Andersen, G. Behrmann, H. Hulgaard, K. Kristoffersen and K. G. Larsen, “Verification of Large State/Event Systems using Compositionality and Dependency Analysis”, Proceedings of TACAS 1998, LNCS 1384, April 1998. D. Geist, G. Biran, T. Arons, M. Slavkin, Y. Nustov, M. Farkas, and K. Holtz, “A Methodology for the verification of a System on Chip”, Proc. Of DAC 1999, pp. 574-579. A. Evans, A. Silburt, G. Vrckovnik, T. Brown, M. Dufresne, G. Hall, T. Ho and Y. Liu, “Functional Verification of Large ASICs”, Proc. Of DAC, 1998. S. Taylor, M. Quinn, D. Brown, N. Dohm, S. Hildebrandt, J. Higgins and C. Ramey, “Functional Verification of a Multiple-issue, Out-of-Order, Superscalar Alpha Processor – the DEC Alpha 21264 Microprocessor”, Proc. Of DAC, 1998. T. Henzinger, X. Liu, S. Qadeer and S. Rajamani, “Formal Specification and Verification of a Dataflow Processor Array,”Proceedings of ICCAD 1999 D. Wang, “SAT based Abstraction Refinement for Hardware Verification”, Ph.D. thesis, ECE Dept., Carnegie Mellon University, May 2003 Shankar G. Govindaraju, David L. Dill, Alan J. Hu, and Mark A. Horowitz. "Approximate Reachability with BDDs using Overlapping Projections,” in Proc. DAC 1998 Gaurishankar Govindaraju, "Approximate Symbolic Model Checking using Overlapping Projections" Ph.D. thesis, Stanford University, August 2000. 276 Papers Simulation Based Verification I. Ghosh and M. Fujita, ``Automatic test pattern generation for functional registertransferlevel circuits using assignment decision diagrams,'' IEEE. Trans. on ComputerAided Design, Vol. 20, No. 3, pp. 402-415, March 2001. F. Fallah, S. Devadas, and K. Keutzer, ``OCCOM: Efficient computation of observabilitybased code coverage metrics for functional verification,'' IEEE. Trans. on ComputerAided Design, Vol. 20, No. 8, pp. 1003-1015, Aug. 1998. F. Fallah, S. Devadas, and K. Keutzer, ``Functional vector generation for HDL models using linear programming and 3-satisfiability,”{\em IEEE. Trans. on Computer-Aided Design}, Vol. 20, No. 8, pp. 994-1002, Aug. 1998. S. Ravi, G. Lakshminarayana, and N.K. Jha, ``TAO: Regular expression based high-level testability analysis and optimization,'' in Int. Test Conf., pp. 331-340, Oct. 1998. I. Ghosh and S. Ravi, “On automatic generation of RTL validation test benches using circuit testing techniques,” in Proc. Great Lakes Symposium on VLSI, April 2003. L. Zhang, I. Ghosh and M. Hsiao, “Efficient sequential ATPG for functional RTL circuits,” in Proc. International Test Conference, Oct. 2003. L. Zhang, I. Ghosh and M. Hsiao, “Automatic design validation framework for HDL descriptions via RTL ATPG,” in Proc. Asian Test Symposium, Nov. 2003 F. Fallah, I. Ghosh, and M. Fujita, “Event driven observability enhanced coverage analysis of C programs for functional validation,” in {\em Proc. Asia and South Pacific Design Automation Conference}, Jan. 2003. K. Ara and K. Suzuki, “A proposal for transaction level verification with component wrapper language,” Proc. Design Automation and Test in Europe, March 2003. A. U. Shankar, "An Introduction to Assertional Reasoning for Concurrent Systems", ACM Computing Surveys, Sept. 1993, Vol 25, No. 3, pp. 225-262 277 278 Papers S. Ramesh and P. Bhaduri, “Validation of Pipelined Processor Designs using Esterel Tools: A Case Study”, Proc. of CAV '99, LNCS Vol. 1633, 1999. C. Eisner et. al. “The Temporal Logic Sugar” in Proc. Int Conf. on Computer-aided Verification 2001. Miscellaneous J. Jain, W. Adams and M .Fujita, “Sampling Schemes for Computing OBDD Variable Orderings”, Proceedings of ICCAD 1998, pp. 331-338 J. Jain, R. Mukherjee and M. Fujita, “Advanced Verification Technique Based on Learning”, Proceedings of DAC 1995, pp. 420-426 C. H. Yang and D. L. Dill, “Validation with Guided Search of the State Space”, Proceedings of DAC 1998 A. Jain, “Formal Hardware Verification by Symbolic Trajectory Evaluation”, Ph.D. Thesis, Dept. of Electrical and Computer Engineering, Carnegie Mellon University, August 1997 C.-J.H. Seger and R.E. Bryant, “Formal Verification by Symbolic Evaluation of Partially Ordered Trajectories”, Formal Methods in System Design, Vol. 6, No. 2, pp. 147-190, 1995 279 Important web-sites http://www.comlab.ox.ac.uk/archive/formal-methods.html http://www.csl.sri.com http://www-cad.eecs.Berkeley.edu/ vis http://godel.ece.utexas.edu/texas97-benchmarks/ http://citeseer.nj.nec.com/ http://www.rational.com/uml (Universal Modelling Language HOME-PAGE) http://www-sop.inria.fr/meije/verification/esterel http://www.accellera.org http://www.systemC.org http://www.specC.org 280 Conference Proceedings Computer Aided Verification (CAV) Formal Methods in Computer Aided Design (FMCAD) International Conference on Computer-Aided Design (ICCAD) International Conference on Computer Design (ICCD) Design Automation Conference (DAC) Asia South Pacific Design Automation Conference (ASPDAC) International Conference on VLSI Design (VLSI) Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) 281 Journals/Magazines IEEE Design and Test of Computers IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems IEEE Transactions on Computers IEEE Transactions on VLSI Systems ACM Transactions on Design Automation of Electronic Systems Formal Methods in System Design Formal Aspects of Computing

Descargar
# Simulation Based Verification