NDLI: Using Lava to design and verify recursive and periodic sorters

Please wait, while we are loading the content...

International Journal on Software Tools for Technology Transfer : Volume 19

International Journal on Software Tools for Technology Transfer : Volume 18

International Journal on Software Tools for Technology Transfer : Volume 17

International Journal on Software Tools for Technology Transfer : Volume 16

International Journal on Software Tools for Technology Transfer : Volume 15

International Journal on Software Tools for Technology Transfer : Volume 14

International Journal on Software Tools for Technology Transfer : Volume 13

International Journal on Software Tools for Technology Transfer : Volume 12

International Journal on Software Tools for Technology Transfer : Volume 11

International Journal on Software Tools for Technology Transfer : Volume 10

International Journal on Software Tools for Technology Transfer : Volume 9

International Journal on Software Tools for Technology Transfer : Volume 8

International Journal on Software Tools for Technology Transfer : Volume 7

International Journal on Software Tools for Technology Transfer : Volume 6

International Journal on Software Tools for Technology Transfer : Volume 5

International Journal on Software Tools for Technology Transfer : Volume 4

International Journal on Software Tools for Technology Transfer : Volume 4, Issue 4, August 2003

International Journal on Software Tools for Technology Transfer : Volume 4, Issue 3, May 2003

Platitudes and attitudes

Preface by the section editor

Higher-level techniques for hardware description and synthesis

A framework for superscalar microprocessor correctness statements

Hierarchical formal verification using a hybrid tool

Proof engineering in the large: formal verification of Pentium®4 floating-point divider

Efficient debugging in a formal verification environment

Using Lava to design and verify recursive and periodic sorters

Refinement-based formal verification with heterogeneous timing

Formal verification of conflict detection algorithms

A framework for distributing object-oriented designs

International Journal on Software Tools for Technology Transfer : Volume 4, Issue 2, February 2003

International Journal on Software Tools for Technology Transfer : Volume 4, Issue 1, October 2002

International Journal on Software Tools for Technology Transfer : Volume 3

International Journal on Software Tools for Technology Transfer : Volume 2

International Journal on Software Tools for Technology Transfer : Volume 1

Using Lava to design and verify recursive and periodic sorters

Content Provider	Springer Nature Link
Author	Claessen, Koen Sheeran, Mary Singh, Satnam
Copyright Year	2003
Abstract	The Lava system is an experimental framework for designing, verifying, and implementing circuits using powerful concepts borrowed from the world of lazy functional programming. We show how the Lava system is used to design and analyse fast sorting circuits for implementation on Field Programmable Gate Arrays (FPGAs). Two types of sorting networks are described, analyzed, and implemented. We present recursive sorting networks and periodic sorting networks based on Batcher’s bitonic merger and on Batcher’s odd even merger. 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 and implementing four sorters on a XilinxVirtexTM-IIFPGA.Performance figures are presented.
Starting Page	349
Ending Page	358
Page Count	10
File Format	PDF
ISSN	14332779
Journal	International Journal on Software Tools for Technology Transfer
Volume Number	4
Issue Number	3
Language	English
Publisher	Springer-Verlag
Publisher Date	2003-05-01
Publisher Place	Berlin Heidelberg
Access Restriction	One Nation One Subscription (ONOS)
Content Type	Text
Resource Type	Article
Subject	Information Systems Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard

Architectural Modeling to Verify Security and Nonfunctional Behavior

Using term rewriting systems to design and verify processors

The use of guidelines to automatically verify Web accessibility

Using term rewriting to verify software

Let’s verify this with Why3

A Socio-Technical Approach to Systems Design

Using DAG transformations to verify Euler/Venn homogeneous and Euler/Venn FOL heterogeneous rules of inference

Efficient finite impulse response filters in massively-parallel recursive systems : Fast recursive systems computation with applications to low-level vision using GPUs

Using Lava to design and verify recursive and periodic sorters

Similar Documents

Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard

Architectural Modeling to Verify Security and Nonfunctional Behavior

Using term rewriting systems to design and verify processors

The use of guidelines to automatically verify Web accessibility

Using term rewriting to verify software

Let’s verify this with Why3

A Socio-Technical Approach to Systems Design

Using DAG transformations to verify Euler/Venn homogeneous and Euler/Venn FOL heterogeneous rules of inference

Efficient finite impulse response filters in massively-parallel recursive systems : Fast recursive systems computation with applications to low-level vision using GPUs

Using Lava to design and verify recursive and periodic sorters