A representation of a Boolean function is canonical if, given a variable order, only one instance of the representation is possible for the function. A computation is canonical if the result depends only on the Boolean function and a variable order, and does not depend on how the function is represented and how the computation is implemented.

Hard-wired carry chains in FPGAs are designed to improve efficiency of important arithmetic primitives. Although they are proven to be effective for arithmetic-rich functions, there are very few studies on the optimization opportunities of carry chains for general logic that is poor in arithmetic operations. Recently, Majority-Inverter Graphs (MIGs) were proposed for efficient Boolean logic optimization. MIGs open an opportunity for efficient mapping of critical paths onto hard carry chains, as the carry logic of a full adder is naturally a majority (MAJ) gate. In this paper, we propose an MIG-based synthesis method to exploit hard adders in FPGAs for the mapping of general logic. The proposed heuristic algorithm selects MAJ nodes to be mapped on the carry chains and the associated LUTs; then, the efficiency of carry chain mapping is examined theoretically for efficient LUT utilization. The experimental results show that, compared to traditional design flow Verilog-to-Routing (VTR 7.0), the proposed approach can improve delay by up to 25% with an average of 8%, while the channel width is reduced by up to 20% with an average of 6%.

Classifying functions according to some common properties into libraries of functions is an important step in many logic synthesis and technology mapping algorithms used in FPGA design flows. NPN classification is one of the frequently used classifications. Existing algorithms for NPN classification perform a sequence of steps to derive the resulting NPN class, but discard the intermediate results produced at the end of each step. The hierarchical method introduced in this paper uses the same sequence of steps, but it saves the intermediate results at each step and reuses them when classifying other functions. It is, on average, 3.7 times faster compared to a state-of-the-art non-hierarchical method, at the cost of a modest increase in memory needed to save the class hierarchy. The hierarchical approach enables a rapid exact NPN classification for functions up to 10 inputs-it exactly classifies one million 6-input functions in the same time as the heuristic state-of-the-art algorithm.

Lexicographic Boolean satisfiability (LEXSAT) is a variation of the Boolean satisfiability problem (SAT). Given a variable order, LEXSAT finds a satisfying assignment whose integer value under the given variable order is minimum (maximum) among all satisfiable assignments. If the formula has no satisfying assignments, LEXSAT proves it unsatisfiable, as does the traditional SAT. The paper proposes an efficient algorithm for LEXSAT by combining incremental SAT solving with binary search. It also proposes methods that use the lexicographic properties of the assignments to further improve the runtime when generating consecutive satisfying assignments in lexicographic order. The proposed algorithm outperforms the state-of-the-art LEXSAT algorithm—on average, it is 2.4 times faster when generating a single LEXSAT assignment, and it is 6.3 times faster when generating multiple consecutive assignments.

Carry chains facilitate the implementation of adders and improve the performance of arithmetic circuits in FPGAs. The last version of the commonly used open-source Verilog-to-Routing (VTR) CAD flow now enables modelling carry chains in FPGA architectures. However, one of the shortcomings of the existing flow lies in its inability to identify arithmetic operations when described as gate-level circuits. Moreover, the VTR flow squanders most of the LUTs preceding the chain logic. This paper focuses on these two problems and proposes preprocessing the circuit before technology mapping to allow for a more efficient use of carry chains. The first proposed method maps logic on the carry chains for circuits expressed using a gate-level description. On average, it identifies about 30% more meaningful full adders than the existing tool flow operating on the RTL descriptions. Area is thus improved by up to 15% with an average of 6% for almost no delay penalty. Secondly, we increase the use of the LUTs preceding the chain logic by a factor 2 on average. This reduces delay (up to 9%) and area (up to 2%), compared to the existing VTR flow. The new approach is independent of the specific carry-chain architecture and can be generically adapted to any FPGA with built-in hardened adders.

Craig interpolation is a known method for expressing a target function f as a function of a given set of base functions G. The resulting interpolant represents the dependency function h, such that f = h(G). Generally, the set G contains enough base functions to enable the existence of multiple dependency functions whose quality mainly depends on which base functions were selected for reconstruction. The interpolation is not an optimisation problem and thus, often, it selects some random base functions and, particularly, omits others potentially required for an optimal implementation of the target function. Mainly, it is impossible to impose that the interpolant uses a specific base function. In this paper, we propose a method that forces a specific base function gias a primary input of a dependency function. Such a dependency function is built as a Shannon expansion of two constrained Craig interpolants for the assignments of the primary inputs for which gievaluates to 0 and 1, respectively. We also introduce a method that iteratively imposes a predefined set of base functions. In each iteration, we generate a new dependency function for use as the target function of the next iteration in order to force the use of a base function. We show that, unlike the standard Craig interpolation method, our carving method succeeds to impose the desired base functions with very high probability. It recomposes single-output logic circuits as their delay- or area-optimised implementations regardless of the input implementation. The proposed methods can be efficiently employed for rewriting circuits in some synthesis-based algorithms.