BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Eugene Goldberg

Eugene Goldberg appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Logic in Computer ScienceDiscrete Mathematics

Catalog footprint

What is connected

9works
2topics
2close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

9 published item(s)

preprint2020arXiv

On Verifying Designs With Incomplete Specification

Incompleteness of a specification $\mathit{Spec}$ creates two problems. First, an implementation $\mathit{Impl}$ of $\mathit{Spec}$ may have some $\mathit{unwanted}$ properties that $\mathit{Spec}$ does not forbid. Second, $\mathit{Impl}$ may break some $\mathit{desired}$ properties that are not in $\mathit{Spec}$. In either case, $\mathit{Spec}$ fails to expose bugs of $\mathit{Impl}$. In an earlier paper, we addressed the first problem above by a technique called Partial Quantifier Elimination (PQE). In contrast to complete QE, in PQE, one takes out of the scope of quantifiers only a small piece of the formula. We used PQE to generate properties of $\mathit{Impl}$ i.e. those $\mathit{consistent}$ with $\mathit{Impl}$. Generation of an unwanted property means that $\mathit{Impl}$ is buggy. In this paper, we address the second problem above by using PQE to generate false properties i.e those that are $\mathit{inconsistent}$ with $\mathit{Impl}$. Such properties are meant to imitate the missing properties of $\mathit{Spec}$ that are not satisfied by $\mathit{Impl}$ (if any). A false property is generated by modifying a piece of a quantified formula describing 'the truth table' of $\mathit{Impl}$ and taking this piece out of the scope of quantifiers. By modifying different pieces of this formula one can generate a "structurally complete" set of false properties. By generating tests detecting false properties of $\mathit{Impl}$ one produces a high quality test set. We apply our approach to verification of combinational and sequential circuits.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Equivalence Checking By Logic Relaxation

We introduce a new framework for Equivalence Checking (EC) of Boolean circuits based on a general technique called Logic Relaxation (LoR). The essence of LoR is to relax the formula to be solved and compute a superset S of the set of new behaviors. Namely, S contains all new satisfying assignments that appeared due to relaxation and does not contain assignments satisfying the original formula. Set S is generated by a procedure called partial quantifier elimination. If all possible bad behaviors are in S, the original formula cannot have them and so the property described by this formula holds. The appeal of EC by LoR is twofold. First, it facilitates generation of powerful inductive proofs. Second, proving inequivalence comes down to checking the presence of some bad behaviors in the relaxed formula i.e. in a simpler version of the original formula. We give some experimental evidence that supports our approach.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Property Checking By Logic Relaxation

We introduce a new framework for Property Checking (PC) of sequential circuits. It is based on a method called Lo-gic Relaxation (LoR). Given a safety property, the LoR method relaxes the transition system at hand, which leads to expanding the set of reachable states. For j-th time frame, the LoR method computes a superset A_j of the set of bad states reachable in j transitions only by the relaxed system. Set A_j is constructed by a technique called partial quantifier elimination. If A_j does not contain a bad state and this state is reachable in j transitions in the relaxed system, it is also reachable in the original system. Hence the property in question does not hold. The appeal of PC by LoR is as follows. An inductive invariant (or a counterexample) generated by LoR is a result of computing the states reachable only in the relaxed system. So, the complexity of PC can be drastically reduced by finding a "faulty" relaxation that is close to the original system. This is analogous to equivalence checking whose complexity strongly depends on how similar the designs to be compared are.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Equivalence Checking and Simulation By Computing Range Reduction

We introduce new methods of equivalence checking and simulation based on Computing Range Reduction (CRR). Given a combinational circuit $N$, the CRR problem is to compute the set of outputs that disappear from the range of $N$ if a set of inputs of $N$ is excluded from consideration. Importantly, in many cases, range reduction can be efficiently found even if computing the entire range of $N$ is infeasible. Solving equivalence checking by CRR facilitates generation of proofs of equivalence that mimic a "cut propagation" approach. A limited version of such an approach has been successfully used by commercial tools. Functional verification of a circuit $N$ by simulation can be viewed as a way to reduce the complexity of computing the range of $N$. Instead of finding the entire range of $N$ and checking if it contains a bad output, such a range is computed only for one input. Simulation by CRR offers an alternative way of coping with the complexity of range computation. The idea is to exclude a subset of inputs of $N$ and compute the range reduction caused by such an exclusion. If the set of disappeared outputs contains a bad one, then $N$ is buggy.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Bug Hunting By Computing Range Reduction

We describe a method of model checking called Computing Range Reduction (CRR). The CRR method is based on derivation of clauses that reduce the set of traces of reachable states in such a way that at least one counterexample remains (if any). These clauses are derived by a technique called Partial Quantifier Elimination (PQE). Given a number n, the CRR method finds a counterexample of length less or equal to n or proves that such a counterexample does not exist. We show experimentally that a PQE-solver we developed earlier can be efficiently applied to derivation of constraining clauses for transition relations of realistic benchmarks. One of the most appealing features of the CRR method is that it can potentially find long counterexamples. This is the area where it can beat model checkers computing reachable states (or their approximations as in IC3) or SAT-based methods of bounded model checking. PQE cannot be efficiently simulated by a SAT-solver. This is important because the current research in model checking is dominated by SAT-based algorithms. The CRR method is a reminder that one should not put all eggs in one basket.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Quantifier Elimination by Dependency Sequents

We consider the problem of existential quantifier elimination for Boolean formulas in Conjunctive Normal Form (CNF). We present a new method for solving this problem called Derivation of Dependency-Sequents (DDS). A Dependency-sequent (D-sequent) is used to record that a set of quantified variables is redundant under a partial assignment. We introduce a resolution-like operation called join that produces a new D-sequent from two existing D-sequents. We also show that DDS is compositional, i.e. if our input formula is a conjunction of independent formulas, DDS automatically recognizes and exploits this information. We introduce an algorithm based on DDS and present experimental results demonstrating its potential.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Verification of Sequential Circuits by Tests-As-Proofs Paradigm

We introduce an algorithm for detection of bugs in sequential circuits. This algorithm is incomplete i.e. its failure to find a bug breaking a property P does not imply that P holds. The appeal of incomplete algorithms is that they scale better than their complete counterparts. However, to make an incomplete algorithm effective one needs to guarantee that the probability of finding a bug is reasonably high. We try to achieve such effectiveness by employing the Test-As-Proofs (TAP) paradigm. In our TAP based approach, a counterexample is built as a sequence of states extracted from proofs that some local variations of property P hold. This increases the probability that a) a representative set of states is examined and that b) the considered states are relevant to property P. We describe an algorithm of test generation based on the TAP paradigm and give preliminary experimental results.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Checking Satisfiability by Dependency Sequents

We introduce a new algorithm for checking satisfiability based on a calculus of Dependency sequents (D-sequents). Given a CNF formula F(X), a D-sequent is a record stating that under a partial assignment a set of variables of X is redundant in formula \exists{X}[F]. The D-sequent calculus is based on operation join that forms a new D-sequent from two existing D-sequents. The new algorithm solves the quantified version of SAT. That is, given a satisfiable formula F, it, in general, does not produce an assignment satisfying F. The new algorithm is called DS-QSAT where DS stands for Dependency Sequent and Q for Quantified. Importantly, a DPLL-like procedure is only a special case of DS-QSAT where a very restricted kind of D-sequents is used. We argue that this restriction a) adversely affects scalability of SAT-solvers and b) is caused by looking for an explicit satisfying assignment rather than just proving satisfiability. We give experimental results substantiating these claims.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Removal of Quantifiers by Elimination of Boundary Points

We consider the problem of elimination of existential quantifiers from a Boolean CNF formula. Our approach is based on the following observation. One can get rid of dependency on a set of variables of a quantified CNF formula F by adding resolvent clauses of F eliminating boundary points. This approach is similar to the method of quantifier elimination described in [9]. The difference of the method described in the present paper is twofold: {\bullet} branching is performed only on quantified variables, {\bullet} an explicit search for boundary points is performed by calls to a SAT-solver Although we published the paper [9] before this one, chrono- logically the method of the present report was developed first. Preliminary presentations of this method were made in [10], [11]. We postponed a publication of this method due to preparation of a patent application [8].

0 citations0 reviewsNo code linkedOpen access