HOME   PREV   NEXT (Formal Specification of the Four Phase Handshake)

Automatic Synthesis of Glue and Interface Automata

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

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