Merge branch 'michalis' of https://github.com/mpardalos/vericert into michalis-merge

1 files changed, 36 insertions, 4 deletions

diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index c8a0041..4e8c08e 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -42,9 +42,19 @@ Local Open Scope assocmap.
 
 Definition reg := positive.
 Definition node := positive.
+Definition ident := positive.
 
-Definition datapath := PTree.t Verilog.stmnt.
-Definition controllogic := PTree.t Verilog.stmnt.
+Inductive datapath_stmnt :=
+| HTLfork : ident -> list reg -> datapath_stmnt
+| HTLjoin : ident -> reg -> datapath_stmnt
+| HTLDataVstmnt : Verilog.stmnt -> datapath_stmnt.
+
+Inductive control_stmnt :=
+| HTLwait : ident -> reg -> Verilog.expr -> control_stmnt
+| HTLCtrlVstmnt : Verilog.stmnt -> control_stmnt.
+
+Definition datapath := PTree.t datapath_stmnt.
+Definition controllogic := PTree.t control_stmnt.
 
 Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
   forall p0 : positive,
@@ -111,6 +121,28 @@ 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_HTLfork : forall f ar al i args,
+    datapath_stmnt_runp f ar al (HTLfork i args) ar al
+| stmnt_runp_HTLcall : forall f ar al i dst,
+    datapath_stmnt_runp f ar al (HTLjoin i dst) ar al
+| stmnt_runp_HTLDataVstmnt : forall asr0 asa0 asr1 asa1 f stmnt,
+    Verilog.stmnt_runp f asr0 asa0 stmnt asr1 asa1 ->
+    datapath_stmnt_runp f asr0 asa0 (HTLDataVstmnt stmnt) asr1 asa1.
+
+Inductive control_stmnt_runp:
+  Verilog.fext -> Verilog.reg_associations -> Verilog.arr_associations ->
+  control_stmnt -> Verilog.reg_associations -> Verilog.arr_associations -> Prop :=
+(* TODO give it an actual semantics *)
+| stmnt_runp_HTLwait : forall f ar al i reg expr,
+    control_stmnt_runp f ar al (HTLwait i reg expr) ar al
+| stmnt_runp_HTLCtrlVstmnt : forall asr0 asa0 asr1 asa1 f stmnt,
+    Verilog.stmnt_runp f asr0 asa0 stmnt asr1 asa1 ->
+    control_stmnt_runp f asr0 asa0 (HTLCtrlVstmnt stmnt) asr1 asa1.
+
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
     forall g m st sf ctrl data
@@ -124,14 +156,14 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       asr!(m.(mod_st)) = Some (posToValue st) ->
       m.(mod_controllogic)!st = Some ctrl ->
       m.(mod_datapath)!st = Some data ->
-      Verilog.stmnt_runp f
+      control_stmnt_runp f
         (Verilog.mkassociations asr empty_assocmap)
         (Verilog.mkassociations asa (empty_stack m))
         ctrl
         (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