Papers and talks
E.Goldberg. Property checking by logic relaxation, arXiv:1601.02742 [cs.LO] (A technical report archived at Cornell University Library.)
E.Goldberg. Property checking without invariant generation, arXiv:1602.05829 [cs.LO] (A technical report archived at Cornell University Library.)
E.Goldberg. Equivalence checking by logic relaxation, To appear in Proceedings of FMCAD-16
E.Goldberg. Equivalence checking by logic relaxation, arXiv:1511.01368 [cs.LO] (A technical report archived at Cornell University Library.)
E.Goldberg. Equivalence checking and simulation by computing range reduction, arXiv:1507.02297 [cs.LO] (A technical report archived at Cornell University Library.)
E.Goldberg, P.Manolios. Also available: Partial quantifier elimination , HVC-14, Israel, LNCS-8855, pp.148-165, 2014 the slides of HVC-14 talk
E.Goldberg, P.Manolios. Bug hunting by computing range reduction , arXiv:1408.7039 [cs.LO] (A technical report archived at Cornell University Library.)
E.Goldberg, P.Manolios. Software for quantifier elimination in propositional logic, ICMS-14, Seoul, Korea, LNCS 8592, pp. 291–294, 2014
Quantifier elimination by dependency sequents, Formal Methods in System Design: Vol. 45, No. 2, 2014 pp. 111-143 2013
Also available: Quantifier Elimination Via Clause Redundancy, FMCAD-13, Portland, OR, USA the slides of FMCAD-13 talk
E.Goldberg, M.Jain, P.Manolios. Verification of Sequential Circuits by Tests-As-Proofs Paradigm, arXiv:1308.0583 [cs.LO] (A technical report archived at Cornell University Library.)
Also available: Quantifier Elimination by Dependency Sequents, FMCAD-12, pp. 34-44, Cambridge, UK the slides of FMCAD-12 talk
E.Goldberg, P.Manolios. Checking Satisfiability by Dependency Sequents, arXiv:1207.5014 [cs.LO] (A technical report archived at Cornell University Library.)
E.Goldberg, P.Manolios. Quantifier Elimination by Dependency Sequents
arXiv:1201.5653v4 [cs.LO] (A technical report archived at Cornell University Library.)
E.Goldberg, P.Manolios. Removal of Quantifiers by Elimination of Boundary Points, arXiv:1204.1746v2 [cs.LO] (A technical report archived at Cornell University Library.)
E.Goldberg, P.Manolios. Boundary Points and Resolution, in Advanced Techniques in Logic Synthesis, Optimizations and Applications, Sunil
P. Khatri and Kanupriya Gulati, editors, Springer, 2010, chapter 7,
E.Goldberg, P.Manolios. SAT-solving Based on Boundary Point
Elimination, HVC-2010, Haifa, Israel, LNCS 6504
Also available: Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encoding, TAP-2010, Malaga, Spain, LNCS 6143, pp.101-116
and the slides of TAP-2010 talk
an extended version of this talk given at Intel and IBM.
Boundary Point Elimination: A Path to Structure Aware SAT-solvers. A talk at a Dagstuhl seminar. Here is a link to the seminar page.
Also available: an abstract
Also available: Boundary points and resolution, SAT-2009, Swansea,Wales,UK, LNCS 5584, pp.147-160.
Also available: On bridging simulation and formal verification, VMCAI-2008, San Francisco, USA, LNCS 4905, pp.127-141
Also available: A decision-making procedure for resolution-based SAT-solvers, SAT-2008, Guangzhou, China,LNCS 4996,pp. 119-132. slides
A Resolution Based SAT-solver Operating on Complete Assignments. Journal on Satisfiability, Boolean Modeling and Computation, Vol. 5 (2008), pp. 217-242.
Also available: On complexity of internal and external equivalence checking, DSD-2007,Lubeck, Germany.
E.Goldberg,K.Gulati,S.Khatri. Also available: Toggle Equivalence Preserving (TEP) logic synthesis, DSD-2007,Lubeck, Germany.
Also available: Escaping Local Minima in Logic Synthesis, IWLS-2007,San Diego 2007.
E.Goldberg. Escaping Local Minima in Logic Synthesis (and some other problems of logic synthesis preserving specification).
Technical Report CDNL-TR-2007-0123, January 2007
E.Goldberg. Also available:
On Bridging Simulation and Formal Verification. Technical Report CDNL-TR-2007-0212, February 2007 a short version
Technical Report CDNL-TR-2007-0106, January 2007 Determinization of resolution by an algorithm operating on complete assignments. The technical report above replaces
the previous report on "Determinization of resolution by an algorithm operating on complete assignments".
The new report contains one more table of results and proves that the set of points visited by FI is actually a point image of the resolution proof FI builds.
Note that I use a new definition of the point image that is slightly different from one used in the SAT-2006 paper and in the previous report mentioned above.
BerkMin: A fast and robust Sat-solver, Discrete Applied Mathematics 155 (2007) pp. 1549-1561
Although the preamble of the paper above says that it was submitted in 2006, in reality it had been in the pipeline of DAM for three years since 2003. This paper is different from our DATE-2002 submission in that
every feature of BerkMin is justified experimentally. So you may still find it interesting. I am not allowed to have this paper accessible through my webpage. But I can send it to you by email.
The slides of 3 lectures I gave at the workshop "Algorithms for the SAT-Problem". Humboldt University, Berlin, October 27-29, 2006.
Gives some introduction to SAT and some basic knowledge about resolution proof system. Describes DP and DPLL procedures.
First lecture. Describes the interiors of modern resolution based SAT-solvers.
Second lecture. Introduces formulas with short resolution proofs that can not be found efficiently. Describes testing satisfiability by
computing a stable set of points/clusters.
E.Goldberg. Determinization of resolution by an algorithm operating on complete assignments. SAT-2006,
LNCS 4121, pp.90-95
E.Goldberg,K.Gulati. On Complexity of External and Internal Equivalence Checking. Technical Report CDNL-TR-2006-0105, January 2006
Powerpoint slides of my SAT-2006 talk (short version).
Powerpoint slides of my SAT-2006 talk (long version with experimental results).
E.Goldberg,K.Gulati. Toggle Equivalence Preserving Logic Synthesis. Technical Report CDNL-TR-2005-0912, September 2005
E.Goldberg. Solving satisfiability problem by computing stable sets of points in clusters. Technical Report CDNL-TR-2005-1001, October 2005
E.Goldberg. Equivalence checking of circuits with parameterized specifications. International Conference
on Theory and Applications of Satisfiability Testing, St Andrews, UK, June 19-23,2005,
LNCS 3569, pp.107-121
Powerpoint slides of my SAT-2005 talk.
E.Goldberg. On Equivalence Checking and Logic Synthesis of Circuits with a Common Specification. Proceedings of GLSVLSI, Chicago, April 17-19, 2005,pp.102-107
E.Goldberg. Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points. Annals of Mathematics and Artificial Intelligence, 43 (1-4): 65-89, January 2005
E. Goldberg. What Sat-solvers can and cannot do. A chapter in Advanced Formal
verification. Kluwer Academic Publishers, edited by Rolf Drechsler, 2004, pp.1-43.
E.Goldberg. On equivalence checking and logic synthesis of circuits with a common specification. Technical Report CDNL-TR-2004-1220, August 2004
E.Goldberg. Equivalence checking of dissimilar circuits II. Technical Report CDNL-TR-2004-0830, August 2004
E.Goldberg. Logic synthesis preserving high-level specification. International Workshop on Logic Synthesis, IWLS-2004.
Powerpoint slides of my IWLS-2004 talk.
E.Goldberg, Y.Novikov. Verification of proofs of unsatisfiability for CNF formulas. Design, Automation and Test in Europe. 2003, March 3-7,pp.886-891.
E.Goldberg, Y.Novikov. . How good can a resolution based SAT-solver be? Sixth International Conference
on Theory and Applications of Satisfiability Testing, Portofino, May 5-8,2003, Italy,
LNCS 2919, pp.37-52
E.Goldberg, Y. Novikov. Equivalence Checking of Dissimilar Circuits. International Workshop on Logic and Synthesis, May 28-30, 2003, USA.
E.Goldberg, Y.Novikov. . On complexity
of equivalence checking. Technical Report CDNL-TR-2003-08026, August 2003
E.Goldberg, M.Prasad, R.Brayton. Using Problem Symmetry in Search Based Satisfiability Algorithms , DATE-2002, Paris,pp. 134-141.
E.Goldberg, Y.Novikov. . BerkMin: a Fast and Robust SAT-Solver. DATE-2002,Paris,pp. 142-149
E.Goldberg. . Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points. Proceedigns of Conference on Automated Deduction, CADE
E. Goldberg. Proving Unsatisfiability of CNFs locally. Journal of Automated Reasoning. vol 28:417-434, 2002.
E. Goldberg, M.Prasad, R.K.Brayton. Using SAT for combinational equivalence checking. Proceedings of DATE-2001, pp. 114 -121.
Novikov Y., Goldberg E. An efficient learning procedure for multiple implication checks.
Proceedings of DATE-2001 pp. 127 -133.
Goldberg E. Proving unsatisfiability of CNFs locally. Proceedings of LICS 2001 Workshop on Theory and Applications of Satisfiability Testing.
E.Goldberg,A.Saldanha. . Timing Analysis with Implicitly Specified False Paths. VLSI-2000,pp. 518-522
A few papers written in the past century :-):-)
L.P.Carloni,E.I.Goldberg,T.Villa,R.K.Brayton and A.L.Sangiovanni-Vincentelli. Aura II: Combining Negative Thinking and Branch-and-Bound in Unate Covering Problems. In "VLSI: Systems on a Chip" (L.M. Silveira, R. Reis, S. Devadas editors), Kluwer 1999.
Goldberg E.I., Kukimoto K., Brayton R.K. Combinational verification based on high-level functional specifications. Proceedings of DATE-98, Paris, p.803-807.
Goldberg, E.I., Villa T., Brayton R.K., Sangiovanni-Vincentelli A.L. A fast and robust exact algorithm for face embedding. Proceedings of IEEE International Conference on Computer Aided Design (ICCAD), San Jose, CA, USA, 9-13 Nov. 1997). Los Alamitos, CA, USA: IEEE Comput. Soc, 1997. p. 296-303.
Goldberg, E.I., Carloni L.P., Villa T., Brayton R.K. Negative thinking by incremental problem solving: application to unate
covering. Proceedings of IEEE International Conference on Computer Aided
Design (ICCAD), San Jose, CA, USA, 9-13 Nov. 1997). Los Alamitos, CA, USA:IEEE Comput. Soc, 1997. p. 91-99.