Word-Level Counterexample Reduction Methods for Hardware Verification

Abstract

Hardware verification is crucial to ensure the correctness in the logic design of digital circuits. The purpose of verification is to either find bugs or show their absence. Prior works mostly focus on the bug-finding process and have proposed a range of verification algorithms and techniques to be faster to reach a bug or conclude with a proof of correctness. However, for a human verification engineer, it also matters how to better analyze the counterexamples trace to understand the root cause of bugs. This kind of technique remains absent in word-level circuit analysis. In this paper, we investigate the counterexample reduction method. Given the existing techniques for the bit-level circuit model, we first extend current semantic analysis methods to the word-level counterexample reduction and then develop a more efficient word-level structural analysis approach. We compare the effectiveness and overhead of these methods on the hardware model-checking problems and show the usefulness of such analysis in applications including pivot input analysis, word-level model-checking and counterexample-guided abstraction refinement.

Zhiyuan Yan

Ph.D. student in Microelectronics Thrust

My research interests include hardware formal verification, AI for EDA and Boolean Satisfiability Problem.