Files in this item



application/pdfkatelman_strategy_language_TR_2009.pdf (229kB)


Title:A Strategy Language for Testing Register Transfer Level Logic
Author(s):Katelman, Michael; Meseguer, José
Formal Methods
Abstract:The development of modern ICs requires a huge investment in RTL verification. This is a reflection of brisk release schedules and the complexity of contemporary chip designs. A major bottleneck to reaching verification closure in such designs is the disproportionate effort expended in crafting directed tests; which is necessary to reach those behaviors that other, more automated testing methods fail to cover. This paper defines a novel language that can be used to generate targeted stimuli for RTL logic and which mitigates the complexities of writing directed tests. The main idea is to treat directed testing as a meta-reasoning problem about simulation. Our language is both formalized and prototyped as a proof-search strategy language in rewriting logic. We illustrate its novel features and practical use with several examples.
Issue Date:2009-06-03
Genre:Technical Report
Publication Status:published or submitted for publication
Date Available in IDEALS:2009-06-03

This item appears in the following Collection(s)

Item Statistics