Search

International audience; The paper introduces a novel verification methodof gate-level hardware implementation of divider circuits. Themethod, called hardware reduction, accomplishes the verificationby appending the divider circuit with another circuit, which implementsits arithmetic inverse, followed by logic synthesis. If thecircuit under verification is correct, the resulting resynthesizedcircuit becomes trivially redundant (composed of wires or buffersonly). This method outperforms the established SAT-based andequivalence checking techniques and does not require a referencedesign.

A considerable progress has been made in recent years in verification of arithmetic circuits such as multipliers, fused multiply-adders, multiply-accumulate, and other components of arithmetic datapaths, both in integer and finite field domain. However, the verification of hardware dividers and square-root functions have received only a limited attention from the verification community, with a notable exception for theorem provers and other inductive, non-automated systems. Division, square root, and transcendental functions are all tied to the basic Intel architecture and proving correctness of such algorithms is of grave importance. Although belonging to the same iterative-subtract class of architectures, they widely differ from each other. IEEE floating point standard specifies square-rooting and division as basic arithmetic operation alongside the usual three basic operations. The difficulty of formally verifying hardware implementation of a divider/square-root can be attributed mostly to the modeling of its characteristic function and the high memory complexity required by standard algebraic approach. The work proposed in this thesis discusses formal verification of combinational divider and square-root circuits. Specifically, it addresses the problem of formally verifying gate-level circuits using an algebraic model. In contrast to standard verification approaches using satisfiability (SAT) or equivalence checking, the proposed method verifies whether the gate-level circuit actually performs the intended function or not, without a need for a reference design. Firstly, we present a verification methodology for a constant divider, where the divisor value is fixed to a constant integer. Albeit simpler case of verification, it provides us with the basic understanding of verification techniques and the underlying issues applicable to divider verification. Secondly, a layered verification approach is proposed for the verification of generic array dividers. Finally, the work proposed in this thesis will further analyze the divider and square-root circuits and aim to curb the memory explosion issue experienced by computer algebra based verification methods in order to successfully verify large bit-width divider-type arithmetic circuits. More specifically, a novel idea of "hardware rewriting" is introduced, which avoids the high memory complexity. The mentioned technique verifies a 256-bit gate-level square-root circuit with around 260,000 gates in just under 18 minutes and 127-bit gate-level divider circuit in under one minute.

Timing speculation is a promising approach to increase the processor performance and energy efficiency. Under timing speculation, an integrated circuit is allowed to operate at a speed faster than its slowest path|the critical path. It is based on the empirical observation, which is presented later in the thesis, that these critical path delays are rarely manifested during the program execution. Consequently, as long as the processor is equipped with an error detection and recovery mechanism, its performance can be increased and/or energy consumption reduced beyond that achievable by any other conventional operation. While many past works have dealt with timing speculation within a single core, in this work, a new direction is being uncovered | timing speculation for a multi-core processor executing a parallel, multi-threaded application. Through a rigorous cross-layered circuit architectural analysis, it is observed that during the execution of a multi-threaded program, there is a significant variation in circuit delay characteristics across different threads. Synergistic Timing Speculation (SynTS) is proposed to exploit this variation (heterogeneity) in path sensitization delays, to jointly optimize the energy and execution time of the many-core processor. In particular, SynTS uses a sampling based online error probability estimation technique, coupled with a polynomial time algorithm, to optimally determine the voltage, frequency and the amount of timing speculation for each thread. The experimental analysis is presented for three pipe stages, namely, Decode, SimpleALU and ComplexALU, with a reduction in Energy Delay Product by up to 26%, 25% and 7.5% respectively, compared to existing per-core timing speculation scheme. The analysis also embeds a case study for a General Purpose Graphics Processing Unit.