Cohesive Coverage Management: Simulation Meets Formal Methods
详细信息 查看全文
- 作者：Aritra Hazra (1) aritrah@cse.iitkgp.ernet.in
Priyankar Ghosh (1) priyankar@cse.iitkgp.ernet.in
Pallab Dasgupta (1) pallab@cse.iitkgp.ernet.in
Partha Pratim Chakrabarti (1) ppchak@cse.iitkgp.ernet.in - 关键词：Simulation – ; Formal property verification – ; Test plan – ; Test points – ; Coverage – ; Assertion – ; Inline assertion – ; Semi ; formal verification
- 刊名：Journal of Electronic Testing
- 出版年：2012
- 出版时间：August 2012
- 年：2012
- 卷：28
- 期：4
- 页码：449-468
- 全文大小：602.3 KB
- 参考文献：1. Accellera. SystemVerilog LRM 3.1a. (2004) http://www.systemverilog.org
2. Adir A, Azatchi H, Bin E, Peled O, Shoikhet K (2005) A generic micro-architectural test plan approach for microprocessor verification. In: The proceedings of 42nd annual Design Automation Conference (DAC), pp 769–774
3. ARM. AMBA Specification Rev. 2.0. (1999) http://www.arm.com
4. Basu P, Das S, Banerjee A, Dasgupta P, Chakrabarti PP, Mohan CR, Fix L, Armoni R (2006) Design intent coverage—a new paradigm for formal property verification. IEEE Trans Comput-Aided Des Integr Circuits Syst 25(10):1922–1934
5. Biere A, Cimatti A, Clarke E, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58:118–149
6. Chockler H, Kupferman O, Kurshan RP, Vardi MY (2001) A practical approach to coverage in formal verification. In: The proceedings of the 13th international conference on computer aided verification, pp 66–78
7. Chockler H, Kupferman O, Vardi M (2003) Coverage metrics for formal verification. In: The proceedings of CHARM, pp 111–125
8. Clarke E, Grumberg O, Peled D (2000) Model checking. MIT Press
9. Clarke E, Kurshan R (1996) Computer aided verification. IEEE Spectrum 33(6):61–67
10. Das S, Banerjee A, Basu P, Dasgupta P, Chakrabarti PP, Mohan CR, Fix L (2005) Formal methods for analyzing the completeness of an assertion suite against a high-level fault model. In: The proceedings of 18th international conference on VLSI design, pp 201–206
11. Dasgupta P (2006) A roadmap to formal property verification. Springer
12. Foster H, Loh L, Rabii B, Singhal V (2006) Guidelines for creating a formal verification testplan. In: The tutorial presented in design and verification conference. San Jose, CA
13. Hazra A, Banerjee A, Mitra S, Dasgupta P, Chakrabarti PP, Mohan CR (2008) Cohesive coverage management for simulation and formal property verification. In: The proceedings of IEEE symposium on VLSI (ISVLSI), pp 251–256
14. Hazra A, Dasgupta P, Chakrabarti PP (2012) Cohesive coverage management leveraging formal test plans. LAP LAMBERT Academic Publishers
15. Hazra A, Ghosh P, Dasgupta P, Chakrabarti PP (2009) Inline assertions—embedding formal properties in a test bench. In: The proceedings of 22nd international conference on VLSI design, pp 71–76
16. Hazra A, Ghosh P, Dasgupta P, Chakrabarti PP (2010) Coverage management with inline assertions and formal test points. In: The proceedings of 23rd international conference on VLSI design, pp 140–145
17. Hoskote Y, Kam T, Ho P, Zao X (1999) Coverage estimation for symbolic model checking. In: The proceedings of 36th annual design automation conference, pp 300–305
18. Li J (2006) Automated risk elimination by formally critiquing verification plan and design documentation. In: The proceedings of DesignCon
19. Magellan. An industrial formal verification tool from synopsys. www.synopsys.com/tools/verification/functionalverification/pages/magellan.aspx
20. Piziali A (2004) Functional verification coverage measurement and analysis. Kluwer Academic Publishers
21. Piziali A (2006) Verification planning to functional closure of processor-based SoCs. In: The proceedings of DesignCon,
22. PSL IP. Property specification language. (2004) http://www.eda.org/ieee-1850
23. Rashinkar P, Paterson P, Singh L (2001) System-on-chip verification: methodology and techniques. Kluwer Academic Publishers
24. Savor T, Seviora R (1997) Directed simulation for automatic detection of failures. In: The proceedings of World congress on systems simulation, pp 432–441
25. Sinha A, Dasgupta P, Pal B, Das S, Basu P, Chakrabarti PP (2009) Design intent coverage revisited. ACM Transact Des Automat Electron Syst 14(1):9:1–9:32
26. Sutherland S (2002) The verilog PLI handbook, 2nd edn. Kluwer Academic Publishers
27. Tasiran S, Keutzer K (2001) Coverage metrics for functional verification of hardware designs. IEEE Des Test Comput 18(4):36–45
28. VCS. An industrial simulator tool from synopsys. www.synopsys.com/tools/verification/functionalverification/pages/vcs.aspx
29. VIS. A formal verification tool from Colorado University. http://vlsi.colorado.edu/~vis - 作者单位：1. Department of Computer Science and Engineering, Indian Institute of Technology Kharagpur, Kharagpur, India
- ISSN：1573-0727
文摘
It has been advocated by many experts in design verification that the key to successful verification convergence lies in developing the verification plan with adequate formal rigor. Traditionally, the verification plans for simulation and formal property verification (FPV) are developed in different ways, using different formalisms, and with different coverage goals. In this paper, we propose a framework where the difference between formal properties and simulation test points is diluted by using methods for translating one form of the specification to the other. This allows us to reuse simulation coverage to facilitate formal verification and to reuse proven formal properties to cover simulation test points. We also propose the use of inline assertions in procedural (possibly randomized) test benches, and show that it facilitates the use of hybrid verification techniques between simulation and bounded model checking. We propose the use of promising combinations of formal methods presented in our earlier papers to shape a hierarchical verification flow where simulation and formal methods aim to cover a common design intent specification. The proposed flow is demonstrated using a detailed case study of the ARM AMBA verification benchmark. We believe that the methods presented in this work will stimulate new thought processes and ultimately lead to wider adoption of cohesive coverage management techniques in the design intent validation flow.