Slide 1Applying Data Abstraction to Hardware VerificationChallenge: System-Level VerificationSources of ComplexityExisting Verification MethodsWord-Level AbstractionData Abstraction #1: Bits → IntegersModeling Data SelectionAbstracting Data BitsAbstraction #2: Uninterpreted FunctionsAbstracting FunctionsModeling Data-Dependent ControlAbstraction #3: Modeling Memories as Mutable FunctionsEffect of Memory Write OperationSystems with BuffersSome History of Term-Level ModelingUCLIDChallenge: Model GenerationGenerating Term-Level ModelUnderlying LogicEUF: Equality with Uninterp. FunctsUCLID OperationUCLID ExampleWriting & Reading Register FileWriting Register FileReading Register FileVerifying Safety PropertiesBounded Model CheckingTrue Model CheckingInductive Invariant CheckingAn Out-of-order Processor (OOO)Verifying OOOAdding Shadow StateInvariant CheckingOOO InvariantsState Consistency Invariant ExamplesExtending the OOO ProcessorComparative Verification Effort“I Just Want a Loaf of Bread”Cooking with InvariantsAutomatic Recipe GenerationAutomatic Predicate AbstractionAbstract State SpaceAbstract State MachineGenerating Concrete InvariantSystems Verified with Predicate AbstractionAutomatic Predicate DiscoveryImplementation of Predicate DiscoveryFuture ProspectsCarnegie Mellon UniversitySystem ModelingSystem Modelingand Verificationand Verificationwith UCLIDwith UCLIDSystem ModelingSystem Modelingand Verificationand Verificationwith UCLIDwith UCLIDhttp://www.cs.cmu.edu/~bryantRandal E. BryantContributions by former graduate students:Sanjit Seshia, Shuvendu Lahiri– 2 –Applying Data Abstraction to Hardware VerificationApplying Data Abstraction to Hardware VerificationIdeaIdeaAbstract details of data encodings and operationsKeep control logic preciseApplicationsApplicationsVerify overall correctness of systemAssuming individual functional units correctTechnologyTechnologyUse restricted subset of first-order logicImplement efficient decision proceduresMultiple methods of performing verification– 3 –Alpha 21264 MicroprocessorMicroprocessor Report, Oct. 28, 1996Challenge: System-Level VerificationChallenge: System-Level VerificationVerification TaskVerification TaskDoes processor implement its ISA?Why is it Hard?Why is it Hard?Lots of internal stateComplex control logicComplex functionality– 4 –Sources of ComplexitySources of ComplexityStateStateISA: registers, memoryMicroarchitectural: caches, buffers, reservation stationsConceptually finite state, but practically unboundedControlControlPipelines spread execution across multiple cyclesOut-of-order execution modifies processing orderSuperscalar operation creates parallelismControl logic coordinates everythingResulting behavior matches that of sequential ISA modelFunctionalityFunctionalityArithmetic functions, instruction decoding– 5 –Existing Verification MethodsExisting Verification MethodsSimulators, equivalence checkers, model checkers, …All Operate at Bit LevelAll Operate at Bit LevelRTL modelState encoded as words and arrays of wordsComprised of bitsMost Operate at Cycle or Subcycle LevelMost Operate at Cycle or Subcycle LevelHow each bit of state gets updatedSystem Modeling LanguagesSystem Modeling LanguagesAbstract time up to transaction levelStill view state as collection of bits– 6 –Word-Level AbstractionWord-Level AbstractionData: Abstract details of form & functionsControl: Keep at bit levelTiming: Keep at cycle levelControl LogicControl LogicData PathData PathCom.Log.1Com.Log.2– 7 –Data Abstraction #1: Bits → IntegersData Abstraction #1: Bits → IntegersView Data as Symbolic WordsView Data as Symbolic WordsArbitrary integersNo assumptions about size or encodingClassic model for reasoning about softwareCan store in memories & registersx0x1x2xn-1x– 8 –Modeling Data SelectionModeling Data SelectionIf-Then-Else OperationIf-Then-Else OperationMulitplexorAllows control-dependent data flow10xypITE(p, x, y)10xy1x10xy0y– 9 –Data PathData PathCom.Log.1Com.Log.2Abstracting Data BitsAbstracting Data BitsControl LogicControl LogicData PathData PathCom.Log.1Com.Log.1? ?What do we do about logic functions?– 10 –Abstraction #2:Uninterpreted FunctionsAbstraction #2:Uninterpreted FunctionsFor any Block that Transforms or Evaluates Data:For any Block that Transforms or Evaluates Data:Replace with generic, unspecified functionOnly assumed property is functional consistency:a = x  b = y  f (a, b) = f (x, y)ALUf– 11 –Abstracting FunctionsAbstracting FunctionsFor Any Block that Transforms Data:For Any Block that Transforms Data:Replace by uninterpreted functionIgnore detailed functionalityConservative approximation of actual systemData PathData PathControl LogicControl LogicCom.Log.1Com.Log.1F1F2– 12 –Modeling Data-Dependent ControlModeling Data-Dependent ControlModel by Uninterpreted PredicateModel by Uninterpreted PredicateYields arbitrary Boolean value for each control + data combinationProduces same result when arguments matchPipeline & reference model will branch under same conditionsCondAdataBdataBranch?BranchLogicp– 13 –Abstraction #3: Modeling Memories as Mutable FunctionsAbstraction #3: Modeling Memories as Mutable FunctionsMemory M Modeled as FunctionMemory M Modeled as FunctionM(a): Value at location aInitiallyInitiallyArbitrary stateModeled by uninterpreted function m0MaMam0– 14 –Effect of Memory Write OperationEffect of Memory Write OperationWriting Transforms MemoryWriting Transforms MemoryM = Write(M, wa, wd)Reading from updated memory:Address wa will get wdOtherwise get what’s already in M Express with Lambda NotationExpress with Lambda NotationNotation for defining functionsM = a . ITE(a = wa, wd, M(a))MMa10wd=wa– 15 –Systems with BuffersSystems with BuffersModeling MethodModeling MethodMutable function to describe buffer contentsIntegers to represent head & tail pointers•••••••••tailtailheadheadIn Use••••••tailtailheadheadheadheadIn Use•••0 0 0 0 MaxMax--11MaxMax--11Unbounded BufferCircular Queue– 16 –Some History of Term-Level ModelingSome History of Term-Level ModelingHistoricallyHistoricallyStandard model used for program verificationWidely used with theorem-proving approaches to hardware verificationE.g, Hunt ’85Automated