Property-Based Dynamic Verification and Test
作者： Dominique Borrione , Katell Morin-Allory , Yann Oddos
DOI: 10.1007/978-94-007-1125-9_8
关键词: Property (programming) 、 Control theory 、 Debugging 、 Computer science 、 Industrial design 、 Abstract syntax tree 、 SIGNAL (programming language) 、 Register-transfer level 、 Formal verification 、 Embedded system
摘要: Property-Based Verification has become a main stream part of industrial design flows, supported by mature technology for the development production quality tools. For large systems that defeat formal verification methods, dynamic is called on designs directly connected to test generators and signal observers are compiled from properties. The tests debug efficiency greatly improved. This chapter exposes principles which this approach implemented in Horus system. Temporal properties, written standard (PSL or SVA) language, automatically translated into synthesizable IP’s, using an efficient proven correct method. Resulting monitors (for observing asserted properties) generating constrained vectors) under Horus, providing instrumented can be simulated, emulated synthesized. method illustrated realistic design: conmax_ip controller.
springer.com
sci-hub.st 参考文章(18)
Martin Schickel, Volker Nimbler, Martin Braun, Hans Eveking, An Efficient Synthesis Method for Property-Based Design in Formal Verification: On Consistency and Completeness of Property-Sets Springer, Dordrecht. pp. 179- 196 ,(2007) , 10.1007/978-1-4020-6149-3_11
Bernard Deadman, Erich Marschner, Grant Martin, IP Reuse Hardening via Embedded Sugar Assertions ,(2002)
Cindy Eisner, Dana Fisman, A Practical Introduction to PSL (Series on Integrated Circuits and Systems) Springer-Verlag New York, Inc.. ,(2006)
Eduard Cerny, Janick Bergeron, Alan Hunter, Andy Nightingale, Verification Methodology Manual for SystemVerilog ,(2005)
Zeljko Zilic, Marc Boul, Generating Hardware Assertion Checkers: For Hardware Verification, Emulation, Post-Fabrication Debugging and On-Line Monitoring ,(2008)
Dominique Borrione, Miao Liu, Pierre Ostier, Laurent Fesquet, PSL-based online monitoring of digital systems forum on specification and design languages. pp. 5- 22 ,(2006) , 10.1007/978-1-4020-4998-9_1
I. Beer, S. Ben-David, C. Eisner, D. Geist, L. Gluhovsky, T. Heyman, A. Landver, P. Paanah, Y. Rodeh, G. Ronin, Y. Wolfsthal, RuleBase: Model Checking at IBM computer aided verification. pp. 480- 483 ,(1997) , 10.1007/3-540-63166-6_53
Michael Huth, Mark Ryan, Logic in Computer Science Cambridge University Press. ,(2004) , 10.1017/CBO9780511810275
Harry Foster, Adam Krolnik, David Lacey, Assertion-Based Design Kluwer Academic Publishers. ,(2010) , 10.1007/978-1-4419-9228-4