Formal guarantees for localized bug fixes

Mitra, Srobona ; Banerjee, Ansuman ; Dasgupta, Pallab ; Ghosh, Priyankar ; Kumar, Harish (2013) Formal guarantees for localized bug fixes IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 32 (8). pp. 1274-1287. ISSN 0278-0070

Full text not available from this repository.

Official URL:

Related URL:


Bug traces produced in simulation serve as the basis for patching the RTL code in order to fix a bug. It is important to prove that the patch covers all instances of the bug scenario; otherwise, the bug may return with a different valuation of the variables involved in the bug scenario. For large circuits, formal methods do not scale well enough to comprehensively eliminate the bug, and achieving adequate coverage in simulation and regression testing becomes expensive. This paper proposes formal methods for analyzing the control trace leading to the observed manifestation of the bug and verifying the robustness of the bug fix with respect to that control trace. We propose a classification of the bug fix based on the guarantee that our analysis can provide about the quality of the bug fix. Our method also prescribes the types of tests that are recommended to validate the bug fix on other types of scenarios. Since our methods are more scalable by orders of magnitude than model checking the entire design, we believe that the proposed formal methods hold immense promise in analyzing bug fixes in practice.

Item Type:Article
Source:Copyright of this article belongs to Institute of Electrical and Electronics Engineers.
Keywords:Satisfiability; Debugging; Dynamic Slicing; Hardware Verification
ID Code:101010
Deposited On:09 Mar 2018 10:16
Last Modified:09 Mar 2018 10:16

Repository Staff Only: item control page