package rfsm

Static elaboration

This step takes a typed program consisting of

• types, functions and constant declarations
• global IO declarations
• typed FSM instances and produce a representation, consisting of
• the same types, functions and constant declarations
• a elaborated set of FSM instances In the latter i) the formal IOs of the corresponding model have been bound to the global IOs; for ex, if the input program is like fsm model f (in x: bool, out y: int, ...) ... rules | q -> q' when h.(x=1) with y:=0 ... ... input X: bool output Y: int ... fsm f0 = f(X,Y,...) then, the model describing f0 in the result representation will be like fsm model f (in X: bool, out X: int, ...) ... rules | q -> q' when h.(X=1) with Y:=0 ... Note: the compatibility between formal and actual IOs has already been checked by the typing phase. ii) the (generic) parameters have been replaced by their actual value for ex, if the input program is like fsm model f <n: int> (in x: int<n>, ...) ... vars z: int ... rules | q -> q' when h.(x=1).(z<n) ... ... input X: int<8> ... fsm f8 = f<8>(X,,...) then, the model describing f8 in the result representation will be like fsm model f (in X: int<8>, ...) ... vars z: int ... rules | q -> q' when h.(X=1).(z<8) ... Note: the compatibility between formal and actual parameters has already been checked by the typing phase. iii) Moore-style descriptions (with output assignations attached to states) have been turned to to Mealy-style ones (with output assignations attached to transitions). for ex, if the input program is like fsm model f (out o: int, ...) states { ..., q' with o=1 } ... rules | q -> q' ... ... fsm f0 = f(...) then, the model describing f0 in the result representation will be like fsm model f (out o: int, ...) states { ..., q } ... rules | q -> q' with o:=1 ...

The elaboration step also computes the dependency order induced by shared variables between FSMs. An FSM f depends on another FSM f' if f reads a variable that is written by f'. Note that this order is here purely static because all rules are considered for reading and writing, independentely of the actual FSM state. The resulting order will used by the SystemC (and possibly other) backend to implement instantaneous broadcast using delta cycles.