A Strategy Language for Testing Register Transfer Level Logic

摘要

The development of modern ICs requires a huge investment in RTL verification.This is a reflection of brisk release schedules and the complexity ofcontemporary chip designs. A major bottleneck to reaching verification closurein such designs is the disproportionate effort expended in crafting directedtests; which is necessary to reach those behaviors that other, more automatedtesting methods fail to cover. This paper defines a novel language that can beused to generate targeted stimuli for RTL logic and which mitigates thecomplexities of writing directed tests. The main idea is to treat directedtesting as a meta-reasoning problem about simulation. Our language is bothformalized and prototyped as a proof-search strategy language in rewritinglogic. We illustrate its novel features and practical use with severalexamples.