International Business Machines Corporation

Tatyana Veksler

Rachel Tzoref-Brill

Alexander Ivrii

Itai Segall

Oded Fuhrmann

Sitvanit Ruah

Ohad Shacham

Sharon Keidar-Barner

Ziv Nevo

Cynthia Rae Eisner

Shiri Moran

Dmitry Pidan

Sharon Keidar Barner

Method, apparatus and product for symbolic execution of alternative branches. The method comprising reaching, during symbolic execution of a Control Flow Graph (CFG) of a program, a branching node in the CFG with a first symbolic state, wherein the branching has at least a first branch and a second branch, wherein the first and second branches end at a joining node in the CFG. The method further comprises symbolically executing the first branch using the first symbolic state so as to determine a second symbolic state. The method further comprises symbolically executing the second branch using the second symbolic state so as to determine a third symbolic state. Accordingly, the third symbolic state is based on sequential symbolic execution of alternative branches.

Symbolic execution of alternative branches

Obtaining a functional coverage model of a System Under Test (SUT) defining all functional coverage tasks of the SUT, wherein the functional coverage model defining a test-space with respect to functional attributes; obtaining a set of covered functional coverage tasks; encoding a covered Binary Decision Diagram (BDD) to represent the set of covered functional coverage tasks within the test-space; and manipulating the covered BDD to identify one or more coverage holes, wherein a coverage hole defines a set of coverage tasks in the test-space, all having a same combination of values to a subset of the functional attributes, that are not covered by the set of covered functional coverage task.

BDD-based functional coverage analysis

A computer-implemented method, apparatus, and computer program product for assisting in dynamic verification of a System Under Test (SUT). The method comprising obtaining a set of functional attributes and associated domains with respect to a System Under Test (SUT), and obtaining a set of restrictions over the functional attributes and associated domains. The method comprising encoding a Binary Decision Diagram (BDD) to represent a Cartesian cross-product test-space of all possible combinations of values of the functional attributes excluding combinations that are restricted by the set of restrictions, whereby the BDD symbolically represents the Cartesian cross-product test-space. The method may further comprise analyzing the Cartesian cross-product test-space by manipulating the BDD so as to assist in performing dynamic verification of the SUT.

BDD-based functional modeling

An UNSAT core may be reused during iterations of a bounded model checking process. When increasing the bound, signals corresponding to signals within the UNSAT core may be used to represent the functionality of the model during cycles between the original bound and the increased bound. In case, consecutive unsatisfiability is determined in respect to different bounds, the same UNSAT core may be reused instead of computing a new UNSAT core.

Proof based bounded model checking

A computerized system comprising: a processor; a first interface configured to obtain a constraint; a second interface configured to obtain a first model, wherein the first model is configured to be utilized in model checking, and the first model, when constrained by the constraint, comprises at least one finite path; and a finite path removal module implemented in the processor and configured to generate a second model equivalent to the first model obtained by said second interface, wherein the second model excludes a portion of the at least one finite path, and the second model is configured to be utilized in model checking.

Model generation based on a constraint and an initial model

Device, system and method of efficient automata-based implementation of liveness properties for formal verification. A system according to embodiments of the invention includes a property transformation module to receive an assume verification directive on a liveness property in a property specification language, and to translate the property a fairness statement that uses a deterministic automaton. The deterministic automaton is exponential in the size of the input property. The assume verification directive may be transformed into a strong suffix implication in the property specification language.

Growing community of inventors

Zichron Yaakov, Israel

Tatyana Veksler