By the same authors

CSP/FDR2 to Handel-C translation

Research output: Book/ReportOther report

Author(s)

Department/unit(s)

Publication details

DatePublished - 1 Jun 2003
PublisherThe Department of Computer Science, University of York
VolumeYCS-2003-357
Original languageUndefined/Unknown

Publication series

NameDepartment of Computer Science Technical Report
PublisherDepartment of Computer Science, University of York
VolumeYCS-2003-357

Abstract

This report is adapted from a study performed for AWE in 2001 by the author while at Logica. It investigates the feasibility of using the CSP specification language and FDR2 model-checking tool, and Handel-C programming language, in combination, with FDR2 as a front-end specification and proof tool, then automatically translating the formal designs into executable Handel-C. Such an approach could provide a development path from an abstract specification to a correct executable implementation running on an FPGA.

This report contains the following

a) Identification of a subset of CSP that maps closely to Handel-C. That subset is large enough to accommodate a large subset of CSP specifications.

b) A sketch of a mapping from the identified CSP subset to Handel-C, suitable to be performed automatically. As proof-of-concept, the identified mappings are hand-applied to two example CSP specifications to produce Handel-C implementations.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations