|
Randal E Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 100(8):677–691, 1986. João P Marques-Silva and Karem A Sakallah. Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506–521, 1999. Hantao Zhang. Sato: An efficient propositional prover. In International Conference on Automated Deduction, pages 272–275. Springer, 1997. Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 38th annual Design Automation Conference, pages 530–535, 2001. E Goldberg and Y Novikov. Berkmin: A fast and robust sat-solver. In Proceedings 2002 Design, Automation and Test in Europe Conference and Exhibition, pages 142–149. IEEE, 2002. Niklas Eén and Niklas Sörensson. An extensible sat-solver. In International conference on theory and applications of satisfiability testing, pages 502–518. Springer, 2003. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern sat solvers. In Twenty-first International Joint Conference on Artificial Intelligence, 2009. Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without bdds. In International conference on tools and algorithms for the construction and analysis of systems, pages 193–207. Springer, 1999. Mary Sheeran, Satnam Singh, and Gunnar Stålmarck. Checking safety properties using induction and a sat-solver. In International conference on formal methods in computer-aided design, pages 127–144. Springer, 2000. Niklas Eén and Niklas Sörensson. Temporal induction by incremental sat solving. Electronic Notes in Theoretical Computer Science, 89(4):543–560, 2003. Kenneth L McMillan. Interpolation and sat-based model checking. In International Conference on Computer Aided Verification, pages 1–13. Springer, 2003. William Craig. Linear reasoning. a new form of the herbrand-gentzen theorem. The Journal of Symbolic Logic, 22(3):250–268, 1957. Yakir Vizel and Orna Grumberg. Interpolation-sequence based model checking. In 2009 Formal Methods in Computer-Aided Design, pages 1–8. IEEE, 2009. Vijay D’Silva, Daniel Kroening, Mitra Purandare, and Georg Weissenbacher. Interpolant strength. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 129–145. Springer, 2010. Simone Fulvio Rollini, Ondrej Sery, and Natasha Sharygina. Leveraging interpolant strength in model checking. In International Conference on Computer Aided Verification, pages 193–209. Springer, 2012. Aaron R Bradley. Sat-based model checking without unrolling. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 70–87. Springer, 2011. Aaron R Bradley and Zohar Manna. Checking safety by inductive generalization of counterexamples to induction. In Formal Methods in Computer Aided Design (FMCAD’07), pages 173–180. IEEE, 2007. Niklas Een, Alan Mishchenko, and Robert Brayton. Efficient implementation of property directed reachability. In 2011 Formal Methods in Computer-Aided Design (FMCAD), pages 125–134. IEEE, 2011. Hong-Syun Jiang and Chung-Yang (Ric) Huang. Enhancing property directed reachability technique through cube analysis. Master Thesis, National Taiwan University, 2015. Kuan Fan, Ming-Jen Yang, and Chung-Yang Huang. Automatic abstraction refinement of tr for pdr. In 2016 21st Asia and South Pacific Design Automation Conference (ASP-DAC), pages 121–126. IEEE, 2016. Ming-Jen Yang and Chung-Yang (Ric) Huang. Improving property directed reachability with temporal decomposition. Master Thesis, National Taiwan University, 2016. Cheng-Han Yang and Chung-Yang (Ric) Huang. Improving property directed reachability using dynamic timeframe expansion. Master Thesis, National Taiwan University, 2017. Shih-Yu Chuang and Chung-Yang (Ric) Huang. Property directed reachability with interpolation refinement. Master Thesis, National Taiwan University, 2019. Alexander Ivrii and Arie Gurfinkel. Pushing to the top. In 2015 Formal Methods in Computer-Aided Design (FMCAD), pages 65–72. IEEE, 2015. Ken L McMillan. Applying sat methods in unbounded symbolic model checking. In International Conference on Computer Aided Verification, pages 250–264. Springer, 2002. Armin Biere. The aiger and-inverter graph (aig) format version 20071012. FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr, 69:4040, 2007. Armin Biere, Keijo Heljanko, and Siert Wieringa. Aiger 1.9 and beyond. Available at fmv. jku. at/hwmcc11/beyond1. pdf, 2011. Alan Mishchenko, Satrajit Chatterjee, Roland Jiang, and Robert K Brayton. Fraigs: A unifying representation for logic synthesis and verification. Technical report, ERL Technical Report, 2005. Robert Brummayer and Armin Biere. Local two-level and-inverter graph minimization without blowup. Proc. MEMICS, 6:32–38, 2006. Jordi Cortadella. Timing-driven logic bi-decomposition. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 22(6):675–685, 2003. Niklas Eén and Armin Biere. Effective preprocessing in sat through variable and clause elimination. In International conference on theory and applications of satisfiability testing, pages 61–75. Springer, 2005. Niklas Eén and Niklas Sörensson. The MiniSat Page. http://minisat.se/. Gilles Audemard and Laurent Simon. Glucose’s home page. https://www.labri.fr/perso/lsimon/glucose/. G. S. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic. Leningrad:Steklov Math. Institute, 1968. David A Plaisted and Steven Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2(3):293–304, 1986. Miroslav N Velev. Efficient translation of boolean formulas to cnf in formal verification of microprocessors. In ASP-DAC 2004: Asia and South Pacific Design Automation Conference 2004 (IEEE Cat. No. 04EX753), pages 310–315. IEEE, 2004. Daniel Sheridan. The optimality of a fast cnf conversion and its use with sat. SAT, 2, 2004. Niklas Een, Alan Mishchenko, and Niklas Sörensson. Applying logic synthesis for speeding up sat. In International Conference on Theory and Applications of Satisfiability Testing, pages 272–286. Springer, 2007. Alberto Griggio and Marco Roveri. Comparing different variants of the ic3 algorithm for hardware model checking. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 35(6):1026–1039, 2015. Robert Brayton and Alan Mishchenko. Abc: An academic industrial-strength verification tool. In International Conference on Computer Aided Verification, pages 24–40. Springer, 2010. Cheng-Yin Wu and Chung-Yang (Ric) Huang. V3: An extensible framework for hardware verification. https://github.com/chengyinwe/V3. Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. https://people.eecs.berkeley.edu/~alanmi/abc/.
|