Reachability analysis in RTL circuits using k-induction bounded model checking

摘要

In the system on chip design process, functional validation is regarded as one of the main challenges. One sub problem in functional validation is proving the unsatisfiability of certain properties such as the reachability of some assertions or code blocks. In this work, we present a induction-based bounded model checking technique using a Satisfiability Modulo Theories (SMT) solver for proving the unsatisfiability of the properties. After using program slicing to generate small sized SMT formulas, the novel idea of this work utilizes signal domain constraints to make the induction step more powerful. With this approach it is possible to categorize branches that are otherwise impossible to reach with existing state of the art algorithms. We demonstrate the effectiveness of the proposed idea by proving the unreachability of various branches in ITC'99 and the IWLS benchmark circuits which were previously unresolved.