Synthesis and VerificationFormal and Semi-Formal Verification.ppt
《Synthesis and VerificationFormal and Semi-Formal Verification.ppt》由会员分享,可在线阅读,更多相关《Synthesis and VerificationFormal and Semi-Formal Verification.ppt(93页珍藏版)》请在麦多课文档分享上搜索。
1、Synthesis and Verification Formal and Semi-Formal Verification,Contract #: TJ-684,October 14, 2018,2,Accomplishments!,Yuan Lu (now at BroadComm Inc.) and Marius Minea (now PostDoc at Berkeley) graduated in the year 2000!,Automatic Abstraction by Counterexample-guided Refinement,Edmund M. Clarke Yuan
2、 Lu Pankaj Chauhan Anubhav GuptaJoint work with Orna Grumberg, Somesh Jha, Helmut Veith,684.004: Abstraction in Model Checking,Description: Counterexample-guided Abstraction Refinement Goals: To provide a new abstraction technique to verify large designs.,October 14, 2018,4,684.004: Abstraction in M
3、odel Checking,Plans and directions for the current year (2000): Experiment with other abstraction refinement techniques Experiment on benchmark and industrial designs Abstraction in the context of bounded model checking Experiment on industrial designs (PCI bus protocol),October 14, 2018,5,October 1
4、4, 2018,6,684.004: Abstraction in Model Checking,Accomplishments for the current year (2000): Yuan Lu graduated! Automatic abstraction generation Release of aSMV tool Extensive experimentation with impressive results,684.004: Abstraction in Model Checking,Plans and directions for the next year (2001
5、): Extending the methodology to include all ACTL countertexamples Using SAT for refinement of large state spaces,October 14, 2018,7,684.004: Abstraction in Model Checking Milestones,Automatic abstraction function generation (31-Dec-2000) Development of hierarchical verification algorithms (31-Dec-20
6、00) Extending the methodology to include all ACTL* counterexamples and implementation (31-Dec-2001) Using SAT based techniques for refinement of large state spaces (31-March-2001),October 14, 2018,8,684.004: Abstraction in Model Checking Deliverables,Report on hierarchical model checking without fla
7、ttening for hierarchical circuit descriptions (Planned 31-Dec-2000) Report on model checking of hierarchically structured SMV and StateCharts for embedded systems and mixed hardware designs (Planned 31-Dec-2001) Report/Paper on Extension of methodology for all counterexamples (Planned 31-Dec-2001) N
8、ew version of aSMV with this feature (Planned 30-March-2001) Report/Paper on refinement using large state spaces (Planned 31-June-2001) New version of aSMV with SAT based refinement (Planned 31-Dec-2002),October 14, 2018,9,October 14, 2018,10,Existential Abstraction,M,Mh,Given an abstraction functio
9、n h : S Sh, the concrete states are grouped and mapped into abstract states,M Mh and Mh |= M |= ,October 14, 2018,11,Our Abstraction Methodology (CAV2000),October 14, 2018,12,Highlights of Our Methodology,Impressive results, on average, 3.5x time, 17x space improvements! A large Fujitsu multimedia p
10、rocessor verified Handles all ACTL* loop/path counterexample But. What about non-loop/non-path counterexamples? What if infeasible to check validity of counterexamples?,October 14, 2018,13,General Counterexamples for ACTL*,Not all the counterexamples in ACTL* are linear (path or loop).How to refine
11、the abstraction when a counterexample is not linear?What are counterexamples?How to generate “readable” counterexamples?,October 14, 2018,14,Tree-like Counterexamples,What does the counterexample for (AG p) (AF q) look like?(AG p) (AF q), (EF p) (EG q),October 14, 2018,15,Counterexamples for ACTL,Th
12、eorem All ACTL formulas have tree-like counterexamples.Why tree-like counterexamples ?easy to diagnosedecomposable to simple paths and loops,October 14, 2018,16,Generate Counterexamples for ACTL,We propose an algorithm to generate tree-like counterexamples for ACTLTraverse the parse tree of the form
13、ula in DFS orderGenerate path or loop counterexamples for each node in the parse tree.Glue all the sub-counterexamples for the total,Symbolic!,October 14, 2018,17,Using SAT for Abstraction Refinement,Problem Domain: Hardware circuits with more than 5000 latches! Path/loop counterexamples onlyI : Pri
14、mary Inputs R: Visible Variables A: Invisible Variables V = R U A |R| |V|,C,L,I,R,R,A,A,October 14, 2018,18,Spurious Path Counterexample,Th is spurious,The concrete states mapped to the failure state are partitioned into 3 sets,October 14, 2018,19,Checking the Validity of Counterexample,Describe the
15、 abstract counterexample using propositional formulaFeed the formula to SAT checker Size of SAT problem is linear in the circuit size For a spurious trace, dead end states Si,0 are obtained Set of dad states is could be empty,October 14, 2018,20,Example of Approximation,October 14, 2018,21,Modified
16、Refinement Methodology,October 14, 2018,22,Heuristics for Refinement,Use GRASP (Sakellah et. al.)/Chaff(Mallik et.al.) for checking validity of counterexample Modify these procedures to identify important variables Most backtracked to variable Largest transitive fanout in implication graph(IG) Uniqu
17、e Implication Points Variables from conflicting clauses ,October 14, 2018,23,Implementation Details,visible boolean x; ,Modified NuSMV,Intermediate Block,Modified GRASP/Chaff,Mh|= ,New vars,Th, M,Th, M, Bad, DeadEnd,Sat?, Auxiliary Info,October 14, 2018,24,Future Work,Generate non-path/non-loop coun
18、terexamples Refinement using those counterexamples Formalize and evaluate the heuristics for picking up visible variables using GRASP/Chaff Experiments!,Model Checking and Theorem Proving: A Unified Framework,Sergey Berezin Edmund M. Clarke,October 14, 2018,26,684.005: Combining Model Checking with
19、Theorem Proving,Description: An approach to unifying Model Checking and Theorem Proving in a single framework Goals: Design a framework to combine new state-of-the-art model checking and theorem proving techniques efficiently Develop a tool that supports this framework,October 14, 2018,27,684.005: C
20、ombining Model Checking with Theorem Proving,Plans and directions for the current year (2000):Verify a large hardware example (like PCI bus) Study how the combination of model checking and theorem proving improves both techniques Continue the development of the implementation,October 14, 2018,28,684
21、.005: Combining Model Checking with Theorem Proving,Accomplishments for the current year (2000): Formulated a framework that unifies model checking and theorem proving in a very general way Came up with a new methodology for efficient specialization of theorem proving to particular problem domains I
22、mplemented a “prover generator“ as a new version of SyMP based on the above methodology Implemented the necessary components of the proof system for combining model checking and theorem proving as an instance of a prover generated by SyMP Verified an example of an IBM cache coherence protocol,Octobe
23、r 14, 2018,29,684.005: Combining Model Checking with Theorem Proving,Plans and directions for the next year (2001): Include several powerful reduction rules into the default proof-system of SyMP (like various forms of abstraction, compositional reasoning techniques, etc.) Verify a few more examples
24、using these reduction rulesImplement one or more other proof systems (either completely different or specialized and more automated versions of the default system) in the tool and demonstrate that it works as a prover generator,October 14, 2018,30,684.005: Combining Model Checking with Theorem Provi
- 1.请仔细阅读文档,确保文档完整性,对于不预览、不比对内容而直接下载带来的问题本站不予受理。
- 2.下载的文档,不会出现我们的网址水印。
- 3、该文档所得收入(下载+内容+预览)归上传者、原创作者;如果您是本文档原作者,请点此认领!既往收益都归您。
下载文档到电脑,查找使用更方便
2000 积分 0人已下载
下载 | 加入VIP,交流精品资源 |
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- SYNTHESISANDVERIFICATIONFORMALANDSEMIFORMALVERIFICATIONPPT

链接地址:http://www.mydoc123.com/p-389545.html