< retour aux publications

Extraction of missing formal assumptions in under-constrained designs

Auteur(s) : G. Plassan, K. Morin-Allory, D. Borrione

Doc. Source: 15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2017)

Publisher : ACM, NY, USA

Pages : 94-103

Doi : 10.1145/3127041.3127046

In the context of the formal functional verification of RTL designs, experience shows that a false failure is often observed. Most of the time, this failure is cause d by an under-constrained model. The analysis of the root cause for the verification error and the creation of missing constraints are a significant time burden. In this paper, we present a methodology to automatically infer these missing constraints: Constraint Extraction from Counter-Examples (CExtract). First, multiple counter-examples are generated for the same property. Then, potential constraints are mined from the counterexamples, and filtered to provide a limited number of assumptions for the user for review.