Improvement of Assertion-Based Verification through the generation of proper test sequences

Assertion-Based Verification (ABV) aims at guaranteeing that designs obey properties, usually expressed under the form of logic and temporal formulae. In dynamic ABV, those properties are checked at runtime (e.g., during simulation). In the context of simulation-based verification, the significance of the selected test sequences is well-known. Moreover, if the validity of properties is also to be checked, test generation is of utmost importance because properties should not be considered as satisfied if they are satisfied vacuously i.e., without having actually been checked. Test sequences must be designed to ensure a good coverage of the property checker´s activation conditions. This paper presents our first results towards a method for the automatic test sequences generation directed by the necessity to avoid vacuous assertion satisfaction.