This work presents a new method for verifying optimized register-transfer-level implementations of pipelined circuits. We combine the robust, yet limited, capabilities of combinational equivalence verification with the modular and composable verification strategy of completion functions. We have applied this technique to a 32-bit OpenRISC processor and a Sobel edge-detector circuit. Each case study required less than fifteen verification obligations and each obligation could be checked in less than one minute. We believe that our approach will be applicable to a large class of pipelines with in-order execution. © Springer-Verlag 2004.
CITATION STYLE
Aagaard, M. D., Ciubotariu, V. C., Higgins, J. T., & Khalvati, F. (2004). Combining equivalence verification and completion functions. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3312, 98–112. https://doi.org/10.1007/978-3-540-30494-4_8
Mendeley helps you to discover research relevant for your work.