WIXLIB

Advanced VerificationTechniques for DO-254Mike Bartley (mike@testandverification.com)Test and Verification SolutionsDelivering Tailored Solutions forHardware Verification and Software Testing

Agenda Some background Advanced Verification Techniques Compliance Hardware (Software) Combining Advanced Verification Techniqueswith ComplianceCopyright TVS Limited Private & Confidential Page 2

A Quick Intro to your Speaker PhD in Mathematical Logic Worked in software testing and hardware verification forover 25 years IPL, Praxis, ST-Micro, Infineon, start-ups (Elixent and ClearSpeed) TVS Started TVS in 2008 Software testing and hardware verification products and servicesCopyright TVS Limited Private & Confidential Page 3

TVS – Leaders in Testing and VerificationGermany - 2011UK - 2008France - 2012ChinaSouth KoreaIndia - 2011Consistentrevenuegrowth 2011-12 1.5M2013-14 3.5M2014-15 4M ContinuousgeographicalSingapore - 2014 expansion 2012-13 2.5M Deliver services closer to our customersServices where costs & staff availability are important factorsRun projects on client sites or off-siteHelp customers implement off-shore verification and testingCopyright TVS Limited Private & Confidential Page 4

Customers and Customer RetentionBroadcom2 yearsInfineon5 yearsIntel2 yearsNVIDIA4 yearsNXP2.5 yearsST3 yearsCopyright TVS Limited Private & Confidential Page 5

Some “advanced” verification techniques Constrained Random“Verification Functional Coverageit's all aboutconfidence”Code CoverageMike Bartley,Formal VerificationSNUG 2001Regression results metricsBug rate analysisAnalysis of open issuesCode review completionWhich ones to adopt?Mutation analysisSoftware runningIndependent verification teamAre all requirements verified?Copyright TVS Limited Private & Confidential Page 6

The Human Factor in VerificationWhy do we need separate verification team? Errors are introduced by (mis)interpretation.Assumes you have aspecification!SpecificationRTL CodingInterpretationDANGER: When a designer verifiesher/his own design – then she/heis verifying her/his owninterpretation of the designInterpretationRTLVerificationRTL pyright TVS Limited Private & Confidential Page 7

Functional Verification TrendsIndustry evolving its functional verification techniquesWilson Research Groupand Mentor Graphics2010 FunctionalVerification Study,Used with tion41%64%2007201048%Code coverage72%Listen to the2012 surveyHarry Foster atDVClub April8th40%Functional coverage72%0%10%20%30%40%50%60%70%80%35%29%Median peak number ofverification engineers30%2007201025%19%The adoption offormal propertychecking hasgrown by 53%20%15%10%5%0%20072010Copyright TVS Limited Private & Confidential Page 8

The mechanics of an advanced test DesignUnderTestassertCoverageActivePassiveCode CoverageCopyright TVS Limited Private & Confidential Page 9

What is functional Coverage? Examples The system may transfer packets of differentsizes The test plan may require that transfer sizes with thefollowing size or range of sizes be observed: 1, 2, 3, 4 to 127, 128 to 252, 253, 254, or 255 Functional coverage also examines therelationships between different objects Cross coverage An example of this would be examining whether an ALU hasdone all of its supported operations with every differentinput pair of registers And if the ALU has written back to an input registerCopyright TVS Limited Private & Confidential Page 10

Adding value to your current test assiveExisting Test t TVS Limited Private & Confidential Page 11

Add advanced techniques to your current test benchTechniqueEffortValueCodeCoverage Low effort to start measuring High effort to “sign-off” holes Very useful when 100% When 100% - need other dataFunctionalCoverage High effort to define a full coveragemodel High effort to implement thecoverage model High effort to “sign-off” holes Check that major features arefully verifiedAssertions Effort varies with number ofassertions High value with well definedassertions High value for debugChecker Effort varies with sophistication ofthe checker High value – can write testsmore quickly. Can considerpseudo randomConstrainedrandom High effort – complex Needs a checker and fnal coverage Very highCopyright TVS Limited Private & Confidential Page 12

The mechanics of finding a bug in simulationStimulatePropagate .0101010101100101 . .0100110111110101 .00010101 . .10011010 .01001101Design Under TestMutation testingadds value in termsof test erveCompareCopyright TVS Limited Private & Confidential Page 13

Add advanced techniques to your current test benchTechniqueEffortValueCodeCoverage Low effort to start measuring High effort to “sign-off” holes Very useful when 100% When 100% - need other dataFunctionalCoverage High effort to define a full coveragemodel High effort to implement thecoverage model High effort to “sign-off” holes Check that major features arefully verifiedAssertions Effort varies with number ofassertions High value with well definedassertions High value for debugChecker Effort varies with sophistication ofthe checker High value - High value – canwrite tests more quickly. Canconsider pseudo randomConstrainedrandom High effort – complex Needs a checker and fnal coverage Very highMutationAnalysis Low effort to adopt a tool High effort to run and analyse output Low effort for “Do It Yourself” Very high if using tool –discover quality of you verif. Copyright“DIY”usefulTVS willLimited give Private &Confidentialfeedback Page 14

The rise of design IPExternal IP increase by 138% from 2007 to 2010Wilson Research Group and Mentor Graphics2010 Functional Verification IePCIehardwareFPGAPCIeVIPCopyright TVS Limited Private & Confidential Page 15

Functional Verification amicFormalSimulation PrototypingDynamic eckingTheoremProvingEmulationCopyright TVS Limited Private & Confidential Page 16

The adoption of formal propertychecking has grown by 53% a busy and b busy are never both asserted on thesame cycle if the input ready is asserted on any cycle, then theoutput start must be asserted within 3 cycles if an element with tag t and data value d enters theblock, then the next time that an element with tag tleaves the block, its data value is the same as theoutput of a reference piece of combinatorial logicfor which the input is d stall cannot remain high indefinitelyCan be checked duringsimulation (but not provedby simulation)Formal Verification: Some example propertiesA livenesspropertyCopyright TVS Limited Private & Confidential Page 17

Model Checking – a brief introductionInputs to the tool 3 inputs to the tool For example A model of the design– Usually RTL A property or set ofproperties representing therequirements– Items are transmitted to one of threedestinations within 2 cycles of beingaccepted (req in && gnt in) - ##[1;2](rec a rec b rec c) A set of assumptions,expressed in the samelanguage as the properties typically constraints on theinputs to the design– The request signal is stable until it isgranted (req in && !gnt out) - ##1req in We would of course need acomplete set of constraintsCopyright TVS Limited Private & Confidential Page 18

Model Checking – a brief introductionOutputs from the tool Proved the property holds for all valid sequences of inputs Failed(n) there is at least one valid sequence of inputs of length n cycles, asdefined by the design clock, for which the property does not hold. In this case, the tool gives a waveform demonstrating the failure. Most algorithms ensure that n is as small as possible, but some moreadvanced algorithms don’t. Explored(n) there is no way to make the property fail with an input sequence of ncycles or less For large designs, the algorithm can be expensive in both time andmemory and may not terminateCopyright TVS Limited Private & Confidential Page 19

The Strengths of Model Checking Ease of set-up No test bench required, add constraints as you go, VIP? Flexibility of verification environment Constraints can be easily added or removed Full proof Of the properties under the given constraints (Can also prove “completeness” of the properties) Intensive stressing of design Explored(n) constitutes a large amount of exploration of the design Judgement when the number of cycles explored in a run is sufficient Significant bugs already found within a this number of cycles Corner cases Find any way in which a property can fail (under the constraints)Copyright TVS Limited Private & Confidential Page 20

Potential issues with formal verification False failures Need constraints to avoid invalid behaviour of inputs False proofs Bugs may be missed in an over-constrained environment. Limits on size of the model that can be analysed Non-exhaustive checks: Explored(n) Interpret the results Can require significant knowledge and skill Non-uniform run times Often it cannot be predicted how long it will take for a check either toterminate or to reach a useful stageThis can make formal unpredictable!Copyright TVS Limited Private & Confidential Page 21

Safety-critical Systems “A safety critical system is a system wherehuman safety is dependent upon the correctoperation of the system” Elements of safety critical systems: Computer hardware Other electronic and electrical hardware Mechanical hardware Operators or users Software Traditionally associated with embeddedcontrol systemsCopyright TVS Limited Private & Confidential Page 22

Safety Standards IEC61508: Functional Safety ofElectrical/Electronic/Programmable Electronic Safety-relatedSystems IEC60880: Software aspects for computer-based systemsperforming category A functions DO178: Software considerations in airborne systems andequipment certification DO254: Design Assurance Guidelines for Airborne ElectronicHardware EN50128: Software for railway control and protection systems IEC62304: Medical device software -- Software life cycleprocesses ISO26262: Road vehicles – Functional safetyCopyright TVS Limited Private & Confidential Page 23

Safety StandardsProcess objectives and outputsIntegrity levels/classesPicture from Kyle Beane http://www.noisefestival.com/node/14294Copyright TVS Limited Private & Confidential Page 24

DO-254 identifies the following data items Hardware Verification PlanValidation and Verification StandardsHardware Traceability DataHardware Review and Analysis ProceduresHardware Review and Analysis ResultsHardware Test ProceduresHardware Test ResultsHardware Acceptance Test CriteriaProblem ReportsHardware Configuration Management RecordsHardware Process Assurance RecordsCopyright TVS Limited Private & Confidential Page 25

DO-254 identifies the following data items Hardware Verification PlanValidation and Verification StandardsHardware Traceability DataHardware Review and Analysis ProceduresHardware Review and Analysis ResultsHardware Test ProceduresHardware Test ResultsHardware Acceptance Test CriteriaProblem ReportsHardware Configuration Management RecordsHardware Process Assurance RecordsCopyright TVS Limited Private & Confidential Page 26

A closer look Hardware Verification Plan The hardware verification plan describes the procedures,methods and standards to be applied and the processes andactivities to be conducted for the verification of thehardware items. Hardware Traceability Data Hardware traceability establishes a correlation between therequirements, detailed design, implementation andverification data to support configuration control,modification and verification of the hardware itemCopyright TVS Limited Private & Confidential Page 27