Deep Knowledge Test Generators & Functional Verification Methodology IBM Verification Seminar October 2003 - Laurent Fournier IBM Labs in Haifa IBM Labs in Haifa IBM Labs in Haifa Fetch unit All Starting Stages in Holding Position Decode unit Dispatch unit 0 1 2 Completion unit IBM Labs in Haifa 3 IBM Labs in Haifa Extreme Case of Influence on Sticky Bit 1.00111011000111110001110000001110001000111 Rounder 1.00111011000111110010 I 1.cccccccccccccccccccccc000000000000000000001 IBM Labs in Haifa IBM Labs in Haifa Motivation for Deep Knowledge Test Generation Gap + Bug-Prone Control of test generator IBM Labs in Haifa Interesting scenarios IBM Labs in Haifa Deep Knowledge Test Generator? Definition Test generation focused on specific verification areas, e.g. FPU, Microarchitecture Flow, SCU Problem Inefficiency of generic architecture tools in specific error-prone verification areas (bugs not found or found late) Objectives To provide greater control to reach non-covered areas To enable a systematic and comprehensive verification approach to speed up the rate of coverage IBM Labs in Haifa IBM Labs in Haifa The Players FPgen Generic, quasi-optimal solution for a welldefined, albeit complex, field Complex mathematic algorithms Piparazzi An evolving solution to cope with microarchitecture flow complexity Classic constraint solving engine (CSP) DeepTrans More a library of services for now Rounds off the model-based technology IBM Labs in Haifa IBM Labs in Haifa Motivation: Floating Point Bugs General bug curve number of bugs time FP bug curve number of bugs time IBM Labs in Haifa IBM Labs in Haifa Basic Functionality OP1 DIV [FP1, PF2] 1100100010 0101001110 OP2 0X1X001X10 1101011100 1001001101 Multiple random Random solution:solution: Control of coverage sought density Uniform distribution IBM Labs in Haifa Result Denormal 1000110000 0010001010 Max 4 bits set IBM Labs in Haifa Piparazzi – The Main Concept iop[0].PIPELINE = FXU Fetch Decode Dispatch Micro-architecture Model iop[1].PIPELINE User’s request = LSU file iop[1].DISPATCH = iop[0].DISPATCH Iop[0].stage[STAGE_2].STALL > 0 Solver A test program for Micro-processor IBM Labs in Haifa IBM Labs in Haifa Input can be a Full Cross-Product Example: All types model Operand1 +/- Infinity +/- Zero +/- Norm +/- Denorm +/- Large number +/- Small number +/- Min Denorm +/- Max Denorm +/- Min Norm +/- Max Norm IBM Labs in Haifa Multiply Operand2 +/- Infinity +/- Zero +/- Norm +/- Denorm +/- Large number +/- Small number +/- Min Denorm +/- Max Denorm +/- Min Norm +/- Max Norm = Result +/- Infinity +/- Zero +/- Norm +/- Denorm +/- Large number +/- Small number +/- Min Denorm +/- Max Denorm +/- Min Norm +/- Max Norm IBM Labs in Haifa Relationship between Generator Input Language and Test-plan FPgen Test-Plan "Language shapes the way we think, and determines what we can think about" - B.L.Whorf IBM Labs in Haifa IBM Labs in Haifa Fetch unit Generalized Piparazzi Example Decode unit Dispatch unit 0 1 2 Completion unit IBM Labs in Haifa 3 IBM Labs in Haifa Generalized FPgen Example 1.00111011000111110001110000001110001000111 Rounder 1.00111011000111110010 I 1.cccccccccccccccccccccc000000000000000000001 1.cccccccccccccccccccccc000000000000000000010 … 1.cccccccccccccccccccccc100000000000000000000 IBM Labs in Haifa IBM Labs in Haifa Generic Test Plans Dsasjfdlhfkfjs dfajdlkfj lkDsafk l;kf;daslkf; aslkfa; Sadglk;flkgfdlkDsafkl kf;das lkf;aslkfa; Sadglk;flkgfdlk Dsafkl;kf;d aslkf;aslkfa; Sadglk;flkgfdlk Dsasjfdlhfkfjs dfajdlk j lkDsafk l;kf;daslkf; aslkfa; Sadglk;flkgfdlk Dsafkl;k f;daslkf;aslkfa; Sad glk; flkgfdlk fkl;kf;d aslkf;aslk fa; Sadglk; flkg fdlk Dsasjfdlhfkfjs dfajdlkfj lkDsafk l;kf;daslkf; aslkfa; Sadglk;flkgfdlkDsafkl kf;das lkf;aslkfa; Sadglk;flkgfdlk Dsafkl;kf;d aslkf;aslkfa; Sadglk;flkgfdlk Dsasjfdlhfkfjs dfajdlk j lkDsafk l;kf;daslkf; aslkfa; Sadglk;flkgfdlk Dsafkl;k f;daslkf;aslkfa; Sad glk; flkgfdlk fkl;kf;d aslkf;aslk fa; Sadglk; flkg fdlk Methodology – Resource Dependent Density Crossing Reduction Huge models IBM Labs in Haifa IBM Labs in Haifa Ingredients for Test-Plan IEEE test suites Generic & alternative Implementations IEEE standard Bug analysis Papers Test-Plan Test plans from users IBM Labs in Haifa IBM Labs in Haifa The Evolution of Functional Verification Methodology Small design: manual to reach all suspected cases Slow and tedious IBM Labs in Haifa IBM Labs in Haifa The Evolution of Functional Verification Methodology Increased complexity: Random generators No uniformity in bug location probability IBM Labs in Haifa IBM Labs in Haifa The Evolution of Functional Verification Methodology Biased Random generator to control towards suspected areas Faster and more effective IBM Labs in Haifa IBM Labs in Haifa The Evolution of Functional Verification Methodology Deep Knowledge Test Generators Many fast accesses to areas with a high probability of bugs IBM Labs in Haifa IBM Labs in Haifa Coverage by Generation Writes specific Def-files to cover missing items Coverage by generation: feedback: n Test Pla and 1. fourscore s ago 2. seven year rs brought 3. our fathe n this 4. forth upo a new 5. continent eived in 6. nation conc Jan Type task Def-Files Writes Def-files general directly Def-filesasking for model 7. liberty IBM Labs in Haifa Type task Type task Type task Type task DKTGs Comprehensive test generators (FPGen, Piparazzi) (Gpro, X-Gen) Coverage tools (Meteor) Feb Mar Apr May Jun J ul Aug Sep Oct Nov Dec IBM Labs in Haifa Randomness Speed DKTG Performance Broad approach TG GPro, AVPGen DKTG Manual testing Control IBM Labs in Haifa IBM Labs in Haifa Coverage Graph Generation method 100% # events tested DKTG GPro Time IBM Labs in Haifa IBM Labs in Haifa Cross-Product Approach Bugs often lie in the interaction of several factors. This approach is more than a list of disparate tasks. It may include, often inadvertently, many “quasi corner cases”. All types model. Some cases are clearly corner cases, but others, while interesting, might have been overlooked. IBM Labs in Haifa IBM Labs in Haifa Quasi Corner Cases Straightforward cases Less interesting IBM Labs in Haifa Quasi corner cases Corner cases More interesting IBM Labs in Haifa The Non-Uniform View IBM Labs in Haifa IBM Labs in Haifa Pitfalls Quantity at the price of quality Easy to create large, not meaningful event spaces More events than can be covered (waste of verification bandwidth) Leads people to be “thought-lazy” because easy to generate impressive test-plan (quantity-wise) Blindly rely on “nice” coverage numbers Includes many events that require significant effort in knowing whether or not they are reachable (double-edged sword) IBM Labs in Haifa IBM Labs in Haifa Conclusion: The Test-Plan Feedback Loop Test plantest plan Generic Updated DKTG tool development IBM Labs in Haifa IBM Labs in Haifa Test Plan Scope Conclusion: DKTG Impact DKTG Existing Verification Means Knowledge & Control IBM Labs in Haifa IBM Labs in Haifa Technology Perspective Bug prone area CSP Solvers Coverage-based generation Core generation Cross-Products Randomness Slow, tedious, small design RTPG IBM Labs in Haifa Extended control: Randomness vs.specific Generic Productivity 1988 Manual testing Model based 1994 Genesys MBTG Focused approach 1998 2001 Genesys-Pro DKTG Genie