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. We 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. We 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 DFVmethodology, which requires designers' reliable insights. As part of SFV methodology, we 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, we propose to obtain "verification friendly" models that are relatively easier to model check. We demonstrate effectiveness of such a paradigm using existing industry tools and designs.