Combining Equivalence Verification and Completion Functions
作者： Mark D. Aagaard , Vlad C. Ciubotariu , Jason T. Higgins , Farzad Khalvati
DOI: 10.1007/978-3-540-30494-4_8
关键词: Register-transfer level 、 Computer science 、 Modular design 、 OpenRISC 、 Cycles per instruction 、 Runtime verification 、 Computer engineering 、 Functional verification 、 Formal methods 、 Equivalence (measure theory) 、 Implementation 、 Theoretical computer science 、 Circuit design
摘要: This work presents a new method for verifying optimized register-transfer-level implementations of pipelined circuits. We combine the robust, yet limited, capabilities combinational equivalence verification with modular and composable strategy completion functions. have applied this technique to 32-bit OpenRISC processor Sobel edge-detector circuit. Each case study required less than fifteen obligations each obligation could be checked in one minute. believe that our approach will applicable large class pipelines in-order execution.
springer.com
sci-hub.st 参考文章(4)
Jerry R. Burch, David L. Dill, Automatic verification of Pipelined Microprocessor Control computer aided verification. pp. 68- 80 ,(1994) , 10.1007/3-540-58179-0_44
Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam Srivas, Formal Verification of a Complex Pipelined Processor formal methods. ,vol. 23, pp. 171- 213 ,(2003) , 10.1023/A:1024716316140
M.N. Velev, Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer design, automation, and test in europe. pp. 28- 35 ,(2002) , 10.5555/882452.874524
Sergey Berezin, Edmund Clarke, Armin Biere, Yunshan Zhu, Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function formal methods. ,vol. 20, pp. 159- 186 ,(2002) , 10.1023/A:1014170513439