There are natural formal connections between synchronous reactive formalisms and models of synchronous hardware circuits (logical gate shemes and netlists). These similarities have been recently exploited, both to apply optimisation techniques designed for circuits to synchronous processes, and conversely to give constructive causal meaning to circuits.

Achieved Results:

This year we completed our DC2Verilog translator, and performed several experiments with it by submitting the output code to verification systems such as SMV or FPGA_Express (from Synopsys). We wrote a DC2VHDL translator along the same lines, and made it available to several industrial b-test users. This in turn provided new ideas for translation at behavioural/RTL level for structured programs, isolating control path and data path (in a faction actually very similar to the way data and control are combined between the SC and DC formats).

The tools developped in this task are now freely downloadable, together with the documentation on the translation scheme.