Nowadays the advanced applications required in our lives have led to a significant increase in the complexity of circuits, which enhances the possibility of occurring design errors. Hence an automated, powerful, and scalable debugging approach is needed. Therefore, this paper proposes a scalable approach for localizing multiple bugs in Register-Transfer level (RTL) designs by using neural networks. The main idea is that hit-statements which are covered by failed test-vectors are more suspicious than those covered by passed test-vectors. We use coverage data as samples of our data set, label these samples, and tune the neural network model. Then we encode hit-statements and give them to the tuned model as new samples. The model classifies hit-statements. Hit-statements that take the failed labels, labels related to the failed test-vectors, are more suspicious of containing bugs. The results demonstrate that the proposed methodology outperforms recent approaches Tarsel and CirFix by localizing 80% of bugs at Top-1. The results also imply that our methodology increases the F1-score metric by 1.13× in comparison with existing RTL debugging techniques, which are prediction-based.

Existing debugging and correction approaches suffer from weaknesses such as scalability, reproducing new bugs, and lacking a strategy to deal with multiple bugs. Hence, this article proposes FixRTL, a fully automated scalable methodology for localizing and correcting multiple bugs in Register-Transfer level (RTL) designs. FixRTL consists of three phases: (1) Constructing Samples , (2) Debugging , and (3) Correction . First, we simulate the design under verification (DUV), extract coverage data, and construct our samples. Since we are looking for buggy hit-statements, we use the proposed feature burst (FB) clustering algorithm in the Debugging Phase . The algorithm applies samples as train data, categorizes the encoded hit-statements into bursts, and uses them as test data to predict their cluster. Then we rank hit-statements based on their probability of containing bugs per cluster. In the Correction Phase , we apply a proposed mutation-based framework to correct high-ranked hit-statements. The results show that FixRTL reduces the percentage of hit-statements that must be examined to localize bugs on average by 44.3%. The results also demonstrate that FixRTL corrects 67% of injected bugs while recent existing works correct up to 25%. Moreover, unlike recent works, FixRTL offers corrections that match the grand truth.

One promising approach to verify large arithmetic circuits is making use of Symbolic Computer Algebra (SCA), where the circuit and the specification are translated to a set of polynomials, and the verification is performed by the ideal membership testing. Here, the main problem is the monomial explosion for buggy arithmetic circuits, which makes obtaining the word-level remainder become unfeasible. So, automatic correction of such circuits remains a significant challenge. Our proposed correction method partitions the circuit based on primary output bits and modifies the related Groebner basis based on the given suspicious gates, which makes it independent of the word-level remainder. We have applied our method to various signed and unsigned multipliers, with various sizes and numbers of suspicious and buggy gates. The results show that the proposed method corrects the bugs without area overhead. Moreover, it is able to correct the buggy circuit on average 51.9× and 45.72× faster in comparison with the state-of-the-art correction techniques, having single and multiple bugs, respectively.

Although Symbolic Computer Algebra (SCA) is a promising approach to verify large arithmetic circuits, automatic correction of such circuits based on SCA remains a significant challenge due to the monomial explosion. SCA-based verification methods translate the circuit and the specification into a set of polynomials. The verification problem is considered as an ideal membership test for the given specification polynomial where the ideal is generated by the polynomials of the circuit. A polynomial, called the remainder, is returned by the verification algorithm whose value shows the correctness of the circuit. Our main idea to automatically correct the buggy circuit is to construct a sub-circuit called the corrector, implementing the complement of the remainder, which is added to the buggy circuit. Our method is applied to various multiplier circuits, with different sizes (8 to 256 bits) and the number of bugs (1 to 5 bugs). The proposed method is compared with a method, which eliminates one term of the remainder in each step by inserting elements to the circuit to achieve a zero remainder. The results show that generating the corrector sub-circuit is done, on average, 20.03× faster than before applying our method.

Good knowledge of internal circuit states are crucial for efficient post-silicon debug. Due to the area, power, routing, and bandwidth limitations trace buffer-based design for debug hardware provides execution traces of a limited number of state elements which are then usually expanded through signal restoration. In this paper, we propose to record combinational execution traces and show that combined with signal restoration better knowledge of internal circuit states are obtained. Our experiment with benchmark circuits show that restoration quality in terms of state restoration ratio is improved up to 48% on average. Extending the solution space by, including combinational gates drastically increases signal selection runtime. Using hybrid signal selection methods, we also provide good tradeoff between restoration quality and runtime. By dynamically updating some metrics in state-of-the-art hybrid selection method, we achieve 65% reduction in runtime with only 2% penalty in solution quality. Using the proposed signal selection algorithms, designers can better explore the circuit states and achieve more efficient post-silicon debug.

Hardware Trojan attacks have emerged as a major security issue for hardware at different level of abstractions, which relate to malicious tampering of a hardware during design or fabrication process. In this paper, a new low overhead and high speed design for trust methodology for increasing both full activation and side channel sensitivity of Trojan is proposed. The main idea is that the increase in transition probability of individual nets does not necessarily increase the transition probability of the succeeding nets of the circuit. Accordingly, the rules and conflicts of the propagation of maximum transition probability for individual gates have been presented to ensure that a full transition path is constructed between each low transition probability net and primary inputs of the circuit. The results show that the proposed methodology achieves superior efficiency in Trojan full activation by more than 4× through logic testing approach besides higher sensitivity averagely around 20× for power-based side channel analysis compared to existing methods.

As the complexity of digital designs continuously increases, existing methods to ensure their correctness are facing more serious challenges. Although many studies have been provided to enhance the efficiency of debugging methods, they are still suffering from the lack of scalable automatic correction mechanisms. In this paper, we propose a method for correcting multiple design bugs in gate level circuits. To reduce the correction time, an incremental satisfiability-based mechanism is proposed which not only does not require a complete set of test patterns to produce a gate level implementation which does not exhibit erroneous behavior, but also will not reintroduce old bugs after fixing new bugs. The results show that our method can quickly and accurately suggest corrected gates even for large industrial circuits with many bugs. Average improvements in terms of the runtime and memory usage in comparison with existing methods are 2.8× and 6.5×, respectively. Also, the results show that our method compared to the state-of-the-art methods needs 2.6× less test patterns.

Time borrowing techniques have been widely used to mitigate the timing errors in high-performance designs. A new dynamic flip-flop conversion technique is introduced by Ahmadi et al. (2015) which dynamically converts flip-flops into transparent latches to grant the time borrowing from the next stage and prevent setup time violation. However, it is not able to prevent the timing violation in the successive critical path (SCP) and critical feedback path (CFP) structures. In this brief, we introduce a novel idea of using the output of fast prediction logic of the critical path along with dynamic clock stretching in SCP and CFP structures. The results show that our technique, on average, is able to improve the performance by 20.2% and 14.8% during the prelayout and postlayout simulations, respectively. Furthermore, the proposed technique is almost 7.7% more effective in terms of the performance improvement with only 0.1% area overhead in comparison with the best existing technique.

The increasing demand for lower power forces designers to use sophisticated power management strategies such as multivoltage and power gating which are often accompanied with many design bugs. Correcting such bugs can be a time-consuming process that requires considerable manual efforts. In this paper, we propose a scalable automated method for correcting dynamic power management architectures by an incremental SAT-based mechanism. First, an initial counterexample (CEX) is generated by checking the equivalency between the specification model of the processor and its buggy implementation model. Then, we find two candidate solutions instead of one to satisfy this CEX. If two solutions are not equivalent, we generate new CEX in an iterative process which effectively converges into the final solution. The proposed method enables designers to correct multiple bugs such as missing isolation cells between two power domains, disordering in the sequence of control signals, error in the data restoring or saving, and powering off in always-on domains which are not addressed by existing methods. We have shown the effectiveness of our method on modern processors supporting complex power management mechanisms. The results confirm that our proposed method, respectively, reduces symbolic simulation steps and runtime by 2.33× and 47.93× compared to the state-of-the-art methods.

In range analysis (RA), suitable integer bit-widths are assigned to the variables so that no overflow occurs. Although the accuracy in RA rather than error analysis has more impact on hardware cost and efficiency, there are few works that offer new approaches to improve RA. Arithmetic functions, mostly represented by polynomials, are normally suitable for both optimization and verification purposes. In this paper, a safe and more accurate RA of feed-forward fixed-point polynomial data-flow graphs is proposed. The method employs particular features of RA and maps it to a specific class of polynomial optimization problems. The proposed method provides tighter ranges while taking less runtime in comparison with satisfiability-modulo theory-based method. Furthermore, the improved ranges lead to enhance the area and delay efficiency more than 50% and 24%, respectively, when the circuits are implementing the functions in comparison with the state-of-the-art techniques.

In this article, we present a novel methodology based on SMT-solvers to verify equality of a high-level described specification and a pipelined RTL implementation produced by a high-level synthesis tool. The complex transformations existing in the high-level synthesis process, such as nested loop pipelining, cause the conventional methods of equivalence checking to be inefficient. The proposed equivalence checking method simultaneously attacks the two problems in this context: (1) state space explosion and (2) complex high-level synthesis transformations. To show the scalability and efficiency of the proposed method, the verification results of large designs are compared with those of the SAT-based method, including three different state-of-the-art SAT-solvers: the SMT-based procedure, the modular Horner expansion diagram (M-HED)-based method, and the M-HED partitioning approach. The results show 2470×, 2540×, and 142× average memory usage reduction and 252×, 28×, and 914× speedup in comparison with M-HED, M-HED partitioning, and SMT-solver without using the proposed method, respectively.

Field-programmable gate arrays (FPGAs) could outperform microprocessors on floating point computations due to massive parallelism, freedom on the selection of exponent/mantissa width, and utilization of simplified adders and multipliers. However, optimized use of resources and accuracy of the final implemented expression are two important issues in the implementation of floating point arithmetic expressions on FPGAs. High-level optimizations such as changing the form of floating point initial expression by arithmetic rules or deciding on the exponent and mantissa widths have significant effects on the resource usage, accuracy, and efficiency of the final implementation. In this paper, we introduce an optimization framework called OptiFEX, which enables designers to optimize an initial floating point expression in terms of the resource usage and the exponent and mantissa widths based on: 1) input intervals; 2) the smallest presentable number in the implementation; and 3) the maximum permitted error interval provided by the designer. First, we come up with some techniques to generate equivalent expressions for the initial expression, and we make use of some heuristics to speed up the process of equivalent expressions' generation. We also propose a method to estimate the mantissa width. Finally, we introduce an algorithm to choose the best expressions in terms of the resource usage based on the estimated mantissa and exponent widths.

Although using presilicon information in postsilicon debugging phase seems interesting, space and time limitations of existing formal verification tools restrict the possibility of this idea. In this paper, the effective usage of presilicon information to enhance postsilicon trace signal selection in modern processors is discussed. Furthermore, a novel architecture for dynamic per-cycle selection of signals based on the present instruction is implemented and synthesized. In presilicon phase, first, a set of controlling signals and their corresponding rules are extracted manually. Based on these rules, a set of data from model is extracted using an automatic formal method, which determines which signals should be traced at postsilicon according to the values of controlling signals. This mechanism alone results in an average of 79% and 54% bits to be pruned from the traceable signals for Leon3 and multithreaded DLX processors and 86% and 75% improvement when used in conjunction with traditional methods, respectively.

In this paper, we present an efficient formal approach to check the equivalence of synthesized Register Transfer Level (RTL) against the high level specification in the presence of pipelining transformations. With the proposed equivalence checking method, fault tolerance issues when some faults happen in the designs can be formally analyzed. Equivalence checking with the specification can reason about how quickly the design can come back to normal operations when some faults happen. To increase the scalability of our proposed method, we dynamically divide the designs into several smaller parts called segments by introducing dynamic cut-points. Then we employ Modular Horner Expansion Diagram (M-HED) to check whether the specification and the implementation are equivalent or not. Our proposed method enables us to deal with the equivalence checking problem for behaviorally synthesized designs even in the presence of pipelines for nested loops. The empirical results demonstrate the efficiency and scalability of our proposed method in terms of run-time and memory usage for several large designs synthesized by a commercial behavioral synthesis tool. Average improvements in terms of the memory usage and run time in comparison with SMT- and SAT-based equivalence checking are 16.7× and 111.9×, respectively.

FPGA architectural optimization has emerged as one of the most important digital design challenges. In recent years, experimental methods have been replaced by analytical ones to find the optimized architecture. Time is the main reason for this replacement. Conventional Geometric Programming (GP) is a routine framework to solve analytical models, including area, delay, and power models. In this article, we discuss the application of the Genetic Algorithm (GA) to the design of FPGA architectures. The performance model has been integrated into the Genetic Algorithm framework in order to investigate the impact of various architectural parameters on the performance efficiency of FPGAs. This way, we are able to rapidly analyze FPGA architectures and select the best one. The main advantages of using GA versus GP are concurrency and speed. The results show that concurrent optimization of high-level architecture parameters, including lookup table size ( K ) and cluster size ( N ), and low-level parameters, like scaling of transistors, is possible for GA, whereas GP does not capture K and N under its concurrency and it needs to exhaustively search all possible combinations of K and N . The results also show that more than two orders of magnitude in runtime improvement in comparison with GP-based analysis is achieved.

A large amount of time and effort must be spent to ensure the correctness of a digital design. Although many Computer Aided Design (CAD) solutions have been provided to enhance efficiency of existing debugging approaches, they are suffering from shortage of efficient automatic correction mechanisms. In this paper, we introduce an in-circuit mutation technique for correcting design bugs in digital designs. The aim of this work is reducing correction time by connecting primitive gates into inputs of 6-to-1 multiplexers in the place of potential bugs and utilizing satisfiability (SAT) engine for choosing the correct gates. The empirical results demonstrate that our proposed method can correct multiple bugs in a design by targeting gate replacements and wires exchanges efficiently. Average improvements in terms of the runtime and success rate in correction for combinational circuits in comparison with the latest the existing method are 3.4× and 11.5%, respectively. These results for sequential circuits are 3.8× and 17% respectively.

In this paper, we propose a signature based pruning technique to facilitate the debugging of multi-threaded processors. To accomplish this, a pipelined implementation of the multi-threaded processor model is checked for correspondence against the specification model based on flushing proof. Then, a two-stage signature oriented pruning method is proposed to avoid the space explosion problem caused by inserting debugging facilities in the model. The results show an average improvement of 47%, and 71% in the size of decision formula and CPU time for the DLX processor, respectively.

Ensuring from the correctness of system on a chip (SoC) designs after the insertion of high level power management strategies that are disconnected from low level controlling signals, is a serious challenge to be addressed. This paper proposes a methodology for formally verifying dynamic power management strategies on implementations in modern processors. The proposed methodology is based on correspondence checking between a golden model without power features as a specification and a pipelined implementation with various power management strategies. Our main contributions in this paper are: 1) extracting Power Management Unit (PMU) from Unified Power Format (UPF) and Global Power Management (GPM), 2) automatically integrating PMU into the implementation and 3) checking the correspondence between two models with efficient symbolic simulation. The experimental results show that our method enables the designers to verify the designs with different power management strategies up to several thousands of lines of Register Transfer Level (RTL) code in minutes. In comparison with existing methods such as [7], our method reduces the number of state variables, the number of clauses, the number of symbolic simulation steps, and the CPU time by 11.04×, 17.57×, 2.08× and 13.71×, respectively.

By increasing the complexity of digital systems, verification and debugging of such systems have become a major problem and economic issue. Although many computer aided design (CAD) solutions have been suggested to enhance efficiency of existing debugging approaches, they are still suffering from lack of providing a small set of potential error locations and also automatic correction mechanisms. On the other hand, the ever-growing usage of digital signal processing (DSP), computer graphics and embedded systems applications that can be modeled as polynomial computations in their datapath designs, necessitate an effective method to deal with their verification, debugging and correction. In this paper, we introduce a formal debugging approach based on static slicing and dynamic ranking methods to derive a reduced ordered set of potential error locations. In addition, to speed up finding true errors in the presence of multiple design errors, error candidates are sorted in decreasing order of their probability of being an error. After that, a mutation-based technique is employed to automatically correct bugs even in the case of multiple bugs. In order to evaluate the effectiveness of our approach, we have applied it to several industrial designs. The experimental results show that the proposed technique enables us to locate and correct even multiple bugs with high confidence in a short run time even for complex designs of up to several thousand lines of RTL code.

This paper concentrates on high-level data-flow optimization and synthesis techniques for datapath intensive designs such as those in Digital Signal Processing (DSP), computer graphics and embedded systems applications, which are modeled as polynomial computations over Z2n1x Z2n2x . . . x Z2ndto Z2m. Our main contribution in this paper is proposing an optimization method based on functional decomposition of multivariate polynomial in the form of f(x) = g(x) o h(x) + f0= g(h(x)) + f0to obtain good building blocks, and vanishing polynomials over Z2mto add/delete redundancy to/from given polynomial functions to extract further common sub-expressions. Experimental results for combinational implementation of the designs have shown an average saving of 38.85 and 18.85 percent in the number of gates and critical path delay, respectively, compared with the state-of-the-art techniques. Regarding the comparison with our previous works, the area and delay are improved by 10.87 and 11.22 percent, respectively. Furthermore, experimental results of sequential implementations have shown an average saving of 39.26 and 34.70 percent in the area and the latency, respectively, compared with the state-of-the-art techniques.

Dynamic flip-flop (FF) conversion is a method of time borrowing (TB) for improving the performance of digital systems prone to variations. The first type of this method (Type A), which was previously presented, suffers from a large inefficient transparency window. In this brief, we present an improved structure for this method (Type B) that mitigates this problem by automatically closing the window after the arrival of late data at timing critical FFs. This method was compared with soft edge FF and dynamic clock stretching through simulations on different ITC'99 benchmarks. We defined a parameter called improvement efficiency, which is the ratio of the timing yield improvement to the power overhead of TB. According to the simulation results, the efficiency of Type A is on average 269% more than the best results of other methods when considering only the setup time violations. But, when taking both the setup time and the hold time violations into account, Type B is on average 46% more efficient than the best results of other methods. The simulations also show that the yield improvement of this method increases in higher clock frequencies and it remains the most efficient method when reducing the voltage down to near-threshold region.

A novel time borrowing method called dynamic Flip-Flop conversion is presented in this paper. A timing violation predictor detects the violations halfway in the critical path and dynamically converts the critical Flip-Flop to a latch. This way, time borrowing benefits of latches are utilized in a Flip-Flop based design which is more adaptable with Computer-Aided-Design tools. The overhead of this method is smaller than that of similar methods due to the elimination of delay elements. According to the post-synthesis simulations and Monte-Carlo analysis of Spice simulations on some ITC'99 benchmark circuits, the power overhead of the proposed method is about 15% and 19% smaller than that of Soft-Edge-Flip-Flop and Dynamic-Clock-Stretching circuits respectively in a simple case of about 40% yield improvement. This overhead would be relatively even smaller for higher performance and yield improvements.

In this paper, we introduce a new technique that makes use of satisfiability (SAT) based debugging techniques along with a mutation-based technique to correct certain design errors in digital designs automatically. The experimental results demonstrate that our proposed method enables us to locate and correct multiple bugs by targeting gate replacements and wire exchanging within reasonable run-time and memory usage for several designs.

In this paper, we introduce a formal and scalable debugging approach to derive a reduced ordered set of design error candidates in polynomial datapath designs. To make our debugging method scalable for large designs, we utilize a Modular Horner Expansion Diagram (M-HED), which has been shown to be a scalable high level decision model. In our method, we extract data dependency graphs from the polynomial datapath designs using static slicing. Then we combine backward and forward path tracing to extract a reduced set of error candidates. In order to increase the accuracy of the method in the presence of multiple design errors, we rank the error candidates in decreasing order of their probability of being an error using a proposed priority criterion. In order to evaluate the effectiveness of our method, we have applied it to several large designs. The experimental results show that the proposed method enables us to locate even multiple errors with high accuracy in a short run time.

In this paper we present our hardware architecture on a highly scalable, shared-memory, Monte-Carlo Tree Search (MCTS) based Blokus-Duo solver. In the proposed architecture each MCTS solver module contains a centralized MCTS controller which can also be implemented using soft-cores with a true dual-port access to a shared memory called main memory, and multitude number of MCTS engines each containing several simulation cores. Consequently, this highly flexible architecture guaranties the optimized performance of the solver regardless of the actual FPGA platform used. Our design has been inspired from parallel MCTS algorithms and is potentially capable of obtaining maximum possible parallelism from MCTS algorithm. On the other hand, in our design we combine MCTS with pruning heuristics to increase both the memory and LE utilizations. The results show that our architecture can run up to 50MHz on DE2-115 platform, where each Simulation core requires 11K LEs and MCTS controller requires 10KLEs.

By increasing the complexity of digital systems, debugging of such systems has become a major economical issue. In this paper, we introduce a mutation-based debugging technique that allows us to efficiently locate and then correct bugs in datapath dominated applications such as in Digital Signal Processing (DSP) for multimedia applications and embedded systems. In order to evaluate the effectiveness of our approaches, we have applied the proposed debugging technique to several industrial designs. The experimental results show that the proposed debugging technique enables us to locate and correct even multiple bugs in a reasonable run time and memory usage.

The growing market for Digital Signal Processing (DSP), Computer graphics and embedded systems applications that can be modeled as polynomial computations in their datapath designs, requires improvements in high-level synthesis and optimization techniques for such systems. This paper concentrates on how to find common sub-expressions between s given polynomial functions over Z2n1× Z2n2× ... × Z2ndto Z2min order to optimize the area and delay as much as possible. Our main contributions in this paper is proposing an optimization method based on adding/deleting vanishing polynomials over Z2m, i.e., those polynomials that are equivalent to zero over Z2m, to/from given polynomial functions in the hope of achieving further common sub-expressions. After applying our optimization techniques, experimental comparisons with the state-of-the-art techniques show an average improvement in the area by 36.80% with an average delay decrease of 2.41%. Regarding the comparison with our previous works, the area and delay are improved by 21.4% and 8.7% respectively.

The increased parallelism provided by Out-Of-Order (OOO) and superscalar mechanisms have made the control portion of advanced processors more complicated so that the state-of-the-art formal verification techniques for Register-Transfer-Level (RTL) and gate-level designs cannot scale to the complexity of such complicated processors. Moreover, verification and debugging of exceptions and external interrupts on such processors are nontrivial tasks. Because the exceptions arrival time, the external interrupt arrival time, as well as the microprocessor response time must be precise, verification and debugging require sophisticated hardware and software capabilities. This article proposes techniques for effective verification and debugging of cycle-accurate OOO processors in the event of exceptions and external interrupts. The results show that our techniques reduce the complexity of the verification and debugging processes by reducing the number of simulation cycles (3.3 × average reduction) and the number of state variables (8.7 × average reduction) to be traced for localizing bugs.

Early generation of effective high level test patterns can significantly reduce Automatic Test Pattern Generation (ATPG) efforts in gate level. This paper proposes an ATPG methodology targeting non-scan designs. Although our methodology checks all execution paths, a decision procedure is applied to detect the false paths very early and split the cases before generating high level test patterns. Experimental results show robustness and reliability of our method compared to FlexTest as a commercial gate level ATPG tool.

This paper proposes a non-scan gate-level Automatic Test Pattern Generation (ATPG) methodology which keeps the regularity in the arithmetic operations while reasoning about these operations for generating high-level test patterns from only faulty behavior of the design. Then by considering generated high-level test patterns as constraints and passing them to a SMT-solver we are able to automatically and efficiently generate gate-level test patterns. Experimental results show robustness and reliability of our method compared to other contemporary methods in terms of the fault coverage and CPU time.

Clock period of pipelined designs are usually determined by the critical paths to avoid timing errors and guarantee reliable operations. The worst case delays of the slowest pipeline stages cause the clock frequency to be less than the average path delays. This may introduce enormous performance loss if the critical paths rarely happen, and the critical path delays are far larger than the average path delays, which is common for many pipelined circuits. In this paper we present a novel timing error recovery technique that guarantees reliable operation of pipelined designs in presence of any arbitrary number of timing errors in different pipeline stages. We allow the clock frequency to be higher than the worst case; hence increasing the performance. We demonstrate the usefulness of our technique by implementing a pipelined arithmetic circuit with the proposed technique on top of a FPGA board. Our experimental results show that we could successfully increase the clock frequency by 30% with the timing error rate of 13%, all of which are automatically corrected with negligible performance penalty. The timing error recovery circuits need extra flipflops for timing error detection and correction. Since typical FPGAs have LUT with flipflops, the extra area for additional flipflops is minimized as the experimental results have shown. With sophisticated synthesis algorithms for pipelined arithmetic circuits which balanced path delays in the circuits, significantly more performance improvements can be expected.

Due to the highly complicated control structures of modern processors, some of the logical bugs may escape from the verification process and remain into the silicon. This paper proposes verification/debugging/field-rectification methods based on formal verification techniques that enables designers not only to automatically debug high performance processors by concentrating on word-level reasoning but also to introduce key control points with programmability in the silicon so that post-silicon bugs can be rectified in the field. The results show that by considering those state variables that fix wide ranges of pre-silicon bugs as key control points for programmability in the fields, inserted LUTs can be reduced due to the fact that only one LUT can be shared to correct all relevant bugs.

For a variety of signal processing applications polynomials are implemented in circuits. Recent work on polynomial datapath optimization achieved significant reductions of hardware cost as well as delay compared to previous approaches like Horner form or Common Sub-expression Elimination (CSE). This work 1) proposes a formal model for single- and multi-polynomial factorization and 2) handles optimization as a constraint solving problem using an explicit cost function. By this, optimal datapath implementations with respect to the cost function are determined. Compared to recent state-of-the-art heuristics an average reduction of area and critical path delay is achieved.

This paper proposes an automatic design flow of datapath-dominated applications which is able to deal with optimization and equivalence checking of multi-output polynomials over Z2n. This paper also gives four main contributions: 1) proposing a complete design flow for modular equivalence checking, high level synthesis, and optimization; 2) considering hidden monomials to factorize those polynomials which do not have any common monomials; 3) combining and improving our previous optimization heuristics to eliminate multi-operand common sub-expressions as much as possible; and 4) implementing all algorithms on top of the modular Horner expansion diagram package. Experimental results have shown an average saving of 9.9% and 4.5% in the number of gates and critical path delay, respectively, after applying modular reduction over Z2n, while other optimization techniques are not used. Besides, after applying our optimization techniques, experimental comparisons with the state-of-the-art techniques show an average improvement in the area by 19.5% with an average delay decrease of 16.7%. Regarding the comparison with our previous papers, the area and delay are improved by 13.3% and 15.5%, respectively.

This paper proposes a high-level test generation method which considers the control part as well as data path of a register transfer level circuit as a set of polynomial functions to generate behavioral test patterns from faulty behavior instead of comparing the faulty and fault-free circuits based on a hybrid Boolean-word canonical representation called Horner expansion diagram. Since this set of polynomial functions express primary outputs and next states with respect to primary inputs and present states, it is not necessary to perform justification/propagation phase which leads to a minimum number of backtracks. It improves fault coverage and reduces test generation time over logic-level techniques. We assess then the effectiveness of high-level test generation with a simple gate-level automatic test pattern generation algorithm. Experimental results show robustness and reliability of our method compared to other contemporary approaches in terms of fault coverage and CPU time.

Datapath designs that perform polynomial computations over Z 2 nare used in many applications such as computer graphics and digital signal processing domains. As the market of such applications continues to grow, improvements in high-level synthesis and optimization techniques for multivariate polynomials have become really challenging. This paper presents an efficient algorithm for optimizing the implementation of a multivariate polynomial over Z 2 n in terms of the number of multipliers and adders. This approach makes use of promising heuristics to extract more complex common sub-expressions from the polynomial compared to the conventional methods. The proposed algorithm also utilizes a canonical decision diagram, Horner-Expansion Diagram (HED) [1] to reduce the polynomial's degree over Z 2 n. Experimental results have shown an average saving of 27% and 10% in terms of the number of logic gates and critical path delay respectively compared to existing high-level synthesis tools as well as state of the art algebraic approaches.

Conventional high-level synthesis techniques are not able to manipulate polynomial expressions efficiently due to the lack of suitable optimization techniques for redundancy elimination over Z2n.

Integer multipliers with finite output bit-widths are widely used in many Digital Signal Processing (DSP) applications. In such circuits high-level optimizations like Residue Number System (RNS) can be utilized to achieve more efficient architectures compared to the conventional binary representations. This paper presents an efficient high-level Don't-Care Optimization (DC-Opt) method for integer multipliers and in general Multiply Accumulator (MAC) units when the output result is limited to a finite bit-width. This high-level optimization approach can then be combined with logic optimizations at gate-level. Experimental results have shown major improvements in terms of area and latency compared to the conventional optimization approaches.

This paper presents a novel automatic debugging algorithm for a postsynthesis combinational arithmetic circuit. The approach is robust under wide varieties of arithmetic circuit architectures and design optimizations. The debugging algorithm in this paper consists of three phases of partial product initialization, XOR extraction, and carry-signal mapping. The run-time complexity of conventional carry-signal-mapping algorithms, such as the approach described by Stoffel and Kunz, is exponential. However, in the proposed algorithm, by making use of some important design issues, we categorize the extracted XORs into half/full-adders to make a very fast debugging algorithm. This approach is robust under multioperand adders, pin-swap techniques, optimizations concerning carry signals or XOR terms, and irregularities, such as commutative and associative laws. Moreover, the XOR extraction in the proposed algorithm is much faster than conventional techniques, as it does not evaluate the whole netlist. The bugs detected in the partial product initialization and the carry-signal mapping can automatically be replaced with proper logics. However, during the XOR extraction phase, the problematic XORs are only reported by the algorithm, and no automatic replacement is performed for such logic gates. To evaluate the effectiveness of our approach, we run it on several arithmetic circuits.

In this paper, we propose a novel approach to extract a network of half adders from the gate-level net-list of an addition circuit while no internal equivalences exist. The technique begins with a gate-level net-list and tries to map it into word-level adders based on an efficient bit-level adder representation. It will be shown that the proposed technique is suitable for several gate-level architectures of multipliers, as it extracts adder components in a step-wise method. This approach can also be generalized to other arithmetic circuits. In order to evaluate the effectiveness of our approach, we run it on several arithmetic circuits and compare experimental results with those of contemporary techniques.

This paper proposes word-level coverage metric to determine the completeness of a set of properties verified by a word-level method. An algorithm is presented to compute a functionality based coverage metric for a sequence property as specification. Control, intermediate and output signals are represented by a multiplexer based structure of linear integer equations, and RT level properties are directly applied to this representation. A set of integer equations are symbolically simulated based on the specified property in a predictable time. We used a canonical form of linear Taylor expansion diagram