Search

Traditionally, FPGA designers make use of CAD tools for evaluating architectures in terms of the area, delay and power. Recently, analytical methods have been proposed to optimize the architectures faster and easier. A complete analytical power, area and delay model have received little attention to date. In addition, previous works use analytical methods to optimize general-purpose FPGA architectures. Using analytical models for optimizing application-specific FPGA architectures are interesting subjects in the reconfigurable computing field. In this way, designers can investigate the optimized architecture for a set of application circuits and the consumers can find their best architecture among a variety of devices which is optimal for their specific work. In this paper, we complete an analytical FPGA performance model by presenting an analytical model to estimate the dynamic and leakage power and by integrating it into the geometric programming framework. This way, we are able to rapidly analyze various FPGA architectures and select the best one in terms of power consumption as well as area and delay. In the next step, we extend the model for optimizing FPGA architectures for a set of applications. A case of the best architecture for two specific circuits has been investigated in this paper. [ABSTRACT FROM AUTHOR]

Verification of arithmetic circuits is essential as they form the main part of many practical designs such as signal processing and multimedia applications. In these applications, the size of the datapath could be very large so that contemporary verification methods would be almost incapable of verifying such circuits in reasonable time and memory usage. This paper addresses formal verification of large integer arithmetic circuits using symbolic computer algebra techniques. In order to efficiently verify gate level arithmetic circuits, we model the circuit and the specification with polynomial system and the verification problem is formulated as membership testing of the given specification polynomial in corresponding ideal of the circuit polynomials. The membership testing needs Groebner basis reduction. In order to overcome the intensive polynomial reduction needed in Groebner basis computation so that we can deal with verifying large arithmetic circuits, the fanout-free regions (cones) of the circuit are extracted and represented as corresponding polynomials automatically. For further improvement, we make use of Gaussian elimination concept to perform specification polynomial reduction w.r.t Groebner basis using a matrix representation of the problem. To evaluate the effectiveness of our verification technique, we have applied it to very large arithmetic circuits with different architectures. The experimental results show that the proposed verification technique is scalable enough so that large arithmetic circuits can efficiently be verified in reasonable run time and memory usage. [ABSTRACT FROM AUTHOR]

By increasing the complexity of system on chip (SoC) designs formal equivalence verification and debugging have become more and more important. Lower level methods such as BDDs and SAT solvers suffer from space and time explosion problems to match sizes of industrial designs in formal equivalence verification and debugging. This paper proposes techniques to verify and debug datapath intensive designs based on a canonical decision diagram called Horner Expansion Diagram (HED). It allows us to check the equivalence between two models in different levels of abstraction, e.g., a Register Transfer Level (RTL) implementation and a non-cycle-accurate specification. In order to reduce the complexity of equivalence checking problem, we tackle the exponential path enumeration problem by automatically identifying internal equivalent conditional expressions as well as suitable merge points. Our debugging technique is based on introducing mutations into the buggy implementation and then observing if the specification is capable of detecting these changes. We make use of a simple heuristic to reduce the number of mutants when dealing with multiple errors. We report the results of deploying our equivalence verification technique on several industrial designs which show 16.8× average memory usage reduction and 8.0× speedup due to merge-point detection. Furthermore, our debugging technique shows 13.7× average memory usage reduction and 4.6× speedup due to using SMT solvers to find equivalent conditions. In addition, the proposed debugging technique can avoid the computation of unnecessary mutants so that the results show 2.9× average reduction of the number of mutants to be processed. [ABSTRACT FROM AUTHOR]