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.

Constrained random simulation is the main workhorse in today 's hardware verification flows. It requires the random generation of input stimuli that obey a set of declaratively specified input constraints, which are then applied to validate given design properties by simulation. The efficiency of the overall flow depends critically on (1) the performance of the constraint solver and (2) the distribution of the generated solutions. In this paper we discuss the overall problem of efficient constraint solving for stimulus generation for mixed Boolean/integer variable domains and propose a new hybrid solver based on Markov-chain Monte Carlo methods with good performance and distribution.

SAT sweeping is a method for simplifying an shape And/Inverter graph (AIG) by systematically merging graph vertices from the inputs towards the outputs using a combination of structural hashing, simulation, and SAT queries. Due to its robustness and efficiency, SAT sweeping provides a solid algorithm for Booleanreasoning in functional verification and logic synthesis. In previous work, SAT sweeping merges two vertices only if they are functionally equivalent. In this paper we present a significant extension of the SAT-sweeping algorithm that exploits local observability don't-cares (ODCs) to increase the number of vertices merged. We use a novel technique to bound the use of ODCs and thus the computational effort to find them, while still finding a large fraction of them. Our reported results based on a set of industrial benchmark circuits demonstrate that ODC-based SAT sweeping results in significantly more graph simplification with great benefit for Boolean reasoning with a moderate increase in computational effort.

Traditional approaches for sequential logic optimization include (1) explicit state-based techniques such as state minimization, (2) structural techniques such as retiming, and (3) methods that exploit sequential don't-cares derived from unreachable states. These approaches optimize a logic circuit as a single component with a single input/output behavior. In this paper we present a novel concept for sequential optimization referred to as temporal decomposition, which distinguishes the logic that initializes the circuit from the logic needed for the behavior after startup. This work was motivated by a recent observation made for bounded property verification: There is a substantial optimization potential for transition relations when the first execution steps are applied as satisfiability don't-cares. This result suggests that current designs include circuitry that is only used during the first few clock periods after reset and could be discarded or disabled after startup. In this paper we describe how temporal decomposition could be applied to treat the logic for startup separately from the remaining circuitry and discuss multiple alternatives to exploit this for an improved implementation.