The generalization of Property Directed Reachability (PDR) for the theory QF_BV presented in [1] outperforms the original formulation if the required inductive invariant can be represented efficiently as a set of polytopes. However, many QF_BV model checking instances do not belong in this class and can be solved quickly with the original PDR algorithm. In this paper, we present a hybrid approach which uses both polytopes and Boolean cubes as atomic reasoning units combining the advantages of either homogeneous approach. We discuss theoretic properties of the presented algorithm and report experimental results demonstrating its effectiveness.

We present a novel, sound, and complete algorithm for deciding safety properties in programs with static memory allocation. The new algorithm extends the program verification paradigm using loop invariants presented in [1] with a counterexample guided abstraction refinement (CEGAR) loop [2] where the refinement is achieved by strengthening loop invariants using the QFBV generalization of Property Directed Reachability (PDR) discussed in [3, 4]. We compare the algorithm with other approaches to program verification and report experimental results.

In 2011, property directed reachability (PDR) was proposed as an efficient algorithm to solve hardware model checking problems. Recent experimentation suggests that it outperforms interpolation-based verification, which had been considered the best known algorithm for this purpose for almost a decade. In this work, we present a generalization of PDR to the theory of quantifier free formulae over bitvectors (QF BV), illustrate the new algorithm with representative examples and provide experimental results obtained from experimentation with a prototype implementation.

Modern synthesis flows apply a series of technology independent optimization steps followed by mapping algorithms which bind the optimized network to a specific technology library. As the exact solution of the mapping problem is computationally intractable, algorithms used in practice use heuristic, typically tree-based approaches. The application of these algorithms results in mapped but suboptimal networks. In this work, we present a novel, efficient, and effective optimization algorithm for mapped networks which can be considered a generalization of SAT-sweeping. Our algorithm searches for alternative, more efficient implementations of each net in the network. Candidate support nets for reimplementation are selected using simulation signatures and verified using Boolean satisfiability. We report experimental results on the quality of our algorithm obtained from an implementation of the approach using the logic synthesis system ABC.

Constrained random simulation has been widely adopted in contemporary hardware verification flows. In this methodology, a set of user-specified declarative constraints describe valid input stimuli for the design under test (DUT). A constraint solver produces the simulation input vectors; their generation is interleaved with the actual simulation of the design for these vectors. Besides its distribution, the solver's performance is one of the most critical characteristics that determines the overall verification efficiency. There are no general approaches to hardware acceleration for solving declarative constraints. Current setups for hardware acceleration-based verification combine a software constraint solver running on a general-purpose processor with the hardware-accelerated DUT. This approach suffers from a major efficiency bottleneck caused by the significant performance mismatch between the solver executed in software and the DUT running on an accelerator. In this paper, we present a hardware constraint solver that uses a set of parallel solving units executing Markov chain Monte Carlo sampling. We propose to combine this solver and the DUT on the same device and run both entities hardware-accelerated in order to eliminate the performance mismatch. We discuss the details of the solver architecture and its implementation and report comprehensive results on performance and distribution characteristics as well as experience obtained from our case study where we used our solver to verify a real-world hardware design.

A systematic investigation is presented about the robustness of logic synthesis tools to equivalence-preserving transformations of the input Verilog file. We have developed a framework that: 1) parses Verilog behavioral models into an abstract syntax tree; 2) generates random equivalence-preserving transformations on the syntax tree, and; 3) writes the transformed design back in Verilog format. The original and the transformed Verilog descriptions are then checked for equivalence and synthesized. Results show that average (peak) improvements in area of 2.5% (11%) and length of the critical path of 4% (13%) are achievable. Indeed these figures are comparable to recent advancements in logic synthesis ([17] [8] achieve 4.9% (23%) 5% (24%) improvements area-wise, respectively), signaling a relevant lack of robustness in synthesis tools. This lack of robustness suggests that new synthesis algorithms should be evaluated by measuring the average improvement on several transformed files to assess their real contributions to the quality of the results.

Modern logic synthesis systems apply a sequence of loosely-related function-preserving transformations to gradually improve the circuit with respect to certain criteria such as area, performance, power, etc. For the quality of a complete synthesis run, the application order of the transformations for the individual steps are critical as they can produce vastly different outcomes. In practice, the transformation sequences is encoded in synthesis scripts which are derived manually based on experience and intuition of the tool developer. These scripts are static in the sense that transformations are applied independently of the result of previous transformations or the current status of the design. Despite the importance of obtaining high quality scripts, there are only a few attempts to optimize them. In this paper, we present a novel method to select transformations dynamically during the synthesis run leveraging the theory of Markov Decision Processes. The decision to select a particular transformation is based on transition probabilities, the history of the applied synthesis steps, and expectations for future steps. We report experimental results obtained from an implementation of the approach using the logic synthesis system ABC.