Synthesizing "Verification Aware" Models: Why and How?

Design-for-verification (DFV) methodology i.e., exporting designer\´s intent to verification tools has been quite effective in improving verification efforts. The authors take one step further in improving the verification efforts, by separating the design optimized for performance, area and power from the design optimized for correctness, thereby reducing the verification burden. The authors propose a new paradigm synthesis-for-verification (SFV) which involves synthesizing "verification-aware" designs that are more suitable for functional verification. SFV methodology should be applied along with DFV methodology to obtain the full benefit of verification efforts. Note, this SFV paradigm requires support only from automated synthesis approaches, e.g. high level synthesis (HLS), and can be easily automated. This is in contrast to DFV methodology, which requires designers\´ reliable insights. As part of SFV methodology, the authors first identify the effect of various design entities on the performance of model checkers. By guiding the use of such entities in existing behavioral synthesis techniques, the authors propose to obtain "verification friendly" models that are relatively easier to model check. The authors demonstrate effectiveness of such a paradigm using existing industry tools and designs