This chapter analyses the problem of formally checking whether two design specifications are functionally equivalent. In general, there is a wide range of possible definitions of functional equivalence covering comparisons between different levels of abstraction and varying granularity of timing details. The chapter focuses on the aforementioned machine equivalence, which in practical design flows is the most established application of functionally comparing two design specifications. It examines the role of equivalence checking in the design cycle and reviews the major approaches and techniques applied to this problem. The key to the practical success of formal equivalence checking is the separation of function and timing concerns in contemporary design flows. The need for formal equivalence checking methods was triggered by the necessity to use multiple models in hardware design flows. In the initial methodology which predated automatic logic synthesis, the actual logic implementation was designed independently and verified against the register transfer level by formal equivalence checking.

Summary form only given, as follows. A record of the panel discussion was not made available for publication as part of the conference proceedings. In the wake of on-going cyber-attacks against users (WannaCry), companies (Dyn), and countries (Petya), secure development is becoming increasingly important. Although these attacks are all recent, members of this panel are pioneers who anticipated these attacks. In some cases they are seeking to bring new tools and technologies to defend against these attacks, and in others they have already brought some of the best available tools to market. This panel will explore the process of finding a great idea that will matter, getting some seed funding to build a product, getting help from an incubator, and bringing that product to market.

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 QF_BV 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.

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.

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.

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.

Conventional logic synthesis flows are composed of three separate phases: technology independent optimization, technology mapping, and technology dependent optimization. A fundamental problem with such a three-phased approach is that the global logic structure is decided during the first phase without any knowledge of the actual technology parameters considered during later phases. Although technology dependent optimization algorithms perform some limited logic restructuring, they cannot recover from fundamental mistakes made during the first phase, which often results in non-satisfiable solutions. In this paper, we present a method for integrating the three synthesis phases using an annealing algorithm as optimization framework. The annealing-based search is driven by a complex objective function, combining both technology independent as well as technology dependent optimization criteria. Our experimental results shown that, on average, the presented approach can improve the area and delay of circuits optimized with script rugged of SIS by 11.2% and 32.5% respectively.

Cloud computing is used to describe a collection of (remote) data centers (the hardware and the software) and applications delivered from them as a service (SaaS, Software as a Service). Its success is driven by the cost-effective on-demand availability of large, scalable amounts of computing resources. The cloud has become an established paradigm for many enterprise and consumer applications such as email, web servers, productivity applications, customer relationship management, etc. However, in IC design its success is still limited.This panel will discuss the real and perceived hurdles that currently prevent a broad adoption of cloud computing in IC design, and several scenarios on how this could happen.