Liste filtern : Jahre: 2019 |
2018 |
2017 | alle anzeigen nach oben zur Jahresübersicht Tobias Seufert, Christoph SchollfbPDR: 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 SchollfbPDR: 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. nach oben zur Jahresübersicht Tobias Seufert, Christoph SchollCombining 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. nach oben zur Jahresübersicht Tobias Seufert, Christoph SchollSequential 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.