ASPDAC-VLSI 2002 TutorialFunctional Verification of System .ppt

1、ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,1,ASPDAC/VLSI 2002 TutorialFunctional Verification of System on Chip - Practices, Issues and Challenges,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,2,Presenters: Subir K. Roy (Co-ordinator),Synplicity Inc.,935

2、Stewart Drive,Sunnyvale CA 94085,USATel. : 408-215-6049Fax. : 408-990-0296Email: ,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,3,Presenters: S.RameshDept. of Computer Sc. & Engg.,IIT-Bombay, Powai,Mumbai 400 076Tel. : +91-22-576-7722Fax. : +91-22-572-0290Email: rameshcse.iitb.a

3、c.in,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,4,Presenters: Supratik Chakraborty,Dept. of Computer Sc. & Engg.,IIT-Bombay, Powai,Mumbai 400 076Tel. : +91-22-576-7721Fax. : +91-22-572-0290Email: supratikcse.iitb.ac.in,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification

4、 of SoCs“,5,Presenters: Tsuneo Nakata,Fujitsu Laboratories Limited,1-1, Kamikodanaka, 4-Chome,Nakahara-ku, Kawasaki,211-8588, JapanTel. : +81-44-754-2663Fax. :+81-44-754-2664Email: nakataflab.fujitsu.co.jp,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,6,Presenters: Sreeranga P.

5、Rajan,Fujitsu Labs. Of America,595 Lawrence Expressway,Sunnyvale CA 94086-3922,USATel. : 408-530-4519Fax. : 408-530-4515Email: ,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,7,Tutorial Outline,Motivation & Introduction to SoC Design & Re-use. System Verification Techniques for M

6、odule Verification : Formal, Semi-Formal Techniques for System Verification : Simulation, Hybrid, Emulation Quality of Functional Verification : Coverage Issues Academic & Research Lab Verification Tools Case Studies,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,8,Tutorial Outli

7、ne (contd.),Commercial Tools Issues and Challenges / Future Research Topics Summary & Conclusions Bibliography Appendix,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,9,Tutorial Outline (Contd.),Motivation & Introduction to SoC Design & Re-use (Subir K. Roy) Motivation, Verificat

8、ion Heirarchy, System Level Design Flow, SoC Design, SoC Core Types, SoC Design Flow, Implications on Verification. System Verification (S. P. Rajan) Current Design Cycle, Design Cycle with System Verification.,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,10,Tutorial Outline (C

9、ontd.),Techniques for Module Verification Formal Approaches (S. Ramesh) Introduction to Formal Verification Formal Models, Modeling Languages, Formal Methods, Formal Specification, Temporal Logics, CTL, Automatic Verification, Theorem Proving.,ASPDAC / VLSI 2002 - Tutorial on “Functional Verificatio

10、n of SoCs“,11,Tutorial Outline (Contd.),Implementation of Formal Approaches (S. Chakraborty) Binary Decision Diagrams, Combinational Equivalence Checking, Sequential Equivalence Checking, Commercial Equivalence Checkers, Symbolic CTL Model Checking of Sequential Circuits, Forward & Backward Reachabi

11、lity, State of the Art, Related Techniques.,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,12,Tutorial Outline (Contd.),Techniques for Module Verification(contd.) Semi-Formal Approaches Semi-Formal Verification (S. Chakraborty) Interface Specification for Divide & Conquer Verific

12、ation (T. Nakata) Techniques for System Verification Symbolic Simulation & Symbolic Trajectory Evaluation (S. Chakraborty) Hybrid Verification (S. P. Rajan) Emulation (Subir K. Roy),ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,13,Tutorial Outline (Contd.),Quality of Functional

13、Verification (Subir K. Roy) Coverage Metrics Informal, Semi-Formal, Formal. Academic & Research Lab Verification Tools Verification Tools 1 (S. Ramesh) VIS, SMC, FC2toolset, STeP Verification Tools 2 (S. P. Rajan) Fujitsu High Level Model Checking Tool, VeriSoft.,ASPDAC / VLSI 2002 - Tutorial on “Fu

14、nctional Verification of SoCs“,14,Tutorial Outline (Contd.),Case Studies Case Study 1 (S. P. Rajan) ATM Switch Verification Case Study 2 (T. Nakata) Semi-Formal Verification of Media Instruction Unit Commercial Tools (Subir K. Roy) FormalCheck, Specman Elite, ZeroIn-Search, BlackTie,ASPDAC / VLSI 20

15、02 - Tutorial on “Functional Verification of SoCs“,15,Tutorial Outline (contd.),Issues and Challenges / Future Research Topics High Level Specification & Modeling using UML (T. Nakata) Research Issues ( S. Chakraborty) Future Research Directions (S. P. Rajan) Summary & Conclusions Summary ( S. Chakr

16、aborty) Conclusions (Subir K. Roy),ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,16,Tutorial Outline (contd.),Bibliography Papers, Books, Important Web Sites, Conferences, Journals/Magazines. Appendix Linear Temporal Logic, w-Automata based Formal Verification (S. Ramesh) Neat T

17、ricks in BDD Packages (S. Chakraborty) More Research Tools SPIN, FormalCheck (S. Ramesh) More on UML (T. Nakata),ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,17,SoC Design & Re-use (Subir K. Roy),ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,18,Motivation,P

18、entium SRT Division Bug : $0.5 billion loss to Intel Mercury Space Probe : Veered off course due to a failure to implement distance measurement in correct units. Ariane-5 Flight 501 failure : Internal sw exception during data conversion from 64 bit floating point to 16 bit signed integer value led t

19、o mission failure. The corresponding exception handling mechanism contributed to the processor being shutdown (This was part of the system specification).,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,19,Verification Hierarchy,Degree of Automation,Coverage/ Expressive Power,Simu

20、lation,Equivalence Checking of structurally similar circuits,Equivalence Checking,Assume-Guarantee based symbolic simulation/Model Checking,Temporal Logic Based Model Checking,First-Order Theorem Proving,Higher-Order Theorem Proving,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,

21、20,System Level Design Flow,Interface Definition Component Selection ASIC & Software Implementation Glue Logic Implementation PCB Layout Implementation Integration & Validation of Software into System Debugging Board - Manufacturing & Test,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of

22、 SoCs“,21,SoC Design,Core based design approach Design Complexity Time To Market Core : A pre-designed, pre-verified Silicon circuit block. Eg. Microprocessor, VPU, Bus Interface, BIST Logic, SRAM, Memory. Core Integration Re-usable cores : different types, different vendors User defined logic,ASPDA

23、C / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,22,SoC Design,Designing Cores for integration Parameterization Customizable soft cores. Core provider supp-lies essential set of pre-verified parameters. Functionality Single core - preferable Multiple core - Needs good partitioning Inter

24、face Support std. buses to ease integration.,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,23,SoC Core Types,Anderson, 2001 Cell/Macro Library elements DSPs, Microcontrollers Implementation of Standards Function (MPEG, JPEG, CRC, PicoJava,) Interconnects (PCI, SCSI, USB, 1394, I

25、rDA, Bus Bridges) Networking (10/100 ethernet, ATM etc.),ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,24,SoC Core Types,Soft Cores : Technology Independent Synthesizable Description. White Box Implementation - Visible & Modifiable. Core can be extended functionally. Firm Cores

26、: Technology Dependent Gate Level Netlist. Internal implementation of core cannot be modified. User can parameterize I/O to remove unwanted functionality. Hard Cores : Layout & Timing Information provided. Cannot be re-synthesized. Integration is simple & can result in highly predictable performance

27、.,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,25,SoC Design Flow,Co-design approach : Software + Hardware Design exploration at behavioral level (C, C+, etc.) by system architects Creation of Architecture Specification RTL Implementation (Verilog/VHDL) by hardware designers,AS

28、PDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,26,SoC Design Flow,Drawbacks Specification Errors - susceptible to late detection Correlating validations at Behavioral & RTL level difficult Common interface between system & hw designers based on natural language,ASPDAC / VLSI 2002 -

29、 Tutorial on “Functional Verification of SoCs“,27,SoC Implementation Approaches,Vendor Based Approach : ASIC Vendor/Design service group carries out implementation Partial Integration : System Designer implements proprietary & application specific logic. ASIC Vendor integrates above with their cores

30、 In house : ASIC Vendor designs specialized cores. System Designer implements proprietary & appli-cation specific logic, integrates cores & verifies integrated design,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,28,Multiple Sources for IP Reuse,Semiconductor houses I/O Pad, Pro

31、cessor Core, Custom Logic, Memory, Peripheral Interface IP/Core Suppliers Processor Core, Peripheral Interface, Analog /Mixed Signal blocks (DAC, ADC, PLL) System Designer Controller, Custom Logic, AMS blocks,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,29,Advantages of Core/IP

32、 based approach,Short Time To Market (pre-designed) Less Expensive (reuse) Faster Performance (optimized algorithms and implementation) Lesser Area (optimized algorithms and implementation),ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,30,Implications on Verification,Mosensoson,

33、 DesignCon 2000 Verification Focus Integration Verification & Complexity. Bug Classes Interactions between IP/Core/VC blocks Conflicts in accessing shared resources Deadlocks & Arbitration Priority conflicts in exception handling Unexpected HW/SW sequencing,ASPDAC / VLSI 2002 - Tutorial on “Function

34、al Verification of SoCs“,31,Implications on Verification,Need to capture complexity of an SoC into an executable verification environment Automation of all verification activities Reusability of verification components of unit Cores/IPs/VCs Abstraction of verification goals (Eg., Signals to Transcat

35、ions, End to End Transactions) Checkers for internal properties Interface Monitors (BFM, Integration Monitors) Coverage monitors,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,32,Implications on Verification,Implication Rigorous verification of each individual SoC component seper

36、ately Extensive verification of full system Requirements Efficient Verification Methodologies Efficient Tools High Level of Automation,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,33,System Verification (S. P. Rajan),ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of

37、SoCs“,34,Current Design Cycle,OK,Modify RTL Source,Simulation + Formal Verification,RTL/logic Synthesis,Timing Analysis,Modify Script,RTL Description (from Spec/Doc),NOT OK,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,35,Current Design Cycle,Methodology fixed parameter modeling

38、large-scale simulation (expensive) synthesislarge-scale validation (expensive) Design cycle iteration expensive for changes in design parameters Does RTL Description satisfy Specification?,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,36,Design Cycle with System Verification,Val

39、idate = Formally Verify + Simulate,Validate,Cycle Accurate Behavior,Generic Parameters,Cycle Accurate Behavior,Cycle Accurate Behavior,Fixed Parameters,Fixed Parameters,Gate-Level (Large Design),Gate-Level (Small),Validate,Chip,Chip,Instantiation,High/RT-Level Synthesis,Logic Synthesis,ASPDAC / VLSI

40、 2002 - Tutorial on “Functional Verification of SoCs“,37,Design Cycle with System Verification,Parametric Design Methodology: - Higher abstraction level - Reusable generic parametric model - small-scale simulation (low cost) - formal verification viable - Automatic high-level synthesis - validation

41、on a small scale (low cost) Formal verification early in design cycle Drastic reduction in design cost, time-to-market,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,38,Techniques for Module Verification,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,39,Formal

42、 Verification (S. Ramesh),ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,40,Formal Methods,Functional verification SOC context: block level verification, IP Blocks and bus protocols Formally check a formal model of a block against its formal specification Formal - Mathematical, p

43、recise, unambiguous, rigorous Static analysis No test vectors Exhaustive verification Prove absence of bugs rather than their presence Subtle bugs lying deep inside caught,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,41,Three-step process,Formal specification Precise statement

44、of properties System requirements and environmental constraints Logic - PL, FOL, temporal logic Automata, labeled transition systems Models Flexible to model general to specific designs Non-determinism, concurrency, fairness, Transition systems, automata,ASPDAC / VLSI 2002 - Tutorial on “Functional

45、Verification of SoCs“,42,Three-step process (contd.),Verification Checking that model satisfies specification Static and exhaustive checking Automatic or semi-automatic,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,43,Formal verification,Major techniques Equivalence checking Mod

46、el checking Language containment Theorem proving,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,44,EQUIVALENCE CHECKING,Checking equivalence of two similar circuits Comparison of two boolean expressions - BDDs Highly automatic and efficient Useful for validating optimizations, sc

47、an chain insertions Works well for combinational circuits Limited extension to sequential circuits Most widely used formal verification technique. Many commercial tools: Design VERIFYer (Chrysalis), Formality (Synopsis), FormalPro (Mentor Graphics), Vformal(Compass), Conformal (Verplex), etc.,ASPDAC

48、 / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,45,Model checking/Language Containment,Another promising automatic technique Checking design models against specifications Specifications are temporal properties and environment constraints Design models are automata or HDL subsets Checkin

49、g is automatic and bug traces Very effective for control-intensive designs Commercial and Academic tools: FormalCheck (Cadence), BlackTie (Verplex), VIS (UCB), SMV(CMU, Cadence), Spin (Bell labs.), etc. In-house tools: IBM (Rulebase), Intel, SUN, Fujitsu (Bingo), etc.,ASPDAC / VLSI 2002 - Tutorial on “Functional Verification of SoCs“,