Automatic Synthesis of Glue and Interface Automata

If we have a formal specification of participating interfaces, we can synthesise the 'glue'

• RTL glue logic between components for use on target SoC,
• TLM glue between components for modelling,
• Complex switch/router components with filtering,
• Cross-layer glue: TLM to RTL transactors.

Net and method definitions could come from IP-XACT but currently we need a separate mini-language for the protocols:

type protocol_spec_t = 
 | Set of string * string
 | Seq of protocol_spec_t list
 | Conjunction of protocol_spec_t list
 | Disjunction of protocol_spec_t list
;

type net_spec_t =
 | Concrete_enum of string list
 | Symbolic_bitvec of int 
;

let coding_states v = 
   match v with
   | Concrete_enum l   ->  l
   | Symbolic_bitvec _  -> ["dead"; "live"]


(*
 * In a reversed port, the inputs are swapped with the outputs, apart from Always_x forms
 * that do not swap direction (e.g, master clock).
 *)
type netdir_t = Input | Output | Local | Always_input
;