A methodology to take credit for high-level verification during RTL verification

High-level verification and synthesis of SystemC models has become increasingly popular as a means to reduce the high RTL verification cost of today's complex designs. However, the saving derived from performing verification at a higher level of abstraction is largely negated if the RTL then must be completely reverified. We demonstrate how global (system-level) properties may be verified at a behavioral level in a manner that reduces the required RTL verification. Our methodology entails using high-level control models together with semantic stubs for control and data-path refinements. The consequence is that cover goals met during high-level verification are then "virtually" met (in a semantically sound fashion) for RTL verification, and need not be re-established in the RTL. Moreover, it can be significantly more efficient (in terms of required verification cycles) to meet these cover goals at the higher level. This can lead both to less costly verification and earlier debug, providing a better structured, faster and more reliable path to implementation than is possible through conventional RTL verification.