The Design and Verification of a Sorter Core

  • Koen Claessen
  • Mary Sheeran
  • Satnam Singh
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


We show how the Lava system is used to design and analyse fast sorting circuits for implementation on Field Programmable Gate Arrays (FPGAs). We present both recursive and periodic sorting networks, based on recursive merging networks such as Batcher’s bitonic and odd-even mergers. We show how a design style that concentrates on capturing connection patterns gives elegant generic circuit descriptions. This style aids circuit analysis and also gives the user fine control of the final layout on the FPGA. We demonstrate this by analysing andd implementing four sorters on a Xilinx Virtex-II™ FPGA. Performance figures are presented.


Field Programmable Gate Array Connection Pattern Input List Sorting Network Wiring Pattern 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    K.E. Batcher. Sorting networks and their applications. In AFIPS Spring Joint Computing Conference, volume 32, 1969.Google Scholar
  2. 2.
    E.R. Canfield and S.G. Williamson. A sequential sorting network analagous to the Batcher merge. In Linear and Multilinear Algebra, 29, pages 43–51, 1991.zbMATHMathSciNetCrossRefGoogle Scholar
  3. 3.
    Koen Claessen and Mary Sheeran. A tutorial on Lava: A hardware description and verification system. Available from, 2000.
  4. 4.
    M. Dowd, Y. Perl, L. Rudolph, and M. Saks. The periodic balanced sorting network. JACM, 36:738–757, 1989.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Geraint Jones and Mary Sheeran. The study of butterflies. In Graham Birtwistle, editor, Proc. 4th Banff Workshop on Higher Order. Springer Workshops in Computing, 1991.Google Scholar
  6. 6.
    Simon Peyton Jones, John Hughes, (editors), Lennart Augustsson, Dave Barton, Brian Boutel, Warren Burton, Joseph Fasel, Kevin Hammond, Ralf Hinze, Paul Hu-dak, Thomas Johnsson, Mark Jones, John Launchbury, Erik Meijer, John Peterson, Alastair Reid, Colin Runciman, and Philip Wadler. Report on the Programming Language Haskell 98, a Non-strict, Purely Functional Language. Available from, February 1999.
  7. 7.
    D.E. Knuth. Sorting and Searching, vol. 3 of The Art of Computer Programming. Addison-Wesley, 1973.Google Scholar
  8. 8.
    Carl Johan Lillieroth and Satnam Singh. Formal verification of FPGA cores. Nordic Journal of Computing, 6:299–319, 1999.zbMATHGoogle Scholar
  9. 9.
    Mary Sheeran. Sorts of butterflies. In Graham Birtwistle, editor, Proc. 4th Banff Workshop on Higher Order. Springer Workshops in Computing, 1991.Google Scholar
  10. 10.
    Mary Sheeran. Puzzling permutations. In Proc. Glasgow Functional Programming Workshop, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Koen Claessen
    • 1
  • Mary Sheeran
    • 1
  • Satnam Singh
    • 2
  1. 1.Chalmers University of TechnologyUSA
  2. 2.Xilinx, Inc.USA

Personalised recommendations