2019

 nach oben zur Jahresübersicht

• Tobias Seufert, Christoph Scholl
  fbPDR: In-depth Combination of Forward and Backward Analysis in Property Directed Reachability
  2019 Conference on Design, Automation and Test in Europe (DATE)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We describe a thoroughly interweaved forward and backward version of PDR/IC3 called fbPDR. Motivated by the complementary strengths of PDR and Reverse PDR and by related work showing the benefits of collaboration between the two, fbPDR lifts the combination to a new level. We lay the theoretical foundations for sharing information represented by learned lemmas between PDR and Reverse PDR and demonstrate the effectiveness of our approach on benchmarks from the Hardware Model Checking Competition.
• Tobias Seufert, Christoph Scholl
  fbPDR: In-depth Combination of Forward and Backward Analysis in Property Directed Reachability (extended abstract)
  2019 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We describe a thoroughly interweaved forward and backward version of PDR/IC3 called fbPDR. Motivated by the com- plementary strengths of PDR and Reverse PDR, fbPDR enables beneficial collaboration between the two and lifts the combination to a new level. We lay the theoretical foundations for sharing information between PDR and Reverse PDR and demonstrate the effectiveness of our approach on benchmarks from the Hardware Model Checking Competition.

2018

 nach oben zur Jahresübersicht

• Tobias Seufert, Christoph Scholl
  Combining PDR and Reverse PDR for Hardware Model Checking
  2018 Conference on Design, Automation and Test in Europe (DATE)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In the last few years IC3 resp. PDR attracted a lot of attention as a SAT-based hardware verification approach without needing to unroll the transition relation as in Bounded Model Checking (BMC). Motivated by different strengths of forward and backward traversal already observed in BDD based model checking and by an exponential complexity gap between original PDR and its reverted counterpart ‘Reverse PDR’ (which starts its analysis with the initial states instead of the unsafe states as in the original PDR), we take a closer look at Reverse PDR and we present a combined forward/backward version of PDR that inherits the advantages of both original and Reverse PDR. Our experimental results on benchmarks from the Hardware Model Checking Competition demonstrate clear benefits of the combined approach.

2017

 nach oben zur Jahresübersicht

• Tobias Seufert, Christoph Scholl
  Sequential Verification Using Reverse PDR
  2017 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In the last few years IC3 resp. PDR made a great stir as a SAT-based hardware verification approach without needing to unroll the transition relation as in Bounded Model Checking (BMC). Motivated by different strengths of forward and backward traversal observed in BDD based model checking, we consider Reverse PDR which starts its analysis with the initial states instead of the unsafe states as in original PDR. We show great benefits of Reverse PDR both by a theoretical and an experimental analysis. Finally, we profit from parallelism offered by modern multi-core processors and use a portfolio approach combining the advantages of Reverse and original PDR.