< retour aux publications

Proving and Disproving Assertion Rewrite Rules by Automated Theorem Proving

Auteur(s) : K. Morin-Allory, M. Boulé, D. Borrione, Z. Zilic

Doc. Source: Proc. of IEEE International High Level Design Validation and Test Workshop (HLDVT'08)

Publisher : IEEE

Pages : 56-63

Doi : 10.1109/HLDVT.2008.4695875

Modern assertion languages, such as PSL and SVA, include many constructs that are best handled by rewriting to a small set of base cases. Since previous rewrite attempts have shown that the rules could be quite involved, sometimes counterintuitive, and that they can make a significant difference in the complexity of interpreting assertions, workable procedures for proving the correctness of these rules must be established. In this paper, we outline the methodology for computer-assisted proofs of a set of previously published rewrite rules for PSL properties. We show how to express PSL's syntax and semantics in the PVS theorem prover, and proceed to prove the correctness of a set of thirty rewrite rules. In doing so, we also demonstrate how to circumvent issues with PSL semantics regarding the never and eventually! operators.