Improving Termination of MDG-Based Abstract State Enumeration via Term Schematization
S. Renault, E. Cerny · Electronic Notes in Theoretical Computer Science · 2001
The MDG approach for hardware verification was recently proposed to overcome some limitations of traditional ROBDD-based methods of automated verification. One of its weakness, however, is that it may suffer from the non termination of the state enumeration procedure. In this paper, we exploit an idea recently proposed of using term schematization to address this problem. We propose a strategy to direct the introduction of schematized terms in the state enumeration procedure. We show that for certain cases of non termination, it significantly improves over the previously known approaches.