SISCO：选择性不变共享、聚类和排序用于有效的多属性形式验证.pdf

1、SISCO:Selective Invariant Sharing,Clustering and Ordering for EffectiveMulti-Property Formal VerificationSourav Das1,Aritra Hazra1Pallab Dasgupta2,Himanshu Jain2,Sudipta Kundu21Indian Institute of Technology Kharagpur2Synopsys Inc.USAOutline01060502Property DirectedReachability Overview03Introductio

2、nMotivatingExamplesSISCOCurrentState of the ArtConclusion andFuture WorkPDR0407ExperimentalResultsFramework and AlgorithmIntroductionModel Checking tools are not designed for multi-property verificationStatic Cone-of-Influence(COI)methods exists but they do not scale for practical or industrialdesig

3、nsKey observation from recent experience:1.Inductive Invariants discovered while proving one property can help another property2.This motivates ordering properties in a way that earlier ones helps the later ones3.Unfortunately there is no way to know a priori which one will help whichQuestion that l

4、ead to this work:1.Are all invariants required for solving undecided goals?2.Can we improve effectiveness of falsified goals?Current State of the ArtP1P2PnP1P2PnVerification EngineProperties PProperties PSequential Verification of Multi-property DesignsProperty PartitioningProperties Pp1p2p3p4p5p6p7

5、p2p1p5p7p4p6p3Identical WorkersStrategy PartitioningProperties Pp1p2p3p4p5p6p7PPPPPDifferent WorkersParallel Verification of Multi-Property DesignsP1P2P1P2P3P1P3Property Clustering of designs based on COIP3Property Directed Reachability(PDR)Frame=0Create Solvercube=GetBadState(.)IF(cube!=NULLIF(Bloc

6、kState(.)Increment Frame and Create SolverIF(PushClause(.)SATUNSATYYYNNNSTOPGeneralization ProcedurePush Clauses Up and DownMotivating ExamplesClaims and ObjectivesStoring Counter Example(CEX)traces helpsInvariant Sharing is requiredAll the Invariants are not useful010203Motivating Example(Falsified