Formal Specification of the Four Phase Handshake

let four_phase_handshake_nets = 
  [ ("Strobe", Output, Concrete_enum ["true"; "false"]); 
    ("Ack",    Input,  Concrete_enum ["true"; "false"]); 
    ("DL",     Output, Symbolic_bitvec (8) )
  ]


let four_phase_handshake_idle =  
 [
  ("dead", "DL");
  ("false", "Strobe");
  ("false", "Ack")
 ]
;

let four_phase_handshake_protocol =  
 Seq[
  Set("live", "DL");
  Set("true", "Strobe");
  Set("true", "Ack");
  Set("dead", "DL");
  Set("false", "Strobe");
  Set("false", "Ack")
  ]
;

(* Overall composition of the protocol in a direction-agnostic form *)
let fourphase = ("4P", four_phase_handshake_nets, four_phase_handshake_idle, four_phase_handshake_protocol)