With the rise of new technologies the demand for efficient cryptographic hardware and design space exploration is rising. This work presents a framework for the automated synthesis of datapaths that use tower-field constructions for finite field arithmetic. The key idea is a novel encoding of the underlying algebraic structure with the dual view as both a finite field and a vector space. The framework uses symbolic computation capabilities of GAP to generate the expressions, needed for hardware implementations, on-the-fly, and compiles them into synthesizable datapaths, test-vectors and testbenches. It supports implementation of expressions defined over different sized finite fields, tower fields, or even several isomorphic finite fields within the same hardware module.

A binary de Bruijn sequence is a sequence of period 2n in which every binary n-tuple occurs exactly once in each period. A de Bruijn sequence has good randomness properties, such as long period, ideal tuple distribution, and high linear complexity, and can be generated by a nonlinear feedback shift register (NLFSR). Finding an efficient NLFSR that can generate a de Bruijn sequence with a long period is a significant challenge. “Composited construction” is a technique for constructing a de Bruijn sequence of period 2n+kby an NLFSR from a de Bruijn sequence of period 2nthrough a composition operation repeatedly applying k times. The goal of this article is to further investigate the composited construction of de Bruijn sequences with efficient hardware implementations, and determine randomness properties such as linear complexity. Our contributions in this article are as follows. First, we present a generalized construction of composited de Bruijn sequences that is constructed by adding a combination of conjugate pairs of different lengths in the feedback function of the composited construction, which results in generating a class of de Bruijn sequences of size 2k, whereas the original composited construction can generate only two sequences. Second, we investigate the linear complexity and the correlation property of the new class of de Bruijn sequences. We prove theoretically that the linear complexity of this class of de Bruijn sequences is optimal or close to optimal. Interestingly, we also prove that the linear complexities of all the sequences of this class are equal, which strengthens Etzion's conjecture (JCTA 1985, IEEE-IT 1999) about the number of de Bruijn sequences with equal linear complexity. This is the first known construction of de Bruijn sequences of an arbitrarily long period whose linear complexities are determined theoretically. Finally, we implement our construction in hardware to demonstrate its practicality. We synthesize our implementations for a 65 nm ASIC and a Xilinx Spartan FPGA and present hardware areas, and performances of de Bruijn sequences of periods in the range of 2160to 21056. For instance, a class of de Bruijn sequences of period 2160(resp. 2288) can be implemented with an area of 3.43 (resp. 6.71) kGEs in 65 nm ASIC, and 83 (resp. 229) slices in Spartan6 FPGA.

This paper explores tower field constructions and hardware optimizations for the WG-16 stream cipher. The constructions${\mathbb {F}}_{(((2^2)^2)^2)^2}$and${\mathbb {F}}_{(2^{4})^4}$were chosen because their small subfields enable high speed arithmetic implementations and their regularity provides flexibility in pipeline granularity. A design methodology is presented where the tower field constructions guide how to proceed systematically from algebraic optimizations, through initial hardware implementation, selection of submodules, pipelining, and finally detailed hardware optimizations to increase clock speed. The highest frequency WG(16, 32) keystream generator, obtained for the 65 nm ASIC library, reached a clock speed of 2.44 GHz at 26.3 kGE, and the smallest area keystream generator achieved a clock speed of 0.33 GHz at 9.9 kGE. The highest frequency FPGA implementation on a Xilinx Spartan 6 reached a clock speed of 256 MHz using 631 slices. In addition, the paper demonstrates that LFSR feedback polynomials can be optimized to increase security without hurting performance, and retiming optimizations can be used to increase clock speed without increasing area.

A binary de Bruijn sequence with period 2nis a sequence in which every tuple of n bits occurs exactly once. De Bruijn sequence generators have randomness properties that make them attractive for pseudorandom number generators and as building blocks for stream ciphers. Unfortunately, it is very difficult to find de Bruijn sequence generators with long periods (e.g., 2128) and most known de Bruijn sequence generators are computationally quite expensive. In this article, we present “OcDeb-k-n” and the first hardware implementation of de Bruijn sequence generators. OcDeb-k-n efficiently computes a composited de Bruijn sequence where k levels of composition are added to a de Bruijn sequence of period 2n. Numerically, OcDeb reduces the bit operations used for computing the feedback function significantly from Θ(k2+ nk) to Θ(k log k + logn). Furthermore, it enables efficient parallelization and hardware retiming. Comprehensive result analysis is conducted for 65 nm ASIC technology. For example, OcDeb-32-32 has an area of 643 GE with 1.45 Gbps performance, and with parallelization it generates up to 25.4 Gbps at the cost of 4,787 GE. The area of OcDeb-512-32 generating a de Bruijn sequence of period 2544is 7,304 GE and the performance is 1.25 Gbps.

The Forte formal verification environment for datapath-dominated hardware is described. Forte has proven to be effective in large-scale industrial trials and combines an efficient linear-time logic model-checking algorithm, namely the symbolic trajectory evaluation (STE), with lightweight theorem proving in higher-order logic. These are tightly integrated in a general-purpose functional programming language, which both allows the system to be easily customized and at the same time serves as a specification language. The design philosophy behind Forte is presented and the elements of the verification methodology that make it effective in practice are also described.

This article describes a technique that simplifies the design of pipelined circuits automates the specification and verification of structural-hazard and datapath correctness properties for pipelined circuits. The technique is based upon a template for pipeline stages, a control-circuit cell library, a decomposition of structural hazard and datapath correctness into a collection of simple properties, and a prototype design tool that generates verification scripts for use by external tools. Our case studies include scalar and superscalar implementations of a 32-bit OpenRISC integer microprocessor.

This paper describes a strategy for verifying data-hazard correctness of out-of-order processors that implement register-renaming. We define a set of predicates to characterize register-renaming techniques and provide a set of model-checking obligations that are sufficient to guarantee that a register-renaming technique satisfies data-hazard correctness. We demonstrate how two register renaming techniques (retirement-register-file and dual-RAT) instantiate our predicates, and present model checking results for the Dual-RAT technique, which is based on the Intel Pentium 4 processor.

Contemporary microprocessors implement many iterative algorithms. For example, the front-end of a microprocessor repeatedly fetches and decodes instructions while updating internal state such as the program counter; floating-point circuits perform divide and square root computations iteratively. Iterative algorithms often have complex implementations because of performance optimizations like result speculation, re-timing and circuit redundancies. Verifying these iterative circuits against high-level specifications requires two steps: reasoning about the algorithm itself and verifying the implementation against the algorithm. In this paper we discuss the verification of four iterative circuits from Intel microprocessor designs. These verifications were performed using Forte, a custom-built verification system; we discuss the Forte features necessary for our approach. Finally, we discuss how we maintained these proofs in the face of evolving design implementations.

We describe the use of parametric representations of Boolean predicates to encode data-space constraints and significantly extend the capacity of formal verification.The constraints are used to decompose verifications by sets of case splits and to restrict verifications by validity conditions.Our technique is applicable to any symbolic simulator.We illustrate our technique on state-of-the-art Intel (R) designs, without removing latches or modifying the circuits in any way.

We describe the verification of the IM: a large, complex (12,000gates and 1100 latches) circuit that detects and marks the boundariesbetween Intel architecture (IA-32) instructions. We verified agate-level model of the IM against an implementation-independentspecification of IA-32 instruction lengths. We used theorem provingto to derive 56 model-checking runs and to verify that the model-checkingruns imply that the IM meets the specification for all possiblesequences of IA-32 instructions. Our verification discoveredeight previously unknown bugs.

Floating-point circuits are notoriously difficult to design and verify. For verification, simulation barely offers adequate coverage, conventional model-checking techniques are infeasible, and theorem-proving based verification is not sufficiently mature. In this paper we present the formal verification of a radix-eight, pipelined, IEEE double-precision floating-point multiplier. The verification was carried out using a mixture of model-checking and theorem-proving techniques in the Voss hardware verification system. By combining model-checking and theorem-proving we were able to build on the strengths of both areas and achieve significant results with a reasonable amount of effort.

We describe the verification of a logic synthesis tool with the Nuprl proof development system. The logic synthesis tool, Pbs, implements the weak division algorithm. Pbs consists of approximately 1000 lines of code implemented in a functional subset of Standard ML. It is a proven and usable implementation and is an integral part of the Bedroc high level synthesis system. The program was verified by embedding the subset of Standard ML in Nuprl and then verifying the correctness of the implementation of Pbs in the Nuprl logic. The proof required approximately 500 theorems. In the process of verifying Pbs we developed a consistent approach for using a proof development system to reason about functional programs. The approach hides implementation details and uses higher order theorems to structure proofs and aid in abstract reasoning. Our approach is quite general, should be applicable to any higher order proof system, and can aid in the future verification of large software implementations.>

We describe PBS, a formally proven implementation of multi-level logic synthesis based on the weak division algorithm. We have proved that for all legal input circuits, PBS generates an output circuit that is functionally correct and has minimal size. PBS runs on large examples in reasonable time for a prototype system. PBS, was verified using the Nuprl proof development system. The proof of PBS, which required several months, was well worth the effort since the benefits are realized every time the program is run. When engineers use a verified synthesis tool, they get the increased confidence of applying formal methods to their designs without the cost of varying each design produced.>

We present a framework for designing control circuitry for pipelined circuits. Our framework supports any mixture of data-dependent, data-stationary and time-stationary control for pipelines with out-of-order execution. There are four parameters to the framework: (1) Protocol schemes describe how transactions are transferred between stages in the pipeline. (2) Arbitration schemes specify how to prevent and/or handle structural hazards in the pipeline. (3) Control schemes determine how transactions are routed through the pipeline and how stages know what operation to perform. (4) Ordering schemes describe a method for matching up transactions as they leave the pipeline with transactions that entered the pipeline. Based on our framework we have developed an algorithm for compiling the control circuitry for a wide class of pipelines from a high-level description of the schedule for the pipeline.>

The correctness of a logic synthesis system is implemented and proved. The algorithm is based on the weak division algorithm for Boolean simplification previously presented. The implementation is in the programming language ML; and the proof is in the Nuprl proof development system. This study begins with a proof of the algorithm previously presented and extends it to a level of detail sufficient for proving the implementation of the system. In the process of developing the proof many definitions presented in previous accounts of the algorithms were clarified, and several errors in the implementation were discovered. The result is that the designs generated by the implementation can be claimed to be correct by construction, since the correctness of the system was proven.>