Effective bug localization during verification is a challenging step in the development cycle of complex hardware designs. While meeting different coverage goals is possible in the verification process, yet bug localization cannot be directly related to such goals. We propose a two-step methodology to achieve fine-grained design bug localization. First, we obtain multiple error traces based on a failing property. Starting from an initial error trace, we employ model checking to generate supportive error traces that are utilized to mine important assertions. In the second step, we utilize these assertions for fine-grained design bug localization. The mapping of the assertions leads to specific regions in register transfer level descriptions that are highly probable to be the root cause of the design bug. Specifically, we devise a binning methodology to categorize multiple suspects in different bins that need to be investigated by the design engineer for arriving at the correction for corresponding bugs. Experiments on multiple designs illustrate the efficacy of the proposed methodology in comparison to previous work and state-of-the-art industrial tool.

Design debugging is one of the most important steps in the modern integrated circuits (ICs) development cycle. Simulation-based verification is never sufficient for ensuring design correctness because of its incomplete nature. Formal techniques such as model checking promise to solve this issue through a complete state-space traversal approach. However, because of increasing design complexity, such methods suffer from scalability issues. Guidance-based state-space traversal techniques have been proposed in the past to assist the model checkers in overcoming the complexity bottleneck. Automatically identifying these guidance hints is relatively difficult and requires heuristic-based reasoning procedures. Additionally, to come up with quick fixes during the debug stage, an effective bug localization strategy is needed. In this article, we revisit the paradigm of guidance-based model checking and propose a methodology to improve these guidance generation mechanisms for achieving fine-grained bug localization. In particular, this work proposes a systematic methodology to localize the buggy RTL lines from the erroneous RTL simulation trace. The proposed technique involves the mining of invariant-like assertions from simulation traces. The mined assertions act as probable guidance candidates for the model checking exercise. To identify useful guidance hints from possible ones, we use the Bayesian networks that explore conditional dependence between the various hints at different levels and the target property. These guidance hints are utilized for obtaining possible buggy subregions, which are analyzed via an iterative model checking methodology for fine-grained bug localization. By using the proposed framework, bugs can be localized to within a few lines of RTL description.

Approximate circuits are widely gaining popularity in various fields where error tolerance is applicable. However, striking the right balance between error tolerance and the output quality is a challenging step in the overall design of approximate systems. We propose a systematic approach utilizing Look-Up Table (LUT)-based netlist transformations to achieve approximation while targeting specific error guarantees. Specifically, we employ a SAT-based property checking technique to accommodate worst-case error constraints acting as error guarantees. The proposed methodology involves the formulation of templates to enable the reusability of the technique for different design choices. The analysis comprises of fitness function evaluation based on layout area or the considered error guarantees. We analyze the impact of different parameters on the quality of the output of the resulting approximation and the time taken to obtain them.

Model checking of large designs is a challenging task because of different scalability issues. In this paper, we aim to utilize guided state space traversal to address this issue. However, providing guidance for state space traversal of complex designs is also an equally challenging problem. We adopt a simulation-based strategy combined with Bayesian modelling approach for finding effective guidance hints for state space traversal. A heuristic-based structural dependency of the design yields ineffective guidance hints which need further of filtering. To prune out the ineffective guidance hints, we first generate module-level sub-properties from static analysis of the design. These sub-properties and structural dependency-based guidance hints are analyzed in simulation traces generated from the constrained-random test benches. These conditional occurrence of sub-properties and guidance hints are inputs to a Bayesian model which can then provide us the guidance hints with the highest profitability. With the proposed methodology, we succeed in pruning out the set of unprofitable guidance hints and obtain effective search directions which are then used to assist the model checking procedure. Experiments on two complex designs for different properties show the effectiveness of the proposed methodology in reducing CPU time during model checking.