As I start my second two-year term (2017–2018) as the Editor-in-Chief (EIC) of the IEEE Transactions on Very Large Scale Integration Systems (TVLSI), I wish the TVLSI readership a very happy new year and continued professional success. It gives me great pleasure to report on the state of the journal and our performance metrics. Over the past two years, TVLSI has seen a healthy increase in the number of submissions—from 687 in 2014 to 770 in 2015, and at the time of writing of this editorial, we are at 760 submissions for 2016. We expect the number of submissions for 2016 to cross 800 before the end of the year. TVLSI, therefore, continues to be the premier archival journal for university researchers and industry practitioners in the broad area of VLSI system design.

We present parallel algorithms for Binary Decision Diagram (BDD) manipulation optimized for efficient execution on Graphics Processing Units (GPUs). Compared to a sequential CPU-based BDD package with the same capabilities, our GPU implementation achieves at least 5 orders of magnitude speedup. To the best of our knowledge, this is the first work on using GPUs to accelerate a BDD package.

We present a method for exploiting symmetry-breaking constraints in modular schemes for constructing equivalent Boolean encodings of cardinality constraints. These techniques result in speedup in automated debugging of complex VLIW processors in formal verification by Correspondence Checking and efficient translation to Boolean Satisfiability (SAT).

Solving Constraint Satisfaction Problems (CSPs) through Boolean Satisfiability (SAT) requires suitable encodings for translating CSPs to equivalent SAT instances that can not only be efficiently generated, but also efficiently solved by SAT solvers. In this paper we investigate hierarchical and hybrid encodings, as proposed by Velev, namely a previously studied log-direct encoding, and a new combination, the log-order encoding. Experiments on different domain problems with these hierarchical encodings demonstrate their significant promise in practice. Our experiments show that the log-direct encoding significantly outperforms the direct encoding (typically by one or two orders of magnitude) taking advantage not only of the more concise representation, but also of the better capability of the log-direct encoding to represent interval variables. We also show that the log-order encoding is competitive with the order encoding, although more studies are required to understand the tradeoff between the fewer variables and longer clauses in the former, when expressing complex CSP constraints.

We propose a novel method for error diagnosis of pipelined microprocessors that allows us to exploit Positive Equality in Correspondence Checking. We also present static CNF variable ordering heuristics that dramatically reduce the solution space during the debugging. Experimental results indicate speedup of up to 2 orders of magnitude relative to previous approaches when applying the method to automated debugging in formal verification of complex pipelined DSPs.

We present a method for automatic formal verification of Digital Signal Processors (DSPs) that have VLIW architecture and reconfigurable functional units optimized for accelerating Software Defined Radio (SDR) applications to be used for future space communications by NASA. The formal verification was done with the highly automatic method of Correspondence Checking by exploiting the property of Positive Equality that allows a dramatic simplification of the solution space and many orders of magnitude speedup. The formal verification of a complex reconfigurable DSP took approximately 10 minutes of CPU time on a single workstation, when using our industrial-strength tool flow.

We present highly automatic techniques for formal verification of pipelined microprocessors with hardware support for multithreading. The processors are modeled at a high level of abstraction, using a subset of Verilog, in a way that allows us to exploit the property of Positive Equality that results in significant simplifications of the solution space, and orders of magnitude speedup relative to previous methods. We propose abstraction techniques that produce at least 3 orders of magnitude speedup, which is increasing with the number of threads implemented in a pipelined processor. To the best of our knowledge, this is the first work on automatic formal verification of pipelined processors with hardware support for multithreading.

With decreasing transistor sizes, the susceptibility of digital circuits to soft errors will increase. Thus, the need to efficiently evaluate the robustness of a gate-level circuit to multiple simultaneous soft errors. We compare the efficiency of various CNF schemes for encoding of cardinality constraints, which control the number of simultaneously injected soft errors in a gate-level circuit, when the robustness of the circuit is computed with SAT-based formal methods.

Presented is a method for debugging of pipelined processors in their formal verification with the highly automatic and scalable approach of Correspondence Checking, where a pipelined/superscalar/VLIW implementation is compared against a non-pipelined specification via an inductive correctness criterion based on symbolic simulation in a way that guarantees the correctness of the implementation for all possible execution scenarios. The benefit from the proposed method increases with the complexity of the processor under formal verification. For a 12-stage VLIW processor that imitates the Intel Itanium in many features, the method reduced the size of the EUFM correctness formulas from buggy processors by up to an order of magnitude, the number of Boolean variables in the equivalent propositional correctness formulas and the number of 1s in the counterexample traces by up to 2 orders of magnitude, and resulted in an average speedup in detecting the bugs of 2 orders of magnitude, thus increasing the productivity of the processor designers.

We compare 12 new encodings for representing of FPGA detailed routing problems as equivalent Boolean satisfiability (SAT) problems against the only 2 previously used encodings. We also consider two symmetry-breaking heuristics. Compared to other methods for FPGA detailed routing, SAT-based approaches have the advantage that they can prove the unroutability of a global routing for a particular number of tracks per channel, and that they consider all nets simultaneously. The experiments were run on the standard MCNC benchmarks. The combination of one new encoding with a new symmetry-breaking heuristic resulted in speedup of 3 orders of magnitude or 1,139x of the total execution time on the collection of benchmarks, when proving the unroutability of FPGA global routings. The maximum obtained speedup was 9,499x on an individual benchmark. On the other hand, most of the encodings had comparable and very efficient performance when finding solutions for configurations that were routable. The availability of many SAT encodings, that can each be combined with various symmetry-breaking heuristics, opens the possibility to design portfolios of parallel strategies - each a combination of a SAT encoding and a symmetry- breaking heuristic - that can be run in parallel on different cores of a multicore CPU in order to reduce the solution time, with the rest of the runs terminated as soon as one of them returns an answer. We found that a portfolio of three particular parallel strategies produced additional speedup of more than 2x.

Many important EDA problems can be formulated as graph coloring, which is a class of the Constraint Satisfaction Problem (CSP). This paper makes three contributions First, we define new encodings for representing CSPs as equivalent Boolean Satisfiability (SAT) problems: (1) a generalization of the log encoding by using ITE trees to select the domain values of a CSP variable, so that only conflict clauses are required; and (2) a simplified direct encoding, derived from the direct encoding (Where each domain value of a CSP variable is indexed by a unique Boolean variable) by omitting one of the Boolean variables and the at-least-one clause. Second, we propose the use of hierarchical encodings that combine several simple encodings to index the domain values of CSP variables, in order to produce SAT formulas that depend on fewer Boolean variables and are easier to solve. Third, we study schemes for static ordering of the Boolean variables in a Conjunctive Normal Form (CNF) representation of a CSP, based on the structure of the CSP graph, such that the resulting variable order is used for the decisions made by a SAT solver when evaluating the CNF. We compare 12 previously known SAT encodings for CSP with the two new encodings, as well as with 10 hybrid encodings. With symmetry-breaking constraints enforced, static variable ordering produced up to 2 orders of magnitude speedup. Additionally exploiting hierarchical encodings resulted in another order of magnitude speedup.

Compared are seven schemes for encoding unobservability of logic blocks in Boolean-to-CNF translation. Four of the schemes are based on merging of logic blocks with adjacent gates toward the primary output. Two are based on using CNF unobservability variables to encode the unobservability of logic blocks. Also explored is a hybrid scheme. Encoding the unobservability of logic blocks accelerated the SAT-solving of Boolean formulas from formal verification of complex micro-processors, while allowing us to use a conventional CNF-based SAT-solver. On unsatisfiable CNF formulas, best was the strategy of merging logic blocks with adjacent gates on the only path from the block output to the primary output, with a resulting speedup of up to 16x for CNF formulas with hundreds of thousands of variables, millions of clauses, and tens of millions of literals. Furthermore, the speedup is relative to an already very efficient Boolean-to-CNF translation. On satisfiable CNF formulas, best was the strategy of merging logic blocks with leaf gates and with adjacent gates on the only path to the primary output, as well as exploiting the polarity of gates and logic blocks to reduce the number of their clauses. The presented optimizations are general and applicable to other classes of Boolean formulas.

The paper presents a method for translating Boolean circuits to CNF by identifying trees of ITE operators, where each ITE has fanout count of 1, and representing every such tree with a single set of equivalent CNF clauses without intermediate variables for ITE outputs, except for the tree output. This not only eliminates intermediate variables, but also reduces the number of clauses, compared to conventional translation to CNF, where each ITE is assigned an output variable and is represented with a separate set of clauses. Other gates with fanout count of 1 are similarly merged with their fanout gate to generate a single set of equivalent clauses. This translation to CNF was implemented in a decision procedure for the logic of equality with uninterpreted functions and memories (EUFM), and was applied to formulas from formal verification of microprocessors. To increase the number of ITE-trees in the Boolean formulas, the decision procedure was optimized to preserve the ITE-tree structure of arguments to equality comparisons. In conventional translation to CNF with the unoptimized decision procedure, the benchmark formulas require up to hundreds of thousands of CNF variables and millions of clauses. The best translation strategy reduced the CNF variables by up to 8x; the clauses by up to 17x; the SAT-solver decisions by up to 79x; the SAT-solver conflicts by up to 96x; and accelerated the SAT solving by up to 420x.

Presented is a method for formal verification of pipelined processors with long instruction queues. The execution engine and the fetch engine (where the instruction queue is) are formally verified separately, after abstracting the other engine with a non-deterministic FSM derived from the high-level specification of that engine. Without the presented method, the monolithic formal verification of 9-stage, 9-wide VLIW processors--implementing many realistic and speculative features inspired by the Intel Itanium--scaled for models with 5 instruction-queue entries, but ran out of memory if the instruction queue was longer. The presented method resulted in 2 orders of magnitude speedup for the processor with 5 instruction-queue entries, and enabled scaling for designs with 64 instruction-queue entries.

Different methods are compared for the evaluation of formulas expressing microprocessor correctness in the logic of equality with uninterpreted functions and memories (EUFM) by translation to prepositional logic, given recently developed efficient Boolean-to-CNF translations, in order to identify the best overall translation strategy from EUFM to CNF. The translation from EUFM to propositional logic is done by exploiting the property of positive equality, allowing us to treat most of the abstract word-level values as distinct constants while performing complete formal verification. For EUFM formulas from correct microprocessors, the best translation was by using the e/sub ij/ encoding of g-equations (dual-polarity equations), the nested-ITE scheme for the elimination of uninterpreted predicates, preserving the ITE-tree structure of equation arguments, and Boolean-to-CNF translation by encoding the unobservability of logic blocks by merging them with adjacent gates on the only path to the primary output. For EUFM formulas from buggy microprocessors, the best translation was by using the e/sub ij/ encoding of g-equations, the Ackermann scheme for the elimination of uninterpreted predicates, preserving the ITE-tree structure of equation arguments, and Boolean-to-CNF translation by applying optimizations to reduce the number of clauses - merging of ITE-trees with one level of their AND/OR leaves, and exploiting the polarity of gates and logic blocks to reduce the number of their clauses.

The paper presents a collection of 93 different bugs, detected in formal verification of 65 student designs that include: 1) singleissue pipelined DLX processors; 2) extensions with exceptions and branch prediction; and 3) dual-issue superscalar implementations. The processors were described in a high-level HDL, and were formally verified with an automatic tool flow. The bugs are analyzed and classified, and can be used in research on microprocessor testing.

We present the formal verification of an Intel Xscale processor model. The Xscale is a superpipelined RISC processor with 7-stage integer, 8-stage memory, and variable-latency multiply-and-accumulate execution pipelines. The processor uses scoreboarding to track data dependencies, and implements both precise and imprecise exceptions. Such set of features had not been modeled and formally verified previously. The formal verification was done with an automatic tool flow that consists of the term-level symbolic simulator TLSim, the decision procedure EVC, and an efficient SAT-checker.

Rewriting rules and positive equality are combined in an automatic way in order to formally verify out-of-order processors that have a Reorder Buffer and can issue/retire multiple instructions per clock cycle. Only register-register instructions are implemented, and can be executed out-of-order as soon as their data operands can be either read from the Register File, or forwarded as results of instructions ahead in program order in the Reorder Buffer. The verification is based on the Burch and Dill correctness criterion. Rewriting rules are used to prove the correct execution of instructions that are initially in the Reorder Buffer and to remove them from the correctness formula. Positive Equality is then employed to prove the correct execution of newly fetched instructions. The rewriting rules resulted in up to 5 orders of magnitude speedup, compared to using Positive Equality alone. That made it possible to formally verify processors with up to 1,500 instructions in the Reorder Buffer and issue/retire widths of up to 128 instructions per clock cycle.

We consider a variant of the Boolean satisfiability problem where a subset ε of the propositional variables appearing in formula F sat encode a symmetric, transitive, binary relation over N elements. Each of these relational variables, e i,j , for 1 ≤ i < j ≤ N , expresses whether or not the relation holds between elements i and j . The task is to either find a satisfying assignment to F sat that also satisfies all transitivity constraints over the relational variables (e.g., e 1,2 ∧ e 2,3 ⇒ e 1,3 ), or to prove that no such assignment exists. Solving this satisfiability problem is the final and most difficult step in our decision procedure for a logic of equality with uninterpreted functions. This procedure forms the core of our tool for verifying pipelined microprocessors.To use a conventional Boolean satisfiability checker, we augment the set of clauses expressing F sat with clauses expressing the transitivity constraints. We consider methods to reduce the number of such clauses based on the sparse structure of the relational variables.To use Ordered Binary Decision Diagrams (OBDDs), we show that for some sets ε, the OBDD representation of the transitivity constraints has exponential size for all possible variable orderings. By considering only those relational variables that occur in the OBDD representation of F sat , our experiments show that we can readily construct an OBDD representation of the relevant transitivity constraints and thus solve the constrained satisfiability problem.

We compare SAT-checkers and decision diagrams on the evalua-tion of Boolean formulas produced in the formal verification of both correct and buggy versions of superscalar and VLIW micro-processors. We identify one SAT-checker that significantly out-performs the rest. We evaluate ways to enhance its performance by variations in the generation of the Boolean correctness formu-las. We reassess optimizations previously used to speed up the formal verification and probe future challenges.

The logic of Equality with Uninterpreted Functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic. By reducing formulas in this logic to propositional formulas, we can apply Boolean methods such as ordered Binary Decision Diagrams (BDDs) and Boolean satisfiability checkers to perform the verification. We can exploit characteristics of the formulas describing the verification conditions to greatly simplfy the propostional formulas generated. We identify a class of terms we call “p-terms” for which equality comparisons can only be used in monotonically positive formulas. By applying suitable abstractions to the hardware model, we can express the functionality of data values and instruction addresses flowing through an instruction pipeline with p-terms. A decision procedure can exploit the restricted uses of p-terms by considering only “maximally diverse” interpretations of the associated function symbols, where every function application yields a different value execept when constrainted by functional consistency. We present two methods to translate formulas in EUF into propositional logic. The first interprets the formula over a domain of fixed-length bit vectors and uses vectors of propositional variables to encode domain variables. The second generates formulas encoding the conditions under which pairs of terms have equal valuations, introducing propostional variables to encode the equality relations between pairs of terms. Both of these approaches can exploit maximal diversity to greatly reduce the number of propositional variables that need to be introduced and to reduce the overall formula sizes. We present experimental results demonstrating the efficiency of this approach when verifying pipelined processors using the method proposed by Burch and Dill. Exploiting positive equality allows us to overcome the experimental blow-up experienced previously when verifying microprocessors with load, store, and branch instructions.

We extend the Burch and Dill flushing technique [6] for formal verification of microprocessors to be applicable to designs where the functional units and memories have multicycle and possibly arbitrary latency. We also show ways to incorporate exceptions and branch prediction by exploiting the properties of the logic of Positive Equality with Uninterpreted Functions [4][5]. We study the modeling of the above features in different versions of dual-issue superscalar processors.

We study the applicability of the logic of Positive Equality with Uninterpreted Functions (PEUF) [2][3] to the verification of pipelined microprocessors with very large Instruction Set Architectures (ISAs). Abstraction of memory arrays and functional units is employed, while the control logic of the processors is kept intact from the original gate-level designs. PEUF is an extension of the logic of Equality with Uninterpreted Functions, introduced by Burch and Dill [4], that allows us to use distinct constants for the data operands and instruction addresses needed in the symbolic expression for the correctness criterion.We present several techniques that make PEUF scale very efficiently for the verification of pipelined microprocessors with large ISAs.These techniques are based on allowing a limited form of non-consistency in the uninterpreted functions, representing initial memory state and ALU behaviors.Our tool required less than 30 seconds of CPU time and 5 MB of memory to verify a 5-stage MIPS-like pipelined processor that implements 191 instructions of various classes.The verification was done by correspondence checking -a formal method, where a pipelined microprocessor is compared against a non-pipelined specification.

This paper introduces the four timing constraints of setup time, hold time, minimum delay, and maximum delay in the efficient memory model (EMM). The EMM is a behavioral model, where the number of symbolic variables used to characterize the initial state of the memory is proportional to the number of distinct symbolic memory locations accessed. The behavioral model provides a conservative approximation of the replaced memory array, while allowing the address and control inputs of the memory to accept symbolic ternary values. If a circuit has been formally verified with the behavioral model, the system is guaranteed to function correctly with any memory implementation whose timing parameters are bounded by the ones used in the verification.