1、Case study: Integrating FV and DV in the Verification of Intel Core2 Duo Microprocessor,Alon Flaisher Alon Gluska Eli SingermanIntel Corporation Israel Design Center,A. Flaisher,2,Presentation Goals,Share how the integration of FV with dynamic verification improved the productivity & quality of Mero
2、m verification Highlight some of the barriers in effective deployment of FVUpdate how FV is used in todays CPU designs and what are the future challenges,A. Flaisher,3,Outline,Challenges Applying FV in Merom Our FV/DV synergy approach Examples Looking forward,A. Flaisher,4,Challenges in Applying FV
3、in Merom,Allocate resources for FV Replace traditional dynamic verification (DV) activities Choose the best designs to FV Quickly establish new FV environments,A. Flaisher,5,Our Approach FV/DV Integration,Replaced DV activities For each DUT decided what would be the effect on DV 75% of the proofs re
4、placed DV activities, mainly coverage Enabled allocating resources for FV FV was also applied by VE (non FV experts) Familiar with the design, owned both activities Compared the complexity of the design vs. the proof Provided more flexibility in assigning engineers to FV FVE established FV environme
5、nts for VE Better utilized expertise Joint decision where to apply FV Joint test plans and checking,A. Flaisher,6,Example 1: ALU Cluster,Independent execution units FV done in 2nd half of the project Cluster level FV using symbolic simulation (STE/FL) FVE built a Cluster Formal Environment Active un
6、it driven symbolically Remaining units driven with Xs The unit owner (VE) coded the spec/checkers for each micro- instruction in FL Thousands of micro-instructions Some are very simple to code, once you know the spec,A. Flaisher,7,Example 1: ALU Cluster (Cont.),FV/DV approach provided much higher ve
7、rification quality for comparable investment! Higher quality verification 98% of the micro-instructions fully verified! Unit dependencies also verified Zero bugs found in silicon Reduction of effort Done instead of coverage (which requires huge investment) Good utilization of expertise FVers built t
8、he CFE and carried out highly complex proofs DVers wrote most specs,A. Flaisher,8,Example 2: MS Unit,The MS unit Translates instructions to uop sequences Needs to support all combination of uops and events (any ROM) Unit was completely FV by an expert VE MS team chose FV as the main verification too
9、l Used BMC on unit boundaries 1400 vars, bound 40 Reference model for checking,A. Flaisher,9,Example 2: MS Unit (Cont.),FV/DV provided much higher quality for less effort! FV found corner case bugs impractical for simulation Prevented bugs from being released Replaced most DV activities Enabled by t
10、he MS validation team,A. Flaisher,10,Looking Forward,FV integration to mainstream verification continues to grow in current CPU designs More FV resources in Sandy Bridge (Intels 2010 TOC) Good acceptance throughout the project Single spec language for RTL assertions and FV (SVA) Aggressive ABV metho
11、dology improves assertion FV ROI Sharing (unit level) checkers through SV reference-models,A. Flaisher,11,Looking Forward (Cont.),Good results from applying FV for bug-hunting Integrate FV for bug hunting in early stages Integrate FV to get highest confidence in later stagesKey capabilities are still missing Sharing FV/DV environments Unit level capacity Solutions for system level properties Predictability and complexity analysis ,Q&A,
