TUTORIAL No. 3 High Level Design Validation: Current Practices & Future Trends 17th International Conference on VLSI Design Mumbai, India Januray 5th, 2004 Authors Prof. Masahiro Fujita Member of Research Staff Fujitsu Labs. of America Sunnyvale, CA, USA Email: [email protected] Professor Dept. of Electronic Engineering University of Tokyo, Japan Email: [email protected] Dr. Mukul Prasad Member of Research Staff Fujitsu Labs. of America Sunnyvale, CA, USA Email: [email protected] Dr. Indradeep Ghosh Dr. Rajarshi Mukherjee Member of Technical Staff Calypto Design Automation Santa Clara, CA, USA Email: [email protected] Outline & Introduction MASAHIRO FUJITA University of Tokyo Tokyo, Japan [email protected] Tutorial Outline Introduction High level design flow and verification issues Theorem proving and Decision procedures Formal verification techniques for FSM models Semi-formal verification techniques Simulation based verification techniques Conclusions and future directions Necessity of high level verification Over 70% of system LSI design time is for “verification” Over 50% reason of “re-spin” of ASIC designs is functional design errors Need to find as many bugs and as early as possible Once “golden models” are created, never introduce design errors Remaining bugs Time 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 problem Formal Verification “Prove” the correctness of designs Possible mathematical models Both design and spec must be represented with mathematical models Mathematical reasoning Equivalence 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 very important In many cases, it determines the total performance Spec Design Front-end tool Mathematical models Verification engines 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 Example: Formal vs Simulation (Cont.) Verification of Exclusive-OR circuit with “simulation” z and ~x&y+x&~y are equal for all cases Need to simulate 2**N cases 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 Example: Formal vs Simulation (Cont.) Verification of Exclusive-OR circuit with “formal verification” z = ~b + ~c b 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 z Design Representation in High level Super state: Need multiple cycles for executions 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 Fusing Simulation and Formal Verification: Semi-formal Verification Techniques Not so easy... Simulation patterns cannot be used for formal verification (meaningless if used) Properties cannot be “simulated” as it is Anyway, write down properties... Assertion-based verification Switch between formal and simulation-based dynamically … Property Simulation Patterns Tutorial Outline Introduction High level design flow and verification issues Theorem proving and decision procedures Formal verification techniques for FSM models Semi-formal verification techniques Simulation based verification techniques Conclusions and future directions High-Level Design Flow & Verification Issues MASAHIRO FUJITA University of Tokyo Tokyo, Japan [email protected] Section Outline System LSI design From requirement to specification/functional descriptions From functional description to implementation Verification problems in the design methodology Verification techniques for high level designs System LSI Design System-on-Chip (SOC) design Increase of design complexity Level System Number of components 1E0 1E2 1E3 RTL Gate 1E4 1E5 1E6 Transistor 1E7 Accuracy Algorithm Abstraction 1E1 Introduction 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 System-On-Chip Design Specification to architecture to implementation Behavior 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 Section Outline System LSI design From requirement to specification/functional descriptions From functional description to implementation Verification problems in the design methodology Verification techniques for high level designs From Requirement to Specification/functional Descriptions What is UML? UML is a language for: Specifying, Visualizing, Constructing, and Documenting Software Artifacts What does a modeling language provide? Model elements: Concepts and semantics Notation: Visual rendering of model elements Guidelines: Hints and suggestions for using elements in notation Representing System Architecture Logical View Implementation View End-user Functionality Programmers Software management Use Case View Process View Deployment View System integrators Performance Scalability Throughput Conceptual System engineering System topology Delivery, installation Communication Physical The Goals of UML Ready-to-use, expressive visual modeling language that promotes development/Exchange Extensibility/specialization of core concepts Independent of programming languages and development processes Formal basis for understanding language Encourage growth of OO tools market Support higher level design concepts Collaborations, frameworks, patterns, etc. Integrate the best practices of all OOD UML Modeling Constructs/diagrams: Static vs. Dynamic Perspectives A diagram is a view into a model Presented from the aspect of a particular stakeholder Provides a partial representation of the system Is semantically consistent with other views In UML, there are nine standard diagrams Static Views: Use Case, Class, Object, Component, Deployment Dynamic Views: Sequence, Collaboration, Statechart, Activity UML Modeling Constructs/diagrams: Classification by Capability/timeline Use-Case Diagrams Class and Object Diagrams Behavior Diagrams Interaction Diagrams Statechart Diagrams Activity Diagrams Sequence Diagram Collaboration Diagram Implementation Diagrams Component Diagram Deployment Diagram Relationship of Models and Diagrams Use Case Use Case Diagrams Sequence Diagrams Diagrams Scenario Scenario Diagrams Collaboration Diagrams Diagrams Scenario Scenario Diagrams Statechart Diagrams Diagrams Use Case Use Case Diagrams Use Case Diagrams Diagrams State State Diagrams Class Diagrams Diagrams State State Diagrams Object Diagrams Diagrams State State Diagrams Component Diagrams Diagrams Models Component Component Diagrams Deployment Diagrams Activity Diagrams Diagrams Description Example Host interface for compact flash memory Interface between NAND type flash memory and host PC Use data buffer for asynchronous data transfer and protocols Use Case diagram Data transfers with protocol change Host PC Design target Confirm and change various status NAND flash memory Interface between NAND Flash Memory and the Design Target Use Case diagram Confirm /change status NAND flash memory Buffer Data read/write CPU Activity Diagram Wait Wait ATA command/Interrupt Interpret command NAND status Busy Ready Send status to CPU Data transfer b/w Host and the design target Send status to CPU Sequence Diagram Data buffer Synchronous IF CPU NAND flash memory Ask status Ready Get access right Request data transfer Data transfer Start transfer Data transfer Finish transfer Finish transfer Busy Section Outline System LSI design From requirement to specification/functional descriptions From functional description to implementation Verification problems in the design methodology Verification techniques for high level designs Abstraction Levels Structure / Implementation detail Order / Timing detail Requirements Constraints Application domain MOCs (Matlab, SDF, etc.) Functional Specification Untimed (causality) Structural Architecture Timed (estimated) Busfunctional Communication Timingaccurate RTL/IS Implementation Cycleaccurate Manufacturing Gate netlist Many small steps of incremental refinement Gate delays Design Flow Structure / Implementation detail Order / Timing detail System design Capture Functional Algor. IP Untimed (causality) Specification model Architecture exploration Comp. IP Timed (estimated) Architecture model Structural Communication synthesis Busfunctional Proto. IP Timingaccurate Communication model RTL IP RTL/IS Hardware synthesis Interface Software synthesis compilation Implementation model Backend RTOS IP Cycleaccurate SpecC Methodology System design Validation flow Capture Algor. IP Compilation Specification model Architecture exploration Validation Analysis Estimation Comp. IP Compilation Architecture model Communication synthesis Proto. IP Compilation Hardware synthesis Interface Software synthesis compilation Backend Simulation model Validation Analysis Estimation RTOS IP Compilation Implementation model Simulation model Validation Analysis Estimation Communication model RTL IP Simulation model Validation Analysis Estimation Simulation model Specification Model High-level, abstract model No implicit structure / architecture Pure system functionality Algorithmic behavior No implementation details Behavioral hierarchy Untimed Executes in zero (logical) time Causal ordering Events only for synchronization Specification model Architecture exploration Architecture model Communication synthesis Communication model Backend Implementation model Specification Model Example Simple, typical specification model Hierarchical parallel-serial composition Communication through ports and variables, events B1 B1 v1 B2 v2 e2 B3 Architecture Exploration Specification model Component allocation / selection Architecture exploration Architecture model Behavior partitioning Communication synthesis Communication model Variable partitioning Backend Implementation model Scheduling Allocation, Behavior Partitioning B1 B1 PE1 Allocate PEs Partition behaviors Globalize communication PE2 v1 B2 B3 c2 Additional level of hierarchy to model PE structure Architecture Model Example PE1 PE2 B1 B1 v1 B13snd cb13 B13rcv v1 B2 B3 c2 B34rcv cb34 B34snd Architecture Model Component structure/architecture Top level of behavior hierarchy Specification model Architecture exploration Behavioral/functional component Architecture model view Communication synthesis Behaviors grouped under top-level component behaviors Sequential behavior execution Timed Estimated execution delays Communication model Backend Implementation model Communication Synthesis Bus allocation / protocol selection Specification model Architecture exploration Channel partitioning Architecture model Communication synthesis Protocol, transducer insertion Communication model Backend Inlining Implementation model Bus Allocation / Channel Partitioning PE1 PE2 B1 B1 Allocate busses Partition channels Update communication Bus1 v1 B13snd cb13 B13rcv v1 B2 B3 c2 B34rcv cb34 B34snd Additional level of hierarchy to model bus structure Model after Channel Partitioning PE1 PE2 B1 B1 Bus1 v1 cb13 B13snd c2 B13rcv v1 cb34 B2 B3 B34rcv B34snd Communication Model Example PE2 PE1 B1 B1 address[15:0] v1 B13snd data[31:0] B13rcv ready v1 ack B2 B3 B34rcv B34snd Communication Model Component & bus structure/architecture Top level of hierarchy Bus-functional component Specification model Architecture exploration Architecture model Communication synthesis models Communication model Timing-accurate bus protocols Behavioral component description Timed Estimated component delays Backend Implementation model Backend Clock-accurate implementation of PEs Hardware synthesis Specification model Architecture exploration Architecture model Communication synthesis Software synthesis Interface synthesis Communication model Backend Implementation model Hardware Synthesis Schedule operations into clock cycles Define clock boundaries in leaf behavior C code Create FSMD model from scheduled C code Clock boundaries PE2 B13rcv PE2_CLK v1 PE2_CLK B3 PE2_CLK B34snd Software Synthesis Implement behavior on processor instruction-set Code generation Compilation PE1 B1 B1 v1 Ff2 MOVE r0, r1 SHL ADD INC r3 r2, r3, r4 r2 PUSH CALL POP r1 Ff3 r0 B13snd B2 B34rcv Interface Synthesis Implement communication on components Hardware bus interface logic Software bus drivers S4 IBusSlave addr[15:0] data[31:0] ready ack IProtocolSlave S3 addr[15:0] data[31:0] ready ack PE2Bus PE2Protocol S2 PE1Protocol S1 IProtocolMaster PE1Bus S0 IBusMaster DRV Implementation Model Example Software processor Custom hardware PE1 PE2 OBJ Instruction Set Simulator (ISS) PORTA address[15:0] PORTB data[31:0] PORTC ready INTA ack S0 S1 S2 S3 S4 PE1_CLK PE2_CLK Implementation Model Cycle-accurate system description Specification model RTL description of hardware Behavioral/structural FSMD view Object code for processors Instruction-set co-simulation Clocked bus communication Bus interface timing based on PE clock Architecture exploration Architecture model Communication synthesis Communication model Backend Implementation model Support: 1. Modeling Engine Validation Compile Capture Specification model Simulate Arch. refinement Architecture model Simulate Comm. refinement Communication model Simulate Impl. refinement Implementation model Simulate Support: 2. Refinement Engine Refinement Validation Alg. selection Compile Browsing Capture Spec. optimization Specification model Simulate Allocation Beh. partitioning Arch. refinement Scheduling / RTOS Architecture model Simulate Protocol selection Channel partitioning Comm. refinement Arbitration Communication model Simulate Cycle scheduling Protocol scheduling Impl. refinement SW assembly Implementation model Simulate Support: 3. Exploration Engine Refinement Validation Alg. selection Compile Browsing Capture Spec. optimization Profiling weights Profile Profiling Specification model Profiling data Simulate Allocation Beh. partitioning Arch. refinement Scheduling / RTOS Comp. / IP models Estimate Estimation Architecture model Simulate Estimation results Protocol selection Channel partitioning Comm. refinement Arbitration Protocol models Estimate Estimation Communication model Simulate Estimation results Cycle scheduling Protocol scheduling Impl. refinement SW assembly Implementation model Simulate Support: 4. Synthesis Engine Refinement Validation Alg. selection Compile Browsing Capture Profile Spec. optimization Profiling weights Profiling Specification model Profiling data Allocation Comp. / IP attributes Synthesize decisions Arch. refinement Estimate Scheduling / RTOS Comp. / IP models Estimation Architecture model Estimation results Protocol selection Protocol attributes Verify Synthesize decisions Comm. refinement Estimate Arbitration Protocol models Estimation Communication model Estimation results Protocol scheduling Simulate Comm. synthesis Design Channel partitioning Cycle scheduling Verify Arch. synthesis Design Beh. partitioning Simulate RTL comp. Simulate Verify Impl. synthesis Design decisions Synthesize Impl. refinement SW assembly Simulate Implementation model Verify Tool example: SoC Environment: SCE from UCI Refinement Alg. selection http://www.ics.uci.edu/~cad/sce.html Validation Compile Browsing Capture Spec. optimization Profiling weights Profile Profiling Specification model Profiling data Simulate Allocation Beh. partitioning Arch. refinement Scheduling / RTOS Comp. / IP models Estimate Estimation Architecture model Simulate Estimation results Protocol selection Channel partitioning Comm. refinement Arbitration Protocol models Estimate Estimation Communication model Simulate Estimation results Cycle scheduling Protocol scheduling Impl. refinement SW assembly Implementation model Simulate Section Outline System LSI design From requirement to specification/functional descriptions From functional description to implementation Verification problems in the design methodology Verification techniques for high level designs Formal verification in SpecC based design methodology C based design description from specification (functional) level down to RTL Incremental refinement on the SpecC/C descriptions Equivalence checking between refinements Between sequential and parallel descriptions Between two same control structures Property checking on each refinement 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 ) : R e fin e m en t step F ig u re 1 . C -b a sed sy stem d esig n flo w To RTL d e sig n 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 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 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 Execution semantics in SpecC (cont.) Waitfor rule: 0 <= Tstart(a) < Tend(a) < 1 0 <= Tstart(w) < Tend(w) = 10 10 <= Tstart(b) < Tend(b) < 11 Time-interval formalism Simulation time Only waitfor increases simulation time Other statements execute in zero simulation time Example behavior B { void main(void) { a.main(); waitfor 10; b.main(); } }; a t=0 w t=1 b t = 10 t = 11 time 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 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 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 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 Comparison of two Descriptions with Same Control 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 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 ! Various SpecC Description Refinements Starting from pure functional ones, refine them into more HW/SW oriented ones 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 SpecC Description Refinements (cont.) From sequential ones to parallel ones void A1() { A1 void A1() { A1 } void B1() { B1 } void B1() { B1 } void C1() { } void main() { A1(); B1(); C1(); } } void C1() { C1 } void main() { par{ A1.main(); B1.main(); } C1.main(); } C1 SpecC Description Refinements (cont.) More refinement on each block of descriptions void A1() { void A1() { A1 B1 } void B1() { } void C1() { } void main() { par{ A1.main(); B1.main(); } C1.main(); } A2 B2 } void B1() { C1 } void C1() { } void main() { par{ A1.main(); B1.main(); } C1.main(); } C2 Equivalence Checking between Same Control Structures The two below are equivalence, if A and A1, B and B1, C and C1 are equivalent Equivalence checking between two very similar descriptions void A() { void A1() { A B } void B() { } void C() { } void main() { par{ A.main(); B.main(); } C.main(); } A1 B1 } void B1() { C } void C1() { } void main() { par{ A1.main(); B1.main(); } C1.main(); } C1 Equivalence Checking between Sequential and Parallel Structures For example, if A and B are totally independent computations, they are equivalent Extract control structure and check the final computation is equal void A() { A void A() { A } void B() { B } void B() { B } void C() { } void main() { A(); B(); C(); } } void C() { C C } void main() { par{ A.main(); B.main(); } C.main(); } Verification of Synchronization Synchronization Verification: 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 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 Synchronization in SpecC (cont.) 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 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; /*st1*/ /*st2*/ / * N e w * /} } St2 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 Section Outline System LSI design From requirement to specification/functional descriptions From functional description to implementation Verification problems in the design methodology Verification techniques for high level designs Basic Method: Symbolic Simulation * Further discussed in later Section Example of checking the behavioral consistency based on symbolic simulation 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 Symbolic Simulation Example This is an example of equivalence checking based on symbolic simulation 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 Symbolic Simulation Example This is an example of equivalence checking based on symbolic simulation 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 Symbolic Simulation Example This is an example of equivalence checking based on symbolic simulation 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 Symbolic Simulation Example This is an example of equivalence checking based on symbolic simulation 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’ Program Slicing for C/SpecC The codes to be symbolically simulated are extracted by program slicing This means only extracted codes will be simulated for verification Program slicing can extract the codes that can affect (be affected by) a variable Two kinds of slicing: backward slicing and forward slicing Based on C program slicer, program slicer for SpecC is developed based on VHDL program slicer [Shankar] IF the two descriptions have the same control structures, a little bit of extension is enough 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; 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; Efficient Equivalence Checking Comparison of two similar design descriptions Extract textual differences Dependency 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 Verification Flow (1) Description 1 Description 2 Pre-processes Identification of textual differences & ordering them Output the set of textual differences (d1, d2, d3, …) Identification of Textual Differences First, textual differences are identified by “diff” Then, they are sorted in the order of execution int v1, v2, out, opcode; v1 = 3; v2 = 5; if(opcode == 1) { out = v1 + v2; } Description 1 d1 d2 d3 int v1, v2, out, opcode; int reg1, reg2, alu; v1 = 3; v2 = 5; reg1 = v1; reg2 = v2; if(opcode == 1) { alu = reg1 + reg2; out = alu; } Description 2 Verification Flow (2) (d1, d2, d3, …) Is there any differences left? No Yes Verification terminates successfully Decision of target variables Backward slicing Consistency Symbolic simulation is proved Consistency is not proved Forward slicing An erroneous Symbolic simulation Consistency Consistency trace is reported is proved is not proved Verification Flow (2) (d1, d2, d3, …) Is there any differences left? No Yes Verification terminates successfully Decision of target variables Backward slicing Consistency Symbolic simulation is proved Consistency is not proved Forward slicing An erroneous Symbolic simulation Consistency Consistency trace is reported is proved is not proved Decision of Target Variables A variable v in a difference d is a target variable, When the variable v is defined in both descriptions, and assigned in the difference d int v1, v2, out, opcode; v1 = 3; v2 = 5; if(opcode == 1) { out = v1 + v2; } Description 1 d1 d2 d3 int v1, v2, out, opcode; int reg1, reg2, alu; v1 = 3; v2 = 5; reg1 = v1; reg2 = v2; if(opcode == 1) { alu = reg1 + reg2; out = alu; } Description 2 Case Split (d1, d2, d3, …) Is there any differences left? No Yes Verification terminates successfully Decision of target variables Backward slicing Consistency Symbolic simulation is proved Consistency is not proved Forward slicing An erroneous Symbolic simulation Consistency Consistency trace is reported is proved is not proved Symbolic Simulation/ Bounded Model Checking Reduced to Boolean SAT problems (OBDD or SAT) x0 … xn Expand k times … … ym y m Cycle 1 Cycle 2 0 y0 0 ym ym Mem. 1 1 k k x0 … xn Cycle k … … Convert Property (reset && X(reset) && XX(reset) &&c) ⇒（XX(out)=in) Checker Circuit k y0 … y0 … y 0 1 1 x0 … xn … y0 0 0 x0 … xn k ym Is there an input pattern generating “one” at the output Approaches for Verifying High-level Designs Propositional logic ⇒ First-order logic, ... e.g. Abstraction of arithmetic op’s by symbols(<, +, *,...) Approaches SAT for Logic of uninterpreted functions with equality Equivalence checking without considering meaning of functions Hybrid SAT SAT for Boolean formulas with linear constraints Tool SVC(Stanford Validity Checker) tool – Boolean logic, linear programming, uninterpreted function,. arrays.. Logic of Uninterpreted Functions with Equality Arithmetic operations are handled as symbols x y 1 f 0 Y Y:= if c then x else f(x,y) c Equivalence checking :“Design 1 = Design 2 ?” There is a decision procedure. Can be checked by SVC tool. Abstraction * Further discussed in later Section Like to handle very large descriptions Reduction of the number of states is a must A set of behaviors of the abstracted design Merging multiple states into a single state Abstracted designs contain more behaviors than the originals False-negative results possible, but never falsepositive A set of behaviors of the original design Abstraction If some property holds, then the original design is correct Otherwise, the design is incorrect, or the abstraction is too strong Refinement is necessary to prove the property Behaviors allowed by a property “The property holds”. incorrect Indistinguishable from the verification result for the abstracted design abstraction is too strong “The property does not hold”. Model Checking of C programs Basic techniques abstraction, model checking, and error analysis + refinement Abstracti on Ｃ Program Properties Modified Program Abstracted Boolean Program Model New constraints Checking Error analysis Microsoft’s SLAM tool Bugs Counterexample Correct Tutorial Outline Introduction High level design flow and verification issues Theorem proving and Decision procedures Formal verification techniques for FSM models Semi-formal verification techniques Simulation based verification techniques Conclusions and future directions Theorem Proving & Decision Procedures MASAHIRO FUJITA University of Tokyo Tokyo, Japan [email protected] 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 Symbolic Logic (cont.) More precisely, a formal symbolic logic consists of A notation (symbols and syntax) A set of axioms (facts) A set of inference rules (deduction sheme) 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 Key Features of a Theory Expressiveness Completeness what kind of statements can be written in the theory all valid formulas are provable Decidability there exists an algorithm to deduce the truth of any formula in the theory Comparison of Types of Logic Propositional First Order Logic Least expressive, decidable, complete More expressive, decidable, not complete Higher Order Logic Most expressive, not decidable, not complete 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 , 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 ) 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 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 it Why is Validity Checking Interesting? 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 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! Theorem Prover Given Advantages a theory, a proof system, and a formula whose validity must be proved a system that allows a user to carry out the proof is broadly classified as a theorem prover Expressive, high abstraction, powerful reasoning, Disadvantages Low automation, expert knowledge required 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) Well-known Theorem Provers Higher order: ALF, Alfa, Coq, HOL, PVS Logical Frameworks: Isabelle, LF, Twelf Inductive: ACL2, Inka Automated: Gandalf, TPS, Otter, Setheo, SPASS EQP, Maude, SVC Provers used in Verification – HOL, PVS, ACL2, SVC 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 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 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] 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) Example (cont.) (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 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 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! How are Multiple Decision Procedures Combined? Shostak’s method 1984 [Shostak ‘84] Future corrections & clarifications [Cyrluk et al. ‘96] [Ruess and Shankar ‘01] Used in several automated deduction systems PVS, STeP, SVC Shostak’s Method - Canonizer Two main components Canonizer Solver The canonizer rewrites terms into a unique form = a = b canon (a ) = canon (b ) Examples of canonizer for linear arithmetic canon (a + a ) = 2a Unique ordering of variables canon ( b + a ) = a + b Shostak’s Method – Solved form Solved form – A set of equations is said to be in solved form if the variable on the LHS of each equation appears in the set only once a=x+c b = 2x + y Not in solved form: a = b + c x=a+z In solved form: R denotes replacement of each LHS variable occuring in any RHS with its equation R (a + x) = 2b + 2c + z Shostak’s Method - Solver The solver transforms an equation into a corresponding set of equations in solved form If = a b , then solve (a = b ) = { false } Otherwise: solve (a = b ) = a set of equations in solved form = (a = b x. ) – x is a set of fresh variables appearing in , but not in a or b. Example: solver for real linear arithmetic solve (x - y - z = 0 ) = { x = y + z } solve (x + 1 = x - 1 ) = { false } The Simplified Shostak Algorithm Simplified algorithm due to Clark Barrett, NYU Given a set of equations E and disequations D Step 1: Use the solver to convert E into an equisatisfiable set of equations E’ in solved form Step 2: Use this set of equations together with the canonizer to check if any disequality is violated For each a b D Check if canon (E’ (a ) ) = canon (E’ (b ) ) Combining Theories in Shostak Two Shostak theories 1 and 2 can be combined under certain restrictions to form a new Shostak theory = 2 2 Solvers from two theories can be combined Treating terms from other theory as variables Repeatedly apply solvers from each theory until resulting set of equations is in solved form Issue of applying appropriate constraints to the variables from other theories is tricky Summing Up A very powerful proof methodology Proof is not fully automatic can describe and prove properties on the most wide array of systems and abstractions requires manual intervention requires expertise and understanding of modeling concepts some proofs may not terminate Industrial use not yet very popular some dedicated specialized use in Intel need to make procedure more automated for practical use Tutorial Outline Introduction Design flow and verification issues Theorem proving and Decision procedures Formal verification techniques for FSM models model checking and formal engines model checking in practice equivalence checking Semi-formal verification techniques Simulation based verification techniques Conclusions and future directions Model Checking and Formal Engines MUKUL PRASAD Fujitsu Labs. of America Sunnyvale, California Section Outline Introduction to Model Checking Engines for model checking SAT Solvers Binary Decision Diagrams (BDDs) Symbolic Model Checking with BDDs Model Checking using SAT 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 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 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 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 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 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 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) 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 CTL Model Checking Example 1 P Compute EFp EF p = p EX(p) EX(EX(p)) . . . STEP 1 STEP 2 P STEP 3 Fixed Point !! P P Computation terminates EF p Holds in all green states Computation involves backward breadth first traversal Calculation of Strongly Connected Subgraphs (cycles) 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 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 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 Section Outline Introduction to Model Checking Engines for model checking SAT Solvers Binary Decision Diagrams (BDDs) Symbolic Model Checking with BDDs Model Checking using SAT 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 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 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 ) 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 Conflict Driven Search Pruning (GRASP) Silva & Sakallah ‘95 x1 Non-chronological backtracking Conflict-clause recording x2 2 xj SAT xk-1 xk 1 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) Example Contd: 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(3((xx12xx93 xx104) x11) Example Contd…. 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 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. 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 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 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 Section Outline Introduction to Model Checking Engines for model checking SAT Solvers Binary Decision Diagrams (BDDs) Symbolic Model Checking with BDDs Model Checking using SAT 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 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 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 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 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 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. 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 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) 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 Section Outline Introduction to Model Checking Engines for model checking SAT Solvers Binary Decision Diagrams (BDDs) Symbolic Model Checking with BDDs Model Checking using SAT 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 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) 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) 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 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 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 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 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 Breadth-First Reachability Analysis 00 01 00 00 00 10 R R11 R R00 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 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 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 … Section Outline Introduction to Model Checking Engines for model checking SAT Solvers Binary Decision Diagrams (BDDs) Symbolic Model Checking with BDDs Model Checking using SAT Solving Circuit Problems as SAT a b h f c d g i e Input Vector Assignment ? Primary Output ‘i’ to 1 ? 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 ) 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 ) 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 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 SAT-Based Inductive Reasoning UNSAT ‘1’ I0 Induction Step Base Case P P + AG P is TRUE UNSAT ‘1’ ‘1’ CLk+1 Simple Induction P ‘1’ SAT-Based Inductive Reasoning P I0 Induction Step Base Case P CL1 P CL2 CLk ‘1’ P ‘1’ P P CL1 ‘1’ P ‘1’ CLk CLk+1 Induction with depth ‘k’ (Sheeran et al, Bjesse et al FMCAD 2000) P ‘1’ 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 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! Summary: 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 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 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 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 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 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) 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 Tutorial Outline Introduction Design flow and verification issues Theorem proving and Decision procedures Formal verification techniques for FSM models model checking and formal engines model checking in practice equivalence checking Semi-formal verification techniques Simulation based verification techniques Conclusions and future directions Model Checking in Practice INDRADEEP GHOSH Fujitsu Labs. of America Sunnyvale, California Section Outline Enhancing Formal Verification Capacity Abstraction-refinement Assume guarantee/Compositional Reasoning Approximation Symmetry reduction Partial Order Reduction Formal Verification: Case Study Industrial and Research Tool Offerings 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. 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 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? 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 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 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’’ 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 Assume-Guarantee Reasoning P’ Q’ P’ P Q’ P + Q’ P’ Q Q Used for: Compositional reasoning In a refinement checking setting Ref: [Stark] [Chandy-Misra] [AbadiLamport][Alur-Henzinger][McMillan] AG Reasoning: Example •true b’ := true P’ a’ := true Q’ X X •true a’ b’ := true •a’ b’ := false b’ a’ := true •b’ a’ := false P Q Assume all variables are initialized to true AG Reasoning: Example •true b’ := true P’ •true a’ := true Q’ a’ b’ := true •a’ b’ := false •true a’ := true P Q’ •true b’ := true b’ a’ := true •b’ a’ := false P’ Assume all variables are initialized to true Q 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) ] 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 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 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 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 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 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 Case Study: VGI VGI = “Video-Graphics-Image” Designed by Infopad group at Berkeley Purpose: web-based image processing Designed using VHDL (control) Schematics (Data path) Source: T. Henzinger, X. Liu, S. Qadeer and S. Rajamani, “Formal Specification and Verification of a Dataflow Processor Array,” ICCAD 1999 VGI Architecture 16 clusters with 6 processors in each - 4 compute, 1 memory, 1 I/O ~30K logic gates per processor Pipelined compute processors Low latency data transfer between processors - complex control VGI Architecture pipeline pipeline pipeline pipeline Complex handshake pipeline FIFO buffer ISA ISA ISA ISA ISA Verification Different time scales Implementation two-phase clock level-sensitive latches activity on both HI and LO phases of clk Specification no clk signal Sample Operator S I I’ = Sample I at Runs of I’ = Runs of I sampled at instances where holds Sample Operator ISA ISA ISA ISA ISA pipeline pipeline pipeline pipeline pipeline clk Difficulty - Verification Size of the VGI chip ~800 latches in each compute processor 64 compute processors Need “divide and conquer” assume guarantee reasoning compositional reasoning refinement checking Compositional Reasoning Q’ P’ P TP P’ Q’ TP TQ Q TQ P P’ P Q Q’ Q Mocha Reactive Modules - language for describing designs Assume-guarantee refinement checking “Mocha: modularity in model checking,” Alur, Henzinger, Mang, Qadeer, Rajamani, Tasiran, CAV 1998 Network of Processors to Single Processor pipeline ISA clk pipeline pipeline ISA clk ISA pipeline clk clk pipeline clk ISA ISA Single Processor pipeline ISA TP clk Single processor still has ~800 latches Need “divide-and-conquer” again Refinement Map Input from upstream processor ISA REGFILE FIFO buffer Input from upstream processor REGFILE ALU Spec OP GEN P I P E ALU Gate Level Comm Stage clk Decompose Proof Input from upstream processor ISA REGFILE OP GEN Input from upstream processor REGFILE ALU Spec ALU P I P E FIFO buffer AbsAluOut ALU Gate Level Comm Stage clk Abstraction and Compositional Reasoning aluOutSpec stall aluOutImpl’ = aluOutImpl stall aluOutImpl’ = aluOutSpec much smaller than stall AbsAluOut REGFILE aluOutImpl P I P E ALU Gate Level Property: Communication Control FIFO buffer AbsAluOut Comm Stage TP clk Refinement Checking Input from upstream processor ISA REGFILE ALU Spec OP GEN AbsOps FIFO buffer AbsAluOut Input from upstream processor REGFILE P I P E ALU Gate Level Comm Stage clk Results Circular assume-guarantee AbsOps used to verify AbsAluOut AbsAluOut used to verify AbsOps All lemmas (except one) checked by Mocha in a few minutes 3 bugs in communication control found and fixed Abstraction modules crucial - designer insight needed 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) Industrial Model Checkers FormalCheck (Cadence) COSPAN (from Bell Labs) under the hood Support for arbitrary precision arithmetic Automatic bus-contention, multi-driver violation, tri-state 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 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 Tutorial Outline Introduction High level design flow and verification issues Theorem proving and Decision procedures Formal verification techniques for FSM models model checking and formal engines model checking in practice equivalence checking Semi-formal verification techniques Simulation based verification techniques Conclusions and future directions Equivalence Checking MUKUL PRASAD Fujitsu Labs. of America Sunnyvale, California 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 Formal Equivalence Checking Equivalence checking can be applied at or across various levels System Level Gate Level Device Level RTL 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 CEC CEC ECO 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 = 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 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’) 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 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 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) 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 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 System-level design Property & Model Checking Manual effort RTL Gate-level design Equivalence Checking System-level Synthesis System-level design Manual effort RTL Gate-level design Automatic Synthesis 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 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 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 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 Tutorial Outline Introduction High level design flow and verification issues Theorem proving and Decision procedures Formal verification techniques for FSM models Semi-formal verification techniques Simulation based verification techniques Conclusions and future directions Semi-Formal Verification Techniques MUKUL PRASAD Fujitsu Labs. of America Sunnyvale, California The need for 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 Section Outline Symbolic Simulation Symbolic Trajectory evaluation (STE) SAT-based Bounded Model Checking Sequential ATPG-based model checking Guided Search Smart Simulation 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 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 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 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 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. 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) 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] 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 Section Outline Symbolic Simulation Symbolic Trajectory evaluation (STE) SAT-based Bounded Model Checking Sequential ATPG-based model checking Guided Search Smart Simulation 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 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 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 Ref: Prof. Randal Bryant, 2002 T=0 Dout T=1 Dout T=2 Dout T=3 Dout T=4 Dout NNNN Dout = a Check STE: Pros, Cons & Practical Use 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 Section Outline Symbolic Simulation Symbolic Trajectory evaluation (STE) SAT-based Bounded Model Checking Sequential ATPG-based model checking Guided Search Smart Simulation 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) 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 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 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: SAT-BMC 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 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 Section Outline Symbolic Simulation Symbolic Trajectory evaluation (STE) SAT-based Bounded Model Checking Sequential ATPG-based model checking Guided Search Smart Simulation 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 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 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 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) Section Outline Symbolic Simulation Symbolic Trajectory evaluation (STE) SAT-based Bounded Model Checking Sequential ATPG-based model checking Guided Search (academic) Smart Simulation (mixed engine) SIVA (academic) Coverage-driven test generation: Magellan (industrial) Test amplification: 0-in search (industrial) 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 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 Section Outline Symbolic Simulation Symbolic Trajectory evaluation (STE) SAT-based Bounded Model Checking Sequential ATPG-based model checking Guided Search (academic) Smart Simulation (mixed engine) SIVA (academic) Coverage-driven test generation: Magellan (industrial) Test amplification: 0-in search (industrial) 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 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 Smart Simulation II: Magellan [Ho et al, ICCAD 2000 (Synopsys)] Approach: 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 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) 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 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 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 Tutorial Outline Introduction High level design flow and verification issues Theorem proving and Decision procedures Formal verification techniques for FSM Semi-formal verification techniques Simulation based verification techniques Conclusions and future directions Simulation Based Verification INDRADEEP GHOSH Fujitsu Labs. of America Sunnyvale, California Section Outline Introduction Making simulation effective why simulation types of simulation Coverage analysis Test bench automation RTL ATPG SOC verification challenges Case study Verification Using Simulation Test Cases / Features Test Sequences Implementation to be Verified Spec Expected Responses Output Responses =? Simulation and Abstraction Levels Specification level simulation Behavioral simulation possible to simulate just C/C++/SpecC/SystemC program checking with spec requires cutting out relevant portions of behavior RTL simulation particular behavior or properties can be captured in UML like languages and simulated. e.g. protocols most widely used in industry many commercial tools checking with behavior requires time checkpointing Logic simulation fairly straight forward and easy to check with RTL detailed timing simulation comes into picture Advantages/Disadvantages Advantages simple concept scales well with design size compared to formal or semiformal methods most popular strategy in industry Disadvantages simulation semantics may not mimic hardware cannot be exhaustive cannot prove correctness writing extensive test benches is tedious do not know when to stop still can be resource intensive and slow Static RTL checks : Linting Design rule based Fix non-synthesizeable code force uniform and correct style among all designers Verilog syntax can compile but create problems in synthesis and simulation no point simulating stuff that cannot be synthesized Synthesis results vary based on coding styles coding, style, documentation, naming, custom comparing different length variables if(a[2:0] == b[1:0] ) using blocking/non-blocking assignments at wrong places latch interfaces etc. Standard set of rules are based on Reuse Methodology Manual (RMM) (reference page 2) Linting CAD Tools LEDA from Synopsys nLint from Novas Software integrated with the Debussy debugging system HDLLint from Veritools VN-check from TransEDA Surelint from Verisity Spyglass from Atrenta Tackling Simulation Drawbacks Simulation semantics may not mimic hardware Cannot be exhaustive cannot prove correctness Writing extensive test benches is tedious Do not know when to stop Still can be resource intensive and slow RTL Simulation Semantics Ddelay 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 0 a D=2 1 c Events: •Input: b(1)=1 •Output: none 1 0 b 0 1 Event: change in logic value, at a certain instant of time (V,T) 1 0 a D=2 1 b 0 1 c 1 0 3 Events: •Input: b(1)=1 •Output: c(3)=0 Event-driven Simulation Uses a timewheel to manage the relationship between components Timewheel = list of all events not processed yet, sorted in time (complete ordering) When event is generated, it is put in the appropriate point in the timewheel to ensure causality Event-driven Simulation 1 1 0 0 a c D=2 1 1 1 e D=1 b 0 0 3 4 6 1 d 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 Cycle-based Simulation Compute steady-state response of the circuit at each clock cycle at each boundary node L a t c h e s Internal Node L a t c h e s Cycle-based vs Event-driven Cycle-based: Only boundary nodes No delay information Event-driven: Each internal node Need scheduling and functions may be evaluated multiple times At RTL if timing information is unknown Cycle-based is more appropriate Cycle-based is 10x-100x faster than event-driven (and less memory usage) Cycle-based does not detect glitches and setup/hold time violations, while event-driven does 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 Tackling Simulation Drawbacks Simulation semantics may not mimic hardware Cannot be exhaustive cannot prove correctness Writing extensive test benches is tedious Do not know when to stop Still can be resource intensive and slow Coverage Analysis Quantitative measure of simulation effectiveness Determines if the simulation test bench is exercising the design effectively Concepts borrowed from software testing Various metrics available Coverage Analysis Tool HDL Design Display in GUI Gather Coverage Data Instrumented Design Test Bench RTL Simulation Common Coverage Metrics * Statement Coverage - see if all statements are covered by testbench Example if ( a > 0) e = c * d; else f = c + d; Statement Coverage: 66.7% * Branch Coverage - see if both sides are taken in all possible branches * Toggle Coverage - see if each variable bit value has toggled if (b > 0) e = e + 1; if (b <= 0) did not occur Branch Coverage: 50% Verification engineers should aim for 100% statement, branch and toggle coverage Condition Coverage * See if all possible conditions in an expression are taken Example: if ((a < 0) && (b > 3) && (c = 5)) { ..... } * All eight possibilities are to be present for 100% condition coverage - e.g. {(a>=0), (b<=3), (c != 5)} ; {(a >=0), (b<=3), (c=5)} etc. * All don’t care possibilities may not be feasible - use only care combinations Focussed Expression Coverage * Only try possibilities that make each clause important Thus try {(true, true, true); (false, true, true); (true, false, true); (true, true, false)} If some combinations are still not possible then expression in redundant! Verification engineers should aim for > 95% FEC Path Coverage State <= S State <= S no Done == ‘1’ yes no Done == ‘1’ yes State = Q no Isb == ‘1’ yes State = R State <= S no Done == ‘1’ yes State = Q no Isb == ‘1’ yes State = R State <= S no Done == ‘1’ yes State = Q no Isb == ‘1’ yes State = Q no Isb == ‘1’ State = R * Path Coverage: What % of paths are covered? - exponential number of paths - difficult to do the bookkeeping - impossible to get good coverage - false paths may hinder coverage - supported to a limited extent in most tools Mostly ignored by verification engineerers yes State = R FSM Coverage If there are FSM descriptions in the machine see that all states of all FSMs are visited all possible state transitions in every FSM is taken FSMs need to be described in particular manner automatic extraction fails mostly if other coverage metrics are good, this is already taken care of else this should at least be 100% A C B D Cover - 4 states - 7 transitions Coverage Analysis CAD Tools Work in conjunction with RTL simulators Synopsys Covermeter Verisity Surecov Verilog coverage analysis tool integrated with Specman Elite tool TransEDA Verification Navigator Verilog coverage integrated with VCS simulator supports both VHDL and Verilog works with all major simulators Cadence Affirma works with their NCSim RTL simulators (VHDL and Verilog) Coverage Analysis - Pros & Cons Pros: provides some quantitative analysis of verification effort increases confidence level in simulation based verification points out untested functionality in the design gives some type of closure to verification effort Cons: cannot model many types of errors high confidence level due to good coverage numbers can give false sense of security observability of error is ignored still covering implementation, not specification Importance of Observability Example: input a, b, c, d; f = 1; e = 0; if ( a > 0) error e = c * d; else error f = c + d; if (b > 0) print(e); else print(f); simulate: a = 1, b = -1; a = 0, b = 1; 100% statement and branch coverage, but no errors detected Observability Enhanced Code Coverage Analysis Does vector set propagate an erroneous value on variable a to an observable output? a = 1; erroneous value c = 4 - a; printf(“%d”, c); • • • • This metric known as OCCOM is based on Fallah et.al’s work at DAC 98. Possibility of an error represented by tagging variable in left-hand side of an assignment or an expression by +D or -D . A Tag at a location/variable represents the possibility that an incorrect value is present at the location/variable Goal: see if Tag injected at a location is propagated to output by test set Tag Propagation Positive, Negative and Unsigned tag Single error assumption A 1; D D C 4 A; printf( "C %d",C D D ); Error Model Errors in design modeled as errors in assignment statements and expression clauses Method confirms that a design error is detected if the vector set activates and propagates the required tag on the location of the error only positive and negative errors tackled to reduce complexity sometimes unkown tags (D') generated error may propagate even if tag does not tag propagation is conservative if +D and -D collide then usually (D') tag is killed after sometime but error can still be observable Error model is sufficient but not necessary for error detection Research Results * How good is the tag coverage metric for tracking bugs? Intelligent Vectors Bug Coverage Tag Coverage Random Vectors Bug Coverage Tag Coverage - 30 typical bugs were introduced into a Fujitsu RTL circuit - functional simulation done using intelligent vectors that target tag coverage and random vectors Conclusion: Tag coverage closely tracks bug coverage but is slightly pessimistic. Specification Coverage using CWL CWL (Component Wrapper Language) Jointly developed by Hitachi and Fujitsu Hierarchical description aimed at abstraction level conversion Support for split transactions Support for interface specific hardware Hierarchical Description: Base clk rst en ad[9:0] a wait dt[7:0] d I signalset all = N : I : Q(a): W : S(d): endsignalset N Q(a) W W S(d) N {clk,rst, en, ad,wait,dt}; { R, 1, 1, x, 1, x}; { R, 0, x, x, 1, x}; { R, 1, 0, a, 1, x}; { R, 1, 1, x, 0, x}; { R, 1, 1, x, 1, d}; Hierarchical Description: Transaction clk rst en ad[9:0] a wait dt[7:0] d I N Q(a) reset nop W W read(a,d) S(d) N nop sentence word; nop : N ; reset : I ; read(a,d) : Q(a) W* S(d) ; endword sentence; reset [ nop | read ]+ ; endsentence Specification Coverage using Transitions Once specification sentence protocol generated create complete regular expression create FSM that recognizes regular expression convert FSM to Verilog monitor during simulation see that all transitions in FSM are covered Then protocol specification completely verified ensures coverage of all possible legal signal combinations not just the interesting scenarios Tackling Simulation Drawbacks Simulation semantics may not mimic hardware Cannot be exhaustive cannot prove correctness Writing extensive test benches is tedious Do not know when to stop Still can be resource intensive and slow Test Bench Automation Today’s ASICs and SOCs multi million gates, extremely complex 1000s of inputs and outputs Writing meaningful input patterns in 1s and 0s impossible Impossible to verify output pattern in 1s and 0s Need specialized language and framework to write good, complex and extensive test bench Example: Ethernet frame header, addresses, payload (variable length), error correction code (72 bytes to 10000 bytes) Write function Create_frame(parameters) creates correct frame in terms of patterns of 1s and 0s Key Features Constrained input sequence generation write input sequence in high level construct may use structures, fields etc. Automatic Output Checker generation put constraints on input fields tool converts these to signal level test sequence tool can also solve for constraints on some inputs tool can iterate on several parameters to generate numerous test sequences automatically create a set of rules to check expected output again high level structures can be used e.g. if packet sent to port A from port B earlier that port C, they are output in sequence in port A [check_packet( )] Concise property specification languages Support for constrained random test generation Bus Functional Models These HDL models are used to convert higher level transaction behavior to signal level inputs test bench can be written and analyzed in high level once done prevents detailed signal level stimulus more robust and less error prone, hides details Example: memory write() read() address[7:0] Bus Functional Model data[7:0 rw ale Pre-defined vald protocol with timing Property Specification Languages Is needed for unambiguous modeling of Spec Should be formal yet easy to read/understand support for real life properties - Boolean, temporal etc support for modeling design input behavior PSL Sugar from IBM standardized by Accellera it has 4 layers of formalism Boolean layer describes states of design Temporal layer describes behavior of design over time Modeling layer model auxiliary state variables and state machines and input environment Verification layer directives to verification tool assume/assert/cover etc. Writing Properties in Sugar Example {true[*];req;ack} |=> {start;busy[*];end} true req ack start busy end if then if then Temporal Operators never (read_enable and write_enable) always (req -> next ack) when request is asserted ack must be asserted next cycle using forall operator always (req && data_in == ‘b000 -> next data_out == ‘b000) always (req && data_in == ‘b001 -> next data_out == ‘b001) .. can be written as forall i in 0..7 always (req && data_in == i -> next data_out == i) Assertion Checking Example assert if request signal is high for 5 cycles without the acknowledge signal going high, then system should assert busy flag Sugar property vunit check_busy_flag { assert { [*], {request & !acknowledge} [*5] } |-> {busy flag} } If this checker is written in Verilog Automatic translators exist now 50 lines of HDL code e.g. FOCS from IBM Verification efficiency is increased a lot CAD Tools for Test Bench Automation & Assertion Checking Verisity Specman Elite Cadence Testbuilder uses its own OVL (Open Vera Language) (now open) Avery VCK uses C++ classes to automate tests Synopsys Vera uses proprietary E language (free licenses available) uses VLE (Verilog language enhancements) As Accellera Sugar has become industry standard all tools are now supporting it Automatic Test Pattern Generation at RTL Generating good RTL simulation test benches is hard and tedious still manual process test bench automation helps somewhat but still need to write tests in high-level test language like Sugar etc. may not exercise design completely (bugs may remain) Alternative: attempt to generate RTL test benches automatically by analyzing the RTL design (ATPG) only HDL design is needed approach is bottom up as opposed to top down may not be suitable in all cases Requires RTL error models currently stuck-at fault model and OCCOM is used experimentally determined they correlate well with bugs Application Scenarios Test Bench Test Generation Algorithm/Tool Executable Specification RTL Design Under Test SCENARIO 1 near 100% coverage Test Responses =? Test Bench Test Generation Algorithm/Tool Optimized RTL model Golden RTL Model near 100% coverage SCENARIO 2 * Formal RTL equivalence checking fails as circuits are too dissimilar Test Responses Test Responses =? Test Responses Data Structure Used Represent RTL netlist as an Assignment Decision Diagram (ADD) Previously proposed for highlevel synthesis by Chaiyakul et.al. (DAC 93) Case state is when st3 => if (a < 7) r = p + q; else r = p - q; Example a 7 = < Assignment Condition st3 state & q - + v c ! c & • p Assignment Value v r Advantages – Represents a structural view suitable for ATPG Assignment Target Algorithm Overview Convert HDL file into a series of ADDs each process converted to an ADD ADDs connected together by read and write nodes Infer RTL structural components from ADDs Each inferred component is fed its logic-level stuck-at test PI PI 2-to-1 mux : 4 vectors register / latch : 4 / 2 vectors logic gate : well known test set logic memories : checker board test < arithmetic module : precomputed test an universal test set preferable random logic / test set unavailable PO excite HDL code and observe effect at system primary output Modeling RTL Values Cg C0 C1 Ca1 : : : : control an n-bit bus to any of 2n value control a variable to the 0 value (00..00) control a variable to the 1 value (00..01) control a variable to the all ones vector (11..11) CA1 of 1 bit variable is C1 Cq Cs Cz Cp O O’ : : : : : control a variable to any constant (5, 10, etc.) control a state variable to a particular state value (St1) control to high-impedance state (zz..zzz) control to a particular range of integers (16-32) observe an any fault on multi-bit variable or an 1/0 fault on a single-bit variable : observe a 0/1 fault only for a single-bit variable * These constants are sufficient to propagate test vectors across all RTL modules Algorithm Cg Cg backtrack To PIs C1 Cg C1 Cg + To PIs Cg Cq C1 O * < O C1 O To POs Results & Ongoing Research This is in technology transfer phase Has been applied on industrial examples Prototype shows huge speed up over logic ATPG 2 to 3 orders of magnitude reduction in CPU time Test sets automatically give close to 100% line, branch and condition coverage Can be used as initial filter before manual test benches or formal verification Disadvantages: application scenarios limited still block level tool, about 20,000-50,000 line flat HDL search is NP complete and uses branch and bound Ongoing research speed up engine using circuit SAT techniques modify engine for RTL property checking Tackling Simulation Drawbacks Simulation semantics may not mimic hardware Cannot be exhaustive cannot prove correctness Writing extensive test benches is tedious Do not know when to stop Still can be resource intensive and slow Stopping Criteria Coverage based Bug rate based when rate of new bugs detected fallen below particular level, e.g. - 2 per week Random simulation based e.g. >99.5% line coverage, >99% branch coverage, >90% condition coverage e.g. random simulation ran for 3 days without problem Some weighted average of all the above Use case emulation e.g. video processor watch output of emulator in real time on a TV screen Deadline based need to tape out chip, hence stop simulation !! Tackling Simulation Drawbacks Simulation semantics may not mimic hardware Cannot be exhaustive cannot prove correctness Writing extensive test benches is tedious Do not know when to stop Still can be resource intensive and slow Tackling the Time Complexity Still huge amounts of time and resources required to simulate multi-million gate designs but only simulation scales to large designs Alternatives Hardware emulation/acceleration Core based design of SOC use preverified modules and just verify interface some peculiar problems arise Correct by construction design Emulation Compile RTL design into a number of FPGAs and PLDs Directly simulate test bench on the hardware using a computer interface Capture output responses in a memory buffer and display using the computer Advantages 10X to 100X faster than software simulation simulation semantics problems are lower Disadvantages systems are expensive cumbersome to set up debugging support weaker than software debuggers Tackling the Time Complexity Still huge amounts of time and resources required to simulate multi-million gate designs but only simulation scales to large designs Alternatives Hardware emulation/acceleration Core based design of SOC use preverified modules and just verify interface some peculiar problems arise Correct by construction design SOC Verification Issues What is new in SOC verification? SOCs - large designs, small teams Why is SOC verification more challenging? closer to computer systems than ASICs but built rapidly with small design teams using cores Verification team cannot get deep understanding of target design Not enough resources to develop verification tools specific to design Verification teams must rely on existing tools and technology generic knowledge of domain with small adaptations More Challenges Most SOCs contain a processor Processors can be used to stimulate rest of the system but.. How to treat system software big and complex and programmable ignoring means not testing entire system leaving it in means more difficult to use processor to test other components HW/SW co-simulation a major issue simulating processor will slow down RTL simulation hardware and software operate at different rates modeling solutions are required e.g. Instruction Set Architecture Interface issues how to check that the cores are talking correctly with each other e.g. protocol verification Solution - Raise Abstraction Level Focus at level where design complexity lies Advantages match shift in design paradigm improved productivity due to reasoning at right level early start of verification effort start on high-level models of design but use same methodology for lower level New building blocks signals, packets, complex transactions cores instead of registers, FSMs etc. New Paradigms Transaction based verification and coverage System level test generators New applications of formal verification protocol verification E.g. - Product by Jasper Design Automation High Level Checking Techniques Behavioral rules can be checked to test aspects of behavior e.g. : transaction ordering, coherence Need means to describe rules and check them e.g. : when write transaction begins all previous read transactions have finished look for all read transactions and check their status check order with respect to write transaction Data flow is a good source of behavioral rules record the history of each transaction analyze the the behavior of system according to the flow of transactions and their interaction Using System Level Test Generators Goal: Systematic verification of IP (core) interaction to verify global functional behavior Generates tests that cover the interaction among IPs Tool Esterel Studio assumes each IP has been individually verified based on hierarchical concurrent finite state machines (HFSMs) Four step process model system as HFSM (need lot of abstraction) create symbolic tests transform tests to concrete tests simulate the concrete tests Creating Symbolic Tests Use BDD based traversal engine to compute all the possible paths to the test_completed state in the global test scheduling FSM each path is associated with an input sequence Transform input sequences to output sequences using the Esterel Studio simulator The resulting sequences are commands to and by the IPs that create the requested scenario config_data_channel_1 req_dst_wav req_src write_frame Tackling the Time Complexity Still huge amounts of time and resources required to simulate multi-million gate designs but only simulation scales to large designs Alternatives Hardware emulation Core based design of SOC use preverified modules and just verify interface some peculiar problems arise Correct by construction design Correct By Construction Translation from higher to lower level description Easier said than done automatic and correct no need to verify lower level CAD tools will contain bugs (software program) requires years of use before some degree of confidence Example Synopsys Design Compiler RTL to gate level generator after 12 years of use and numerous bug fixes most designers trust its output in terms of functionality timing still not completely robust Platform based design another design flow with this philosophy Case Study: Fujitsu 10GB Ethernet Switch Fujitsu 10 Gb Ethernet Switch Chip Layer 2 Switch 12 I/O XAUI ports (IEEE 802.3ae) MAC frame relay and spanning tree (802.1D) Virtual LAN (802.1Q) Design Complexity 6.3 million gates & 900 KBytes SRAM approximately 70 million transistors process 0.11m Our mission is to verify the Switch Chip Processor (BPDU, GMRP, GVRP, Management) Switch Chip (Filtering, Relay) Verification Framework Test Program-1 (.cc) Test Program-2 (.cc) APIs Frame Generator (.cc) XAUI BFM (.v) MAC XAUI XAUI Driver / Receiver (.cc) XGMII BFM (.v) Switch Chip (DUV) XGMII Driver / Receiver (.cc) Reference Model (.cc) Interrupt Handler / Device Driver (.cc) Processor BFM (.v) EEPROM BFM (.v) Verilog-HDL Driver (.cc) TestBuilder Black Box Verification Just see if design conforms to Spec. Spec. - IEEE 802.3ae, 802.1D, 802.1Q over 1000 pages of English text IEEE Specifications conformance test Micro-architecture independent PICS (Protocol Implementation Conformance Statement) somebody painfully went through the text to extract about 200 points to test (this is well known) extracted 39 test cases (one test case can cover multiple tests) Example: frame address is learnt by switch send frame with source address A from port 2 send frame with destination address A from port 3 check that second frame comes out at port 2 White Box Verification Test the special features of the chip not mentioned in IEEE Spec implementation dependent verification engineer need to understand design functionality Micro-architecture dependent test cases E.g. 1. memory corruption test memory protected by error correcting code intentionally corrupt memory during frame transmission see that error correction is occurring correctly E.g. 2. mode registers: extracted 88 test cases Total dedicated test cases - 200 simulation cycles - 25.9 million IP Verification Design used one 3rd party soft IP IP came with own testbench Manually translated IP test bench to system test bench for regression tests verified line coverage of IP > 99.5% even within system 5 bugs were found in the IP Random Simulation Random test Arbitrary random frames generation Reference model for automatic verification this is tricky as bugs may be in reference model may be tedious to write Best used to hit assertions put in by designer the random seeds needs to be stored for each test case so that failed test may be reproduced Random test #cycles: 1B (2M frames) Coverage Analysis At this point line coverage > 95% branch coverage > 90% If not rethink verification strategy Otherwise find uncovered code ask designer what he intended to do in that piece of code (broad idea only) write test case to test functionality careful not to repeat same bug Final Coverage line - 99.3% branch - 99.5% condition - 94.5% Code Size 10 Gb Switch Chip (Hierarchical RTL Verilog): 75k lines Bus Functional Models (Verilog) : 6k lines Transaction Verification Model (C++) with random test : 10k lines Test Programs (C++) : 48k lines Total RTL Verilog - 75K lines Total Verification Testbench - 64K lines (almost same as design) Bug Rate 18 16 14 12 10 8 6 4 2 0 Block Level System Level week 300 250 200 150 271 Total Block Level System Level 157 114 100 50 0 week Start Unit Level Verification Start System Level Verification (early functional) Start System Level Verification (full functional) First Code Review Logic Freeze Use Case Simulation Final step Get a few typical applications running on 2 to 3 servers these applications should need to exchange data between them frequently over the LAN obtain data traffic trace over the LAN assuming they are connected by this switch Simulate/Emulate with this traffic and the applications Check applications are running correctly This step is more involved than software simulation requires testing board, emulator, memory dump, accelerator etc. Lessons Learnt Verification needs to start early in design cycle even with partial designs Designers are responsible for block-level verification Dedicated verification team for system-level verification Equivalence check after scan insertion Coverage analysis necessary but not sufficient Hardware/Software co-simulation necessary Only function verification not enough Timing verification & complete DRC check equally important Tutorial Outline Introduction High level design flow and verification issues Theorem proving and Decision procedures Formal verification techniques for FSM models Semi-formal verification techniques Simulation based verification techniques Conclusions and future directions Recap & Conclusion INDRADEEP GHOSH Fujitsu Labs. of America Sunnyvale, California Verification Importance It is obvious that we need to verify a design before fabrication Many famous bugs Pentium floating point Arian 5 rocket blow up Mars polar lander crash lands Design productivity gap technology available to put 1 billion transistors on chip inability of designers to design that kind of chip verification bottleneck 70% of chip design effort is spent on verification Robust and scalable solutions are required verification effort is reduced larger designs can be addressed Various Types of Verification Higher order theorem proving and decision procedures mostly manual effort and cumbersome requires deep understanding of algorithm still mostly in research phase with limited industrial application Formal Verification has become industrial practice in last few years combinational equivalence checking very successful sequential equivalence checking needs work model checking automatic but does not scale well still block level (10,000 gates 1,000 FFs) some techniques to reduce state space are practical may increase frontier by 4-5 times Various Types of Verification Semiformal Verification recently SAT solvers have become extremely efficient bounded model checking is being used handles large designs but can go to about 1,000 cycles deep Simulation Based most popular in industry (mature technology) scalable but requires huge amounts of CPU and memory full chip simulation may not be practical in few years coverage is an issue and cannot prove correctness 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 Current Industry Practices Most designs still start at RTL RTL simulation well understood and used many mature CAD tools getting more and more difficult to do full chip simulation Model checking tools gaining popularity at block level writing meaningful set of properties difficult designers need to change mindset property specification languages becoming popular automatic property extraction cannot go very far many new CAD tool offerings from EDA vendors functionality still evolving Equivalence checking mainstream for certain cases Emulation used for real-time systems Functional verification not end of story timing verification and DRC check very important New CAD Tool Offerings Model Checking tools Semi-formal verification tools Jasper Design Automation Hardware acceleration 0-in Synopsys Magellan Interface/Protocol Verification tools @HDL, Real Intent, Verplex Tharus Systems Coverage analysis and debugging tools Novas Debussy Sugar based tools from TransEDA, Verisity 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 Concluding Remarks Verification is a fundamental problem for everyone It is becoming a design bottleneck in hardware still nascent technology Remains an exciting filed of research Verification will evolve as design methodology evolves path breaking inventions are required serious industrial and academic efforts are required Newer products will emerge in the formal domain not only hardware but software, mechanical, electrical everywhere will not be irrelevant until correct-by-construction from English is possible (looks impossible so far) newer problems, newer solutions No single approach will suffice Thank You Bibliography 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. 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. 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. 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). 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. 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. 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). 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 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 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 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 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 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. 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 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 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 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) 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