In monadic programming, datatypes are presented as free algebras, generated by data values, and by the algebraic operations and equations capturing some computational effects. These algebras are free in the sense that they satisfy just the equations imposed by their algebraic theory, and remain free of any additional equations. The consequence is that they do not admit quotient types. This is, of course, often inconvenient. Whenever a computation involves data with multiple representatives, and they need to be identified according to some equations that are not satisfied by all data, the monadic programmer has to leave the universe of free algebras, and resort to explicit destructors. We characterize the situation when these destructors are preserved under all operations, and the resulting quotients of free algebras are also their subalgebras. Such quotients are called projective. Although popular in universal algebra, projective algebras did not attract much attention in the monadic setting, where they turn out to have a surprising avatar: for any given monad, a suitable category of projective algebras is equivalent with the category of coalgebras for the comonad induced by any monad resolution. For a monadic programmer, this equivalence provides a convenient way to implement polymorphic quotients as coalgebras. The dual correspondence of injective coalgebras and all algebras leads to a different family of quotient types, which seems to have a different family of applications. Both equivalences also entail several general corollaries concerning monadicity and comonadicity.

The articles in this special issue focus on current trends and developments in the field of computer arithmetic. This is a field that encompasses the definition and standardization of arithmetic system for computers. The field also deals with issues of hardware and software implementations and their subsequent testing and verification. Many practitioners of the field also focus on the art and science of using computer arithmetic to carry out scientific and engineering computations. Computer arithmetic is therefore an interdisciplinary field that draws upon mathematics, computer science and electrical engineering. Advances in this field span from being highly theoretical (for instance, new exotic number systems) to being highly practical (for instance, new floating-point units for microprocessors).

The AMD Jaguar x86 core uses a fully-synthesized, 128-bit native floating-point unit (FPU) built as a co-processor model. The Jaguar FPU supports several x86 ISA extensions, including x87, MMX, SSE1 through SSE4.2, AES, CLMUL, AVX, and F16C instruction sets. The front end of the unit decodes two complex operations per cycle and uses a dedicated renamer (RN), free list (FL), and retire queue (RQ) for in-order dispatch and retire. The FPU issues to the execution units with a dedicated out-of-order, dual-issue scheduler. Execution units source operands from a synthesized physical register file (PRF) and bypass network. The back end of the unit has two execution pipes: the first pipe contains a vector integer ALU, a vector integer MUL unit, and a floating-point adder (FPA), the second pipe contains a vector integer ALU, a store-convert unit, and a floating-point iterative multiplier (FPM). The implementation of the unit focused on low-power design and on vectorized single-precision (SP) performance optimizations. The verification of the unit required complex pseudo-random and formal verification techniques. The Jaguar FPU is built in a 28nm CMOS process.

On behalf of the organizing and program committee, we would like to welcome you to the 28thIEEE International Conference on Computer Design 2010. The International Conference on Computer Design (ICCD) encompasses a wide range of technical topics and provides an ideal environment to discuss practical and theoretical work that enables cross-pollination. The ICCD venue and program reflect this goal. Being a truly international venue, this year the conference is held in the exciting multi-cultural city of Amsterdam, the Netherlands.

We report on the full gate-level verification and FPGA implementation of a highly optimized double precision IEEE floating-point adder. The proposed adder design incorporates many optimizations like a nonstandard separation into two paths, a simple rounding algorithm, unification of rounding cases for addition and subtraction, sign-magnitude computation of a difference based on one's complement subtraction, compound adders, and fast circuits for approximate counting of leading zeros from borrow-save representation. We formally verify a gate-level specification of the algorithm using theorem proving techniques in PVS. The PVS specification was then used to automatically generate a gate-level implementation that was synthesized using Altera Quartus II. The resulting implementation has a total latency of 13.6 ns on an Altera Stratix II device.We have partitioned the design into a 2 stage pipeline running at a frequency of 147 Mhz.

We report the results of an FPGA implementation of double precision floating-point division with IEEE rounding. We achieve a total latency (i.e., cycles times clock period) that is 2:6 times smaller than the latency of the fastest previous implementation on FPGAs. The amount of hardware, on the other hand, is comparable to commercial cores. The division circuit is based on Goldschmidt's algorithm. All IEEE rounding modes are supported and are implemented using dewpoint rounding. The precision of the initial approximation of the reciprocal is 14 bits. To save hardware and reduce the critical path, a half-sized 62x30 Booth radix-8 multiplier is used. This multiplier can receive both the multiplicand and the multiplier in carry-save representation. The division circuit is partitioned into four pipeline stages, has a latency of 11 cycles, and may restart a new double precision division operation after 8 cycles. Synthesis results of an implementation (not including the computation of the initial approximation of the reciprocal and the exponent path) guarantee a clock frequency of 131 MHz on an Altera Stratix II using 3592 ALMs. The implementation was successfully tested with over 10 million random vectors as well as over a million hard-to-round vectors.

We are proposing a micro-architecture for high-performance IEEE floating-point addition that is based on a (non-redundant) high-radix representation of the floating-point operands. The main improvement of the proposed IEEE FP addition implementation is achieved by avoiding the computation of full alignment and normalization shifts which impose major delays in conventional implementations of IEEE FP addition. This reduction is achieved at the cost of wider operand interfaces and an increased complexity for IEEE compliant rounding. We present a detailed discussion of an IEEE FP adder implementation using the proposed high-radix format and explain the specific benefits and challenges of the design.

Research on formal hardware verification has made steady progress in developing methodologies and tools that try to cope with the growing complexities of systems. Despite of case studies that demonstrate the applicability of formal methods to selected contemporary processor designs, the current state in formal hardware verification is far from being considered practical for systems of the complexity of complete contemporary processor designs. It is our goal to improve the practicality of current formal verification methods for complete state-of-the-art processor designs. The recent success in the complete formal verification of the VAMP can be considered pioneering for reaching design complexities close to this range. We dissect the VAMP verification effort in detail with the goal to identify the main technical and organizational challenges and the major productivity bottlenecks of the verification process. This is done in particular to search for opportunities of increased levels of automation. As part of our efforts we are developing the VAMPExplorer, a tool that provides an intuitive interface to the specification, the implementation and the verification of the VAMP. The VAMPExplorer visualizes the general implementation and verification structure and improves accessibility to expert and non-expert users.

Back in the 60's Goldschmidt presented a variation of Newton-Raphson iterations for division that is well suited for pipelining. The problem in using Goldschmidt's division algorithm is to verify that the implementation meets the precision required for the quotient and provides correct rounding, in particular if hardware resources are to be used judiciously. Previous implementations relied on error analysis that were not quite tight and that were specific to one parameter setting and target precision. Our formal verification effort focuses on a parametric division implementation based on Goldschmidt's algorithm for different parameter settings and target precisions. We formalize a tight and parametric error analysis of Goldschmidt's division algorithm in PVS and prove its correctness. On this basis we propose formally verified parametric division implementations.

For progressively higher radices, the reduction in partial products obtained by the well-known modified Booth multiplier recoding is offset by the need to precompute a rapidly increasing store of odd multiples of the multiplicand as inputs to each partial product generator (PPG). We propose secondary radix multiplier recoding schemes reducing the number of odd multiples required in the store for very high radix recodings (e.g., radix 2/sup r/ for 5 /spl les/ r /spl les/ 16). The proposed recoding schemes allow reduction of the number of partial products in the implementation by factors between and beyond the reduction factors of 2, 3, and 4 that can be achieved by traditional Booth recodings to radices 4, 8, and 16, respectively. We develop the theory of these recodings and provide methodology for secondary radix selection. Finally, we summarize latency and cost evaluations of selected implementations indicating potential cost and performance/cost advantages for practical operand sizes.

We present the design of an on-line IEEE floating-point (FP) adder. In on-line arithmetic a result is computed as a digit serial output stream from digit serial input streams. The result digits begin to be produced a short delay after the first input digits arrive and before all the input digits have been received. On-line arithmetic proceeds from the most significant digit first through the least significant digit. Performing on-line addition on IEEE FP numbers imposes challenges beyond the challenges of conventional on-line arithmetic, including the task of normalization and IEEE rounding and its effect on the digits already output. The proposed implementations are very suitable for FPGAs, because the serial organization simplifies critical components of conventional FPGA IEEE FP addition implementations: Large alignment and normalization shifters are avoided allowing for reduced interconnection complexities and reasonable latencies at low implementation cost. The proposed implementations are fully compliant with the IEEE FP standard.

This paper deals with special challenges in the formal verification of high-performance circuits that involve redundant number representations and partial compressions. Our particular focus is the verification of circuits where symbolic consideration of number representations is not sufficient, but where additionally properties beyond operand values need to be considered to show correct operation. As a solution, we consider theorem proving techniques in PVS and we propose a framework that allows for reasoning about signal correlation properties in redundant representations. We develop a library for redundant representations that includes support of basic circuits for partial compression and that verifies several fundamental properties regarding signal correlation and partial compression in the computed results. We outline the applicability of our library in the verification of several practical circuits.

We present an IEEE floating-point adder (FP-adder) design. The adder accepts normalized numbers, supports all four IEEE rounding modes, and outputs the correctly normalized rounded sum/difference in the format required by the IEEE Standard. The FP-adder design achieves a low latency by combining various optimization techniques such as: a nonstandard separation into two paths, a simple rounding algorithm, unification of rounding cases for addition and subtraction, sign-magnitude computation of a difference based on one's complement subtraction, compound adders, and fast circuits for approximate counting of leading zeros from borrow-save representation. We present technology-independent analysis and optimization of our implementation based on the Logical Effort hardware model and we determine optimal gate sizes and optimal buffer insertion. We estimate the delay of our optimized design at 30.6 FO4 delays for double precision operands (15.3 FO4 delays per stage between latches). We overview other IEEE FP addition algorithms from the literature and compare these algorithms with our algorithm. We conclude that our algorithm has shorter latency (-13 percent) and cycle time (-22 percent) compared to the next fastest algorithm.

Back in the 60's Goldschmidt presented a variation of Newton-Raphson iterations for division that is well suited for pipelining. The problem in using Goldschmidt's division algorithm is to present an error analysis that enables one to save hardware by using just the right amount of precision for intermediate calculations while still providing correct rounding. Previous implementations relied on combining formal proof methods (that span thousands of lines) with millions of test vectors. These techniques yield correct designs but the analysis is hard to follow and is not quite tight. We present a simple parametric error analysis of Goldschmidt's division algorithm. This analysis sheds more light on the effect of the different parameters on the error. In addition, we derive closed error formulae that allow to determine optimal parameter choices in four practical settings. We apply our analysis to show that a few bits of precision can be saved in the floating-point division (FP-DIV) microarchitecture of the AMD-K7/spl trade/ microprocessor. These reductions in precision apply to the initial approximation and to the lengths of the multiplicands in the multiplier. When translated to cost, the reductions reflect a savings of 10.6% in the overall cost of the FP-DIV microarchitecture.

We propose optimized pipelined implementations for Goldschmidt's division algorithm with IEEE rounding based on Booth radix-8 multiplication. Compared to other FP-division algorithms, our implementations require fewer clock cycles and admit shorter clock periods. The considered optimizations for the quotient approximation are based on a careful general analysis of tight error bounds for the implementation and are accompanied by the utilization of redundant representations, partial compressions, injection-based rounding, and rectangular multipliers for the internal computations. To efficiently achieve IEEE compliant rounding, we introduce the concept of dew-point rounding that allows efficient implementation and reduced requirements for the quotient approximation. On this basis, we propose the implementation of different versions of Goldschmidt's division algorithm with different pipeline depths. None of these implementations requires a full-sized multiplier at any stage of the computations. In this way we reduce latency, cost, and enable increased throughput at a reasonable cost. We suggest a full range of pipelining depths: On one extreme is a 3-stage pipeline with a restart time that simply equals the latency minus the number of pipeline stages. On the other extreme is a fully pipelined design.

We present an IEEE floating-point adder (FP-adder) design. The adder accepts normalized numbers, supports all four IEEE rounding modes, and outputs the correctly normalized rounded sum/difference in the format required by the IEEE standard. The latency of the design for double precision is roughly 24 logic levels, not including delays of latches between pipeline stages. Moreover, the design can be easily partitioned into 2 stages consisting of 12 logic levels each, and hence, can be used with clock periods that allow for 12 logic levels between latches. The FP-adder design achieves low latency by combining various optimization techniques such as: a non-standard separation into two paths, a simple rounding algorithm, unifying rounding cases for addition and subtraction, sign-magnitude computation of a difference based on complement subtraction, compound adders, and fast circuits for approximate counting of leading zeros from borrow-save representation. A comparison of our design with other implementations suggests a reduction in the latency by at least two logic levels as well as simplified rounding implementation. A reduced precision version of our algorithm has been verified by exhaustive testing.

Multipliers are used at many different places in microprocessor design. As the non-memory sub-blocks of the microprocessor with the largest size and delay, multipliers have a big impact on the cycle time of the microprocessor. Targeting deeper pipelines and higher clock frequencies, there is a growing demand for multiplier designs that can be split into shorter stages. For this purpose, the use of Booth recoding has been a popular method to cut down the number of partial products in a multiplier to reduce the delay of the partial product accumulation and to simplify the partition of the multiplier into several shorter stages. The complexity to pre-compute an increasing number of digit multiples of the multiplicand within the multiplier unit limits the use of Booth recoding mainly to radices 4 and 8. We propose novel encoding schemes for the implementation of higher radix multiplication. In particular we consider multiplication radix-32 and radix-256. The features provide more flexible multiplier designs that can be implemented in shorter pipeline stages. We compare the proposed designs with multipliers that use traditional Booth recoding.

A new IEEE compliant floating-point rounding algorithm for computing the rounded product from a carry-save representation of the product is presented. The new rounding algorithm is compared with the rounding algorithms of Yu and Zyner (1995) and of Quach et al. (1991). For each rounding algorithm, a logical description and a block diagram is given, the correctness is proven, and the latency is analyzed. We conclude that the new rounding algorithm is the fastest rounding algorithm, provided that an injection (which depends only on the rounding mode and the sign) can be added in during the reduction of the partial products into a carry-save encoded digit string. In double precision format, the latency of the new rounding algorithm is 12 logic levels compared to 14 logic levels in the algorithm of Quach et al. and 16 logic levels in the algorithm of Yu and Zyner.

A novel IEEE compliant floating point rounding algorithm for computing the rounded product from a carry-save representation of the product is presented. The new rounding algorithm is compared with the rounding algorithms of R. Yu and G. Zyner (1995) and of N. Quach et al. (1991). For each rounding algorithm, a logical description and a block diagram is given and the latency is analyzed. We conclude that the new rounding algorithm is the fastest rounding algorithm, provided that an injection (which depends only on the rounding mode and the sign) can be added in during the reduction of the partial products into a carry-save encoded digit string. In double precision the latency of the new rounding algorithm is 12 logic levels compared to 14 logic levels in the algorithm of Quach et al., and 16 logic levels in the algorithm of Yu and Zyner.

We present an algorithm for IEEE floating-point addition. The latency of the addition algorithm for double precision is roughly 24 logic levels, not including delays of latches between pipeline stages. The algorithm accepts normalized numbers, supports all four IEEE rounding modes, and outputs the correctly rounded sum/difference in the format required by the IEEE Standard. The presentation of the algorithm is technology independent and can serve as basis for evaluation and comparison with other floating-point addition algorithms.