Formal verification of a logic design
作者： Udo Krautz , Ulrike Schmidt , Maarten Jakob Boersma
DOI:
关键词:
摘要: A method is provided for verification of a logic design processor execution unit which includes an instruction pipeline with one or more stages. The includes: creating under test using at least first and second instance the design; initializing same value in each stage random values its stages; selecting out plurality instructions simultaneously issuing to test; providing comparison between outputs executing instance; if verifiable by formal model checking, approving correctness result true.
lens.org 参考文章(17)
Rajarshi Mukherjee, Anmol Mathur, Gagan Hasteer, Deepak Goyal, Nikhil Sharma, System, method and computer program product for equivalence checking between designs with sequential differences ,(2005)
Chi Duong, Joseph P. Gergen, Xiao Sun, Method and apparatus for pipeline hazard detection ,(2000)
Hans-Werner Tast, Ralf Winkelmann, Christian Habermann, Matthias Pflanz, Christian Jacobi, Method, System, Computer Program Product, and Data Processing Program for Verification of Logic Circuit Designs Using Dynamic Clock Gating ,(2010)
Xiao Sun, John C. Chan, Method and apparatus for generation of pipeline hazard test sequences ,(2000)
Pavlos Konas, Christopher Mark Songer, Walter David Lichtenstein, Akilesh Parameswar, Earl A. Killian, Ricardo E. Gonzalez, Richard Ruddell, Rangarajan Srinivasan, Nupur Bhattacharyya, Albert Ren-Rui Wang, David William Goodwin, Dror E. Maydan, Marines Puig Medina, Automated processor generation system and method for designing a configurable processor ,(2008)
Ping Gao, Miroslav N. Velev, A method for debugging of pipelined processors in formal verification by correspondence checking asia and south pacific design automation conference. pp. 619- 624 ,(2010) , 10.5555/1899721.1899866
P. Mishra, N. Dutt, Functional Coverage Driven Test Generation for Validation of Pipelined Processors design, automation, and test in europe. pp. 678- 683 ,(2005) , 10.1109/DATE.2005.162
Jason Baumgartner, Hari Mony, Michael Case, Jun Sawada, Karen Yorav, Scalable conditional equivalence checking: An automated invariant-generation based approach 2009 Formal Methods in Computer-Aided Design. pp. 120- 127 ,(2009) , 10.1109/FMCAD.2009.5351131
Ulrich Kuhne, Jorg Bormann, John Barstow, Sven Beyer, Automated formal verification of processors based on architectural models formal methods in computer-aided design. pp. 129- 136 ,(2010) , 10.5555/1998496.1998521
Alexander Kamkin, Eugene Kornykhin, Dmitry Vorobyev, Reconfigurable Model-Based Test Program Generator for Microprocessors international conference on software testing verification and validation workshops. pp. 47- 54 ,(2011) , 10.1109/ICSTW.2011.35