HOME   PREV   NEXT (Formal Specification of a Holding Register)

Formal Specification of the TLM Call with one argument

(* The net directions are for the male (data sending) side but the protocol specification is unsexed. *)

let tlm1_handshake_nets = 
  [ ("call",   Input,  Concrete_enum ["idle"; "active"]); 
    ("DH",     Input, Symbolic_bitvec (8) )
  ]


let tlm1_handshake_idle =  
 [
  ("dead", "DH");
  ("idle", "call");
 ]
;

(* This is for a TLM entry point that is a data sink.  If it were a source, the data would be live as the call goes idle. *)
let tlm1_handshake_protocol =  
 Seq[
  Set("live", "DH");
  Set("active", "call");
  Set("dead", "DH");
  Set("idle", "call");
  ]
;

The product machine has a state transition when the TLM caller puts its data live, but of course the glue logic will not see this until the call state goes live, so it cannot really make a transition at that point. Therefore a pre-processing of the participating state machines is live that elides the two operations into one is appropriate.

This is for a TLM entry point that is a data sink. If it were a source, the data would be live as the call goes idle.

In the example live and active occur at once, whereas the dead transition is not elided, since the glue will make an active transition to read out the contents of the register. In a complementary transactor where the TLM is a write upcall, that has the same overall pattern, it is the going dead transition that cannot be seen by the glue, and the going dead and call going idle are elided in the preprocessing.

(* Overall composition of the protocol in a direction-agnostic form *)
let tlm1 = ("TLM1", tlm1_handshake_nets, tlm1_handshake_idle, tlm1_handshake_protocol)