Higher-Level Hardware Synthesis of the KASUMI Algorithm

Programmable Logic Devices (PLDs) continue to grow in size and currentlycontain several millions of gates. At the same time, researcheffort is going into higher-level hardware synthesis methodologiesfor reconfigurable computing that can exploit PLDtechnology. In this paper, we explore the effectiveness and extendone such formal methodology in the design of massively parallelalgorithms. We take a step-wise refinement approach to thedevelopment of correct reconfigurable hardware circuits fromformal specifications. A functional programming notation is usedfor specifying algorithms and for reasoning about them. Thespecifications are realised through the use of a combination offunction decomposition strategies, data refinement techniques, andoff-the-shelf refinements based upon higher-order functions. Theoff-the-shelf refinements are inspired by the operators ofCommunicating Sequential Processes (CSP) and map easilyto programs in Handel-C (a hardware descriptionlanguage). The Handel-C descriptions are directlycompiled into reconfigurable hardware. The practical realisationof this methodology is evidenced by a case studying the thirdgeneration mobile communication security algorithms. Theinvestigated algorithm is the KASUMI block cipher. Inthis paper, we obtain several hardware implementations withdifferent performance characteristics by applying differentrefinements to the algorithm. The developed designs are compiledand tested under Celoxica's RC-1000 reconfigurable computer with its 2million gates Virtex-E FPGA. Performance analysis and evaluation ofthese implementations are included.