This study presents a formal verification method for Galois-field (GF) arithmetic circuits with the characteristics of more than two values. The proposed method formally verifies the correctness of circuit functionality (i.e., the input-output relations given as GF-polynomials) by checking the equivalence between a specification and a gate-level netlist. We represent a netlist using simultaneous algebraic equations and solve them based on a novel polynomial reduction method that can be efficiently applied to arithmetic over extension fields $mathbb{F}_{p^m}$, where the characteristic p is larger than two. By using the reverse topological term order to derive the Gröbner basis, our method can complete the verification, even when a target circuit includes bugs. In addition, we introduce an extension of the Galois-Field binary moment diagrams to perform the polynomial reductions faster. Our experimental results show that the proposed method can efficiently verify practical $mathbb{F}_{p^m}$ arithmetic circuits, including those used in modern cryptography. Moreover, we demonstrate that the extended polynomial reduction technique can enable verification that is up to approximately five times faster than the original one.

This paper presents a system for the automatic generation of Galois-field (GF) arithmetic circuits, named the GF Arithmetic Module Generator (GF-AMG). The proposed system employs a graph-based circuit description called the GF Arithmetic Circuit Graph (GF-ACG). First, we present an extension of the GF-ACG to handle GF(pm) (p≥3) arithmetic circuits, which can be efficiently implemented by multiple-valued logic circuits in addition to the conventional binary circuits. We then show the validity of the generation system through the experimental design of GF(pm) multipliers for different p-values. In addition, we evaluate the performance of three types of GF(2m) multipliers and typical GF(pm) multipliers (p≥3) empirically generated by our system. We confirm from the results that the proposed system can generate a variety of GF parallel multipliers, including practical multipliers over GF(pm) having extension degrees greater than 128.

This paper presents an automatic hierarchical formal verification method for arithmetic circuits over Galois fields (GFs) which are dedicated digital circuits for GF arithmetic operations used in cryptographic processors. The proposed verification method is based on a combination of a word-level computer algebra procedure with a bit-level PPRM (Positive Polarity Reed-Muller) expansion procedure. While the application of the proposed verification method is not limited to cryptographic processors, these processors are our important targets because complicated implementation techniques, such as field conversions, are frequently used for side-channel resistant, compact and low power design. In the proposed method, the correctness of entire datapath is verified over GF(2m) level, or word-level. A datapath implementation is represented hierarchically as a set of components' functional descriptions over GF(2m) and their wiring connections. We verify that the implementation satisfies a given total-functional specification over GF(2m), by using an automatic algebraic method based on the Gröbner basis and a polynomial reduction. Then, in order to verify whether each component circuit is correctly implemented by combination of GF(2) operations, i.e. logic gates in bit-level, we use our fast PPRM expansion procedure which is customized for handling large-scale Boolean expressions with many variables. We have applied the proposed method to a complicated AES (Advanced Encryption Standard) circuit with a masking countermeasure against side-channel attack. The results show that the proposed method can verify such practical circuit automatically within 4 minutes, while any single conventional verification methods fail within a day or even more.

This paper presents a graph-based approach to designing arithmetic circuits over Galois fields (GFs) using normal basis representations. The proposed method is based on a graph-based circuit description called Galois-field Arithmetic Circuit Graph (GF-ACG). First, we extend GF-ACG representation to describe GFs defined by normal basis in addition to polynomial basis. We then apply the extended design method to Massey-Omura parallel multipliers which are well known as typical multipliers based on normal basis. We present the formal description of the multipliers in a hierarchical manner and show that the verification time can be greatly reduced in comparison with those of the conventional techniques. In addition, we design GF exponentiation circuits consisting of the Massey-Omura parallel multipliers and an inversion circuit over composite field GF(((22)2)2) in order to demonstrate the advantages of normal-basis circuits over polynomial-basis ones.

This paper proposes a constant-power adder based on multiple-valued logic and its application to cryptographic processors being resistant to side-channel attacks. The proposed adder is implemented in Multiple-Valued Current-Mode Logic (MV-CML). The important feature of MV-CML is that the power consumption can be constant regardless of input values, which makes it possible to prevent power-analysis attacks using dependencies between power consumption and intermediate values or operations of the executed cryptographic algorithms. In this paper, we focus on a multiple-valued Binary Carry-Save adder based on the Positive-Digit (PD) number system and its application to RSA processors. The power characteristic of the proposed design is evaluated with HSPICE simulation using 90 nm process technology. The result shows that the proposed design can achieve constant power consumption with lower performance overhead in comparison with the conventional binary design.

This paper presents a formal approach to verify arithmetic circuits using symbolic computer algebra. Our method describes arithmetic circuits directly with high-level mathematical objects based on weighted number systems and arithmetic formulae. Such circuit description can be effectively verified by polynomial reduction techniques using Grobner Bases. In this paper, we describe how the symbolic computer algebra can be used to describe and verify arithmetic circuits. The advantageous effects of the proposed approach are demonstrated through experimental verification of some arithmetic circuits such as multiply-accumulator and FIR filter. The result shows that the proposed approach has a definite possibility of verifying practical arithmetic circuits.

This paper presents a formal design of arithmetic circuits using an arithmetic description language called ARITH. The key idea in ARITH is to describe arithmetic algorithms directly with high-level mathematical objects (i.e., number representation systems and arithmetic operations/formulae). Using ARITH, we can provide formal description of arithmetic algorithms including those using unconventional number systems. In addition, the described arithmetic algorithms can be formally verified by equivalence checking with formula manipulations. The verified ARITH descriptions are easily translated into the equivalent HDL descriptions. In this paper, we also present an application of ARITH to an arithmetic module generator, which supports a variety of hardware algorithms for 2-operand adders, multi-operand adders, multipliers, constant-coefficient multipliers and multiply accumulators. The language processing system of ARITH incorporated in the generator verifies the correctness of ARITH descriptions in a formal method. As a result, we can obtain highly-reliable arithmetic modules whose functions are completely verified at the algorithm level.

This paper presents an algorithm-level interpretation of fast adder structures in binary/multiple-valued logic. The key idea is to employ a unified representation of addition algorithms called Counter Tree Diagrams (CTDs). The use of CTDs makes it possible to describe and analyze addition algorithms at various levels of abstraction. A high-level CTD represents a network of coarse-grained components associated with multiple-valued logic devices, while a low-level CTD represents a network of primitive components directly mapped onto binary logic devices. The level of abstraction in circuit representation can be changed by decomposition of CTDs. We can derive possible variations of adder structures by decomposing a high-level CTD into low-level CTDs. This paper demonstrates the interpretation of redundant arithmetic adders based on CTDs. We first introduce an extension of CTDs to represent possible redundant arithmetic adders with limited carry propagation. Using the extended version of CTDs, we can classify the conventional adder structures including those using emerging devices into three types in a systematic way.

This letter presents an efficient graph-based evolutionary optimization technique, and its application to the transistor-level design of multiple-valued arithmetic circuits. The key idea is to introduce "circuit graphs with colored terminals" for modeling heterogeneous networks of various components. The potential of the proposed approach is demonstrated through experimental synthesis of a radix-4 signed-digit (SD) full adder circuit.

This paper presents an efficient graph-based evolutionary optimization technique called Evolutionary Graph Generation (EGG), and its application to the design of fast constant-coefficient multipliers using parallel counter-tree architecture. An important feature of EGG is its capability to handle the general graph structures directly in evolution process instead of encoding the graph structures into indirect representations, such as bit strings and trees. This paper also addresses the major problem of EGG regarding the significant computation time required for verifying the function of generated circuits. To solve this problem, a new functional verification technique for arithmetic circuits is proposed. It is demonstrated that the EGG system can create efficient multiplier structures which are comparable or superior to the known conventional designs.

This paper presents a constant-scale-factor radix-2-4-8 CORDIC algorithm for fast vector rotation and sine/cosine computation. The CORDIC algorithm is a well-known hardware algorithm for computing various elementary functions. Due to its sequential nature of computation, however, significant reduction in processing latency is required for real-time signal processing applications. The proposed radix-2-4-8 CORDIC algorithm dynamically changes the radix of computation during operation, and makes possible the reduction in the number of iterations by 37% for 64-bit precision. This paper also describes the hardware implementation of radix-2-4-8 CORDIC unit that can be installed into practical digital signal processors.

This paper presents a new approach to designing arithmetic circuits by using a graph-based evolutionary optimization technique called Evolutionary Graph Generation (EGG). The key idea of the proposed method is to introduce a higher level of abstraction for arithmetic algorithms, in which arithmetic circuit structures are modeled as data-flow graphs associated with specific number representation systems. The EGG system employs evolutionary operations to transform the structure of graphs directly, which makes it possible to generate the desired circuit structure efficiently. The potential capability of EGG is demonstrated through an experiment of generating constant-coefficient multipliers.

In order to apply formal design verification, it is necessary to describe formally and correctly the specification of the circuit under verification. Especially when we apply conventional OBDD-based logic comparison method for verifying combinational circuits, another correct" logic circuits or Boolean formulae must be given as the specification. It is desired to develop an efficient automatic design verification method which interprets specification that can be described easier. This paper provides a new verification method which is useful for combinational circuits such as arithmetic circuits. The proposed method efficiently verifies whether a designed circuit satisfies a specification given by recurrence equations. This enables us to describe easily an error-free specification for arithmetic circuits. To perform verification efficiently using an ordinary OBDD package, an efficient truth-value rotation algorithm is developed. The truthvalue rotation algorithm efficiently generates an OBDD representing f(x + 1 (mod 2n)) from a given OBDD representing f(x). By experiments on SPARC station 10 model 51, it takes 180 secs to generate an OBDD for designed circuit of 23-bit square function, and additional 60 secs is sufficient to finish verifying that it satisfies the specification given by recurrence equations.