Summary form only given. Formal verification has become an essential method for design, integration and verification of the emerging design IPs and complex systems-on-chips. Despite the great success in proliferating formal in the industry and making it a great companion to simulation and emulation methods, its full power has not been leveraged yet to address the larger spectrum of applications by non-formal experts. To handle this challenge a major effort is still needed to boost its scalability and usability to cope with the emerging complexity of design under verification. In this talk we discuss a new approach for boosting the productivity of formal verification users using an expert system, which is powered by collective intelligence technology, human-machine interface and self guiding and learning rules. Besides the emerging advancements in model checking and proof strategies, expert system helps to break the formal verification complexity and scalability barriers, and make it affordable for a larger set of users, for yet another major leap in the applications and productivity of formal.

Summary form only given. The electronic design industry has emerged in the recent years to adopt the system-on-chip (SoC) design methodology, where systems become a smart and complex integration of many configurable and reusable intellectual properties (IP) designs such as CPU, GPU, DSP, etc. SoC design methodologies have become common to a wide range of systems, starting from high-end servers, down to tablets, smartphones, Internet-of-things and wearable devices. The aggressive time-to-market and the hard competition add a major challenge to the electronic design companies to deliver high volume, and high quality products. Integration and validation of such designs has become the major challenge. The EDA industry and the academia has continued the innovation pipeline trying to cope with the complexity of such systems however major challenges are still ahead. Formal verification has emerged in the recent years to become a mainstream technology in SoC/IP design and verification methodologies. In the past, the usage of formal verification was limited to a small range of applications and it was mainly for verifying complex protocols, or some tricky logic functionality by formal experts. However in the recent years, we see a rapid adoption of formal, and we see a widespread of formal verification applications for low power design, security, SoC connectivity, configuration status register, and many more. In this talk, we provide an overview of the challenges that we see in designing SoC systems and configurable IPs, and provide some ideas to stimulate the academic research, aiming at increasing the research and innovation in such areas for keeping bridging the emerging gap that the electronic design industry is facing now and will face in the future.

This paper presents a diagnostic test pattern generation (DTPG) framework based upon a Boolean Satisfiability engine. We first propose an enhanced miter-based model for distinguishing fault candidates that can achieve greater efficiency as well as can prove a group of undifferentiable faults. The model can also be used to generate diagnostic tests for distinguishing faults of different fault types. Based on this model, we propose a diagnostic pattern compaction strategy. By exploring "don't cares " at the primary inputs, the number of required diagnostic patterns can be reduced. Experimental results show that the proposed method achieves a greater diagnosis resolution when combined with existing approaches. Also, fewer diagnostic test patterns are needed.

Automatic synchronization (or reset) of sequential synchronous circuits is considered one of the most challenging tasks in the domain of formal sequential equivalence verification of hardware designs. Earlier attempts were based on Binary Decision Diagrams (BDDs) or classical reachability analysis, which by nature suffer from capacity limitations. A previous attempt to attack this problem using non-BDD based techniques was essentially a collection of heuristics aimed at toggling of the latches, and it is not guaranteed that a synchronization sequence will be computed if it exists. In this paper we present a novel approach for computing reset sequences (and reset states) in order to perform sequential hardware equivalence verification between circuit models. This approach is based on the dual-rail modeling of circuits and utilizes efficient SAT-based engines for Bounded Model Checking (BMC). It is implemented in Intel's sequential verification tool, Seqver, and has been proven to be highly successful in proving the equivalence of complex industrial designs. The synchronization method described in this paper can be used in many other CAD applications, including formal property verification, automatic test generation, and power estimation.

Commonly used pattern sources in simulation-based verification include random, guided random, or design verification patterns. Although these patterns may help bring the design to those hard-to-reach states for activating the errors and for propagating them to observation points, they tend to be very long, which complicates the subsequent diagnosis process. As a key step in reducing the overall diagnosis complexity, we propose a method of generating a shorter error-sequence based on a given long error-sequence. We formulate the problem as a satisfiability problem and employ a SAT solver as the underlying engine for this task. By heuristically selecting an intermediate state S/sub i/ which is reachable by the given long sequence, the task of finding the transfer sequence from the initial state to the target state can be divided into two easier tasks - finding a transfer sequence from the initial state to S/sub i/ and one from S/sub i/ to the target state. Our preliminary experimental results on public benchmark circuits show that the proposed method can achieve significant reduction in the length of the error sequences.

We introduce a finer concept of a hardware machine, where the set of post-reboot operation states is explicitly a part of the FSM definition. We formalize an ad-hoc flow of combinational equivalence verification of hardware, the way it was performed over the years in the industry. We define a concept of post-reboot bisimulation, which better suits the hardware machines, and show that a right form of combinational equivalence is in fact a form of post-reboot bisimulation. Further, we show that alignability equivalence is a form of post-reboot bisimulation, too, and the latter is a refinement of alignability in the context of compositional hardware verification. We find that post-reboot bisimulation has important advantages over alignability also in the wider context of formal hardware verification, where equivalence verification is combined with formal property verification and with validation of a reboot sequence. As a result, we propose a more comprehensive, compositional, and fully-formal framework for hardware verification. Our results are extendible to other forms of labeled transition systems and adaptable to other forms of bisimulation used to model and verify complex hardware and software systems

Current algorithms for bounded model checking use SAT methods for checking satisfiability of Boolean formulae. These methods suffer from the potential memory explosion problem. Methods based on the validity of quantified Boolean formulae (QBF) allow an exponentially more succinct representation of formulae to be checked, because no "unrolling" of the transition relation is required. These methods have not been widely used, because of the lack of an efficient decision procedure for QBF. We evaluate the usage of QBF in bounded model checking (BMC), using general-purpose SAT and QBF solvers. We develop a special-purpose decision procedure for QBF used in BMC, and compare our technique with the methods using general-purpose SAT and QBF solvers on real-life industrial benchmarks.

We are interested in sequential hardware equivalence (or alignability equivalence) verification of synchronous sequential circuits as stated in C. Pixley (1992). To cope with large industrial designs, the circuits must be divided into smaller subcircuits and verified separately. Furthermore, in order to succeed in verifying the subcircuits, design constraints must be added to the subcircuits. These constraints mimic "essential" behavior of the subcircuit environment. In this work, we extend the classical alignability theory in the presence of design constraints, and prove a compositionality result allowing inferring alignability of the circuits from alignability of the subcircuits. As a result, we build a divide and conquer framework for alignability verification. This framework is successfully used on Intel designs.

The developments of efficient SAT solvers have attracted tremendous research interest in recent years. The merits of these solvers are often compared in terms of their performance based upon a wide spread of benchmarks. In this paper, we extend an earlier-proposed solver design concept called (SCGL) Signal Correlation Guided Learning that is ATPG-based into a family of heuristics. Along with this SCGL family of heuristics, we classify benchmark examples according to their performance using the SCGL heuristics. With this study, we identify the class of problems that are uniquely suitable to be solved by using the SCGL approach. In particular, for solving difficult circuit-based problems at INTEL, our SCGL-based ATPG solver is able to achieve at least an order of magnitude speedup over the state-of-the-art SAT solvers. Our conclusion is that SCGL is an unique solver design concept that can complement heuristics proposed by others for solving circuit-oriented difficult problems.

Design automation problems can often be encoded in propositional logic, and solved by applying propositional logic proof methods. Unfortunately, there exists no single proof method with adequate performance for all problems of interest. It is, therefore, critical to be able to combine different approaches, and to quickly be able to test how different compositions affect overall performance. In this paper, we present a proof engine framework where individual methods are viewed as strategies-functions between different proof states. By defining our proof engine in such a way that we can compose strategies to form new, more powerful, strategies we achieve synergistic effects between the individual methods. Unlike previous approaches, our framework is flexible enough to allow users to quickly come up with specially tailored composite analyses for problems from any of the different subdomains of design automation. We show how several known analyses for solving design automation problems encoded in propositional logic can be integrated as base strategies in our framework. As a proof-of-concept, and to demonstrate the power inherent in the framework, we also present experimental results that show the performance of two default composite strategies that we have developed using the framework over a period of several years. These strategies are often one to two magnitudes faster when compared with binary decision diagram-based techniques and search-based satisfiability solvers such as ZCHAFF. The introduction of the framework was the key facilitator in the development of these default strategies.

There are many approaches available for solving combinational design automation problems encoded as tautology or satisfiability checks. Unfortunately there exists no single analysis that gives adequate performance for all problems of interest, and it is therefore critical to be able to combine approaches.In this paper, we present a proof engine framework where individual analyses are viewed as strategies---functions between different proof states. By defining our proof engine in such a way that we can compose strategies to form new, more powerful, strategies we achieve synergistic effects between the individual methods. The resulting framework has enabled us to develop a small set of powerful composite default strategies.We describe several strategies and their interplay; one of the strategies, variable instantiation, is new. The strength of our approach is demonstrated with experimental results showing that our default strategies can achieve up to several magnitudes of speed-up compared to BDD-based techniques and search-based satisfiability solvers such as ZChaff.

In this paper we present an advanced functional extraction tool for automatic generation of high-level RTL from switch-level circuit netlist representation. The tool is called FEV-Extract and is part of a comprehensive Formal Equivalence Verification (FEV) system developed at Intel to verify modern microprocessor designs. FEV-Extract employs a powerful hierarchical analysis procedure, and advanced and generic algorithms for automatic recognition of logical primitives, to cope with variety of circuit design styles and their complexity. Logic equations are then extracted to generate a behavioral RTL model described in industrial standard HDL languages, to be used in the formal equivalence verification, logic simulation, synthesis and testability flows.