By the same authors

From the same journal

Correct hardware synthesis

Research output: Contribution to journalArticle



Publication details

JournalActa Informatica
DatePublished - Dec 2011
Issue number7-8
Number of pages34
Pages (from-to)363-396
Original languageEnglish


This paper presents an algebraic compilation approach to the correct synthesis (compilation into hardware) of a synchronous language with shared variables and parallelism. The synthesis process generates a hardware component that implements the source program by means of gradually reducing it into a highly parallel state-machine. The correctness of the compiler follows by construction from the correctness of the transformations involved in the synthesis process. Each transformation is proved sound from more basic algebraic laws of the source language; the laws are themselves formally derived from a denotational semantics expressed in the Unified Theories of Programming. The proposed approach is based on previous efforts that handle both software and hardware compilation, in a pure algebraic style, but the complexity of our source language demanded significant adaptations and extensions to the existing approaches.

Discover related content

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

View graph of relations