Add a call instruction to HTL. Use it for Icall.

2 files changed, 30 insertions, 3 deletions

diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 620ef14..ca4270b 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -32,8 +32,13 @@ Local Open Scope assocmap.
 
 Definition reg := positive.
 Definition node := positive.
+Definition ident := positive.
 
-Definition datapath := PTree.t Verilog.stmnt.
+Inductive datapath_stmnt :=
+| HTLcall : ident -> list reg -> reg -> datapath_stmnt
+| HTLVstmnt : Verilog.stmnt -> datapath_stmnt.
+
+Definition datapath := PTree.t datapath_stmnt.
 Definition controllogic := PTree.t Verilog.stmnt.
 
 Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
@@ -101,6 +106,16 @@ Inductive state : Type :=
            (m : module)
            (args : list value), state.
 
+Inductive datapath_stmnt_runp:
+  Verilog.fext -> Verilog.reg_associations -> Verilog.arr_associations ->
+  datapath_stmnt -> Verilog.reg_associations -> Verilog.arr_associations -> Prop :=
+(* TODO give it an actual semantics *)
+| stmnt_runp_HTLcall : forall f ar al i args dst,
+    datapath_stmnt_runp f ar al (HTLcall i args dst) ar al
+| stmnt_runp_HTLVstmnt : forall asr0 asa0 asr1 asa1 f stmnt,
+    Verilog.stmnt_runp f asr0 asa0 stmnt asr1 asa1 ->
+    datapath_stmnt_runp f asr0 asa0 (HTLVstmnt stmnt) asr1 asa1.
+
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
     forall g m st sf ctrl data
@@ -121,7 +136,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
         (Verilog.mkassociations basr1 nasr1)
         (Verilog.mkassociations basa1 nasa1) ->
       basr1!(m.(mod_st)) = Some (posToValue st) ->
-      Verilog.stmnt_runp f
+      datapath_stmnt_runp f
         (Verilog.mkassociations basr1 nasr1)
         (Verilog.mkassociations basa1 nasa1)
         data
diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml
index d87b755..fd6cf49 100644
--- a/src/verilog/PrintHTL.ml
+++ b/src/verilog/PrintHTL.ml
@@ -31,6 +31,8 @@ open VericertClflags
 
 let pstr pp = fprintf pp "%s"
 
+let concat = String.concat ""
+
 let rec intersperse c = function
   | [] -> []
   | [x] -> [x]
@@ -42,6 +44,16 @@ let registers a = String.concat "" (intersperse ", " (List.map register a))
 let print_instruction pp (pc, i) =
   fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i)
 
+let pprint_datapath_stmnt i = function
+  | HTLVstmnt s -> pprint_stmnt i s
+  | HTLcall (name, args, dst) -> concat [
+      register dst; " = ";
+      extern_atom name; "("; concat (intersperse ", " (List.map register args)); ");\n"
+    ]
+
+let print_datapath_instruction pp (pc, i) =
+  fprintf pp "%5d:\t%s" pc (pprint_datapath_stmnt 0 i)
+
 let ptree_to_list ptree =
   List.sort
     (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
@@ -54,7 +66,7 @@ let print_module pp id f =
   let datapath = ptree_to_list f.mod_datapath in
   let controllogic = ptree_to_list f.mod_controllogic in
   fprintf pp "datapath {\n";
-  List.iter (print_instruction pp) datapath;
+  List.iter (print_datapath_instruction pp) datapath;
   fprintf pp "  }\n\n  controllogic {\n";
   List.iter (print_instruction pp) controllogic;
   fprintf pp "  }\n}\n\n"