1 files changed, 159 insertions, 32 deletions

diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 8cebbfd..f16aef5 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -31,6 +31,7 @@ Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.AssocMap.
 Require Import vericert.hls.Array.
+Require Import vericert.common.Maps.
 Require vericert.hls.Verilog.
 
 Local Open Scope positive.
@@ -45,15 +46,20 @@ 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.
+Definition datapath_stmnt := Verilog.stmnt.
+Definition datapath := PTree.t datapath_stmnt.
+Definition control_stmnt := Verilog.stmnt.
+Definition controllogic := PTree.t control_stmnt.
 
 Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
   forall p0 : positive,
     In p0 (map fst (Maps.PTree.elements m)) ->
     (Z.pos p0 <= Integers.Int.max_unsigned)%Z.
 
+Definition ram_ordering a b c d e f := a < b < c /\ c < d < e /\ e < f.
+
 Record ram := mk_ram {
   ram_size: nat;
   ram_mem: reg;
@@ -63,15 +69,26 @@ Record ram := mk_ram {
   ram_wr_en: reg;
   ram_d_in: reg;
   ram_d_out: reg;
-  ram_ordering: (ram_addr < ram_en
-                 /\ ram_en < ram_d_in
-                 /\ ram_d_in < ram_d_out
-                 /\ ram_d_out < ram_wr_en
-                 /\ ram_wr_en < ram_u_en)
+  ram_ordering_wf: ram_ordering ram_addr ram_en ram_d_in ram_d_out ram_wr_en ram_u_en
 }.
 
 Definition module_ordering a b c d e f g := a < b < c /\ c < d < e /\ e < f < g.
 
+Inductive controlsignal : Type :=
+  | ctrl_finish : controlsignal
+  | ctrl_return : controlsignal
+  | ctrl_start : controlsignal
+  | ctrl_reset : controlsignal
+  | ctrl_clk : controlsignal
+  | ctrl_param (idx : nat) : controlsignal.
+
+Definition controlsignal_sz (s : controlsignal) : nat :=
+  match s with
+  | ctrl_param _ => 32
+  | ctrl_return => 32
+  | _ => 1
+  end.
+
 Record module: Type :=
   mkmodule {
     mod_params : list reg;
@@ -88,6 +105,9 @@ Record module: Type :=
     mod_clk : reg;
     mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl);
     mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl);
+    (** Map from registers in this module to control registers in other modules.
+        These will be mapped to the same verilog register. *)
+    mod_externctrl : AssocMap.t (ident * controlsignal);
     mod_ram : option ram;
     mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath;
     mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk;
@@ -108,31 +128,59 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
 Definition empty_stack (m : module) : Verilog.assocmap_arr :=
   (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)).
 
+
+Definition prog_modmap (p : HTL.program) :=
+  PTree_Properties.of_list (Option.map_option
+                               (fun a => match a with
+                                      | (ident, (AST.Gfun (AST.Internal f))) => Some (ident, f)
+                                      | _ => None
+                                      end)
+                               (AST.prog_defs p)).
+
+Lemma max_pc_wf :
+  forall T m, (Z.pos (max_pc_map m) <= Integers.Int.max_unsigned)%Z ->
+            @map_well_formed T m.
+Proof.
+  unfold map_well_formed. intros.
+  exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x.
+  apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B.
+  unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst.
+  simplify. transitivity (Z.pos (max_pc_map m)); eauto.
+Qed.
+
 (** * Operational Semantics *)
 
 Definition genv := Globalenvs.Genv.t fundef unit.
 
+Definition find_func {F V} (ge : Globalenvs.Genv.t F V) (symb : AST.ident) : option F :=
+  match Globalenvs.Genv.find_symbol ge symb with
+  | None => None
+  | Some b => Globalenvs.Genv.find_funct_ptr ge b
+  end.
+
 Inductive stackframe : Type :=
-  Stackframe :
-    forall  (res : reg)
-            (m : module)
-            (pc : node)
-            (reg_assoc : Verilog.assocmap_reg)
-            (arr_assoc : Verilog.assocmap_arr),
-      stackframe.
+  Stackframe : forall (mid : ident)
+                 (m : module)
+                 (st : node)
+                 (reg_assoc : Verilog.assocmap_reg)
+                 (arr_assoc : Verilog.assocmap_arr),
+    stackframe.
 
 Inductive state : Type :=
 | State :
     forall (stack : list stackframe)
+           (mid : ident)
            (m : module)
            (st : node)
            (reg_assoc : Verilog.assocmap_reg)
            (arr_assoc : Verilog.assocmap_arr), state
 | Returnstate :
     forall (res : list stackframe)
+           (mid : ident) (** Name of the callee *)
            (v : value), state
 | Callstate :
     forall (stack : list stackframe)
+           (mid : ident)
            (m : module)
            (args : list value), state.
 
@@ -172,7 +220,7 @@ Inductive exec_ram:
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
-    forall g m st sf ctrl data
+    forall g mid m st sf ctrl_stmnt data_stmnt
       asr asa
       basr1 basa1 nasr1 nasa1
       basr2 basa2 nasr2 nasa2
@@ -182,19 +230,19 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       asr!(mod_reset m) = Some (ZToValue 0) ->
       asr!(mod_finish m) = Some (ZToValue 0) ->
       asr!(m.(mod_st)) = Some (posToValue st) ->
-      m.(mod_controllogic)!st = Some ctrl ->
-      m.(mod_datapath)!st = Some data ->
+      m.(mod_controllogic)!st = Some ctrl_stmnt ->
+      m.(mod_datapath)!st = Some data_stmnt ->
       Verilog.stmnt_runp f
         (Verilog.mkassociations asr empty_assocmap)
         (Verilog.mkassociations asa (empty_stack m))
-        ctrl
+        ctrl_stmnt
         (Verilog.mkassociations basr1 nasr1)
         (Verilog.mkassociations basa1 nasa1) ->
       basr1!(m.(mod_st)) = Some (posToValue st) ->
       Verilog.stmnt_runp f
         (Verilog.mkassociations basr1 nasr1)
         (Verilog.mkassociations basa1 nasa1)
-        data
+        data_stmnt
         (Verilog.mkassociations basr2 nasr2)
         (Verilog.mkassociations basa2 nasa2) ->
       exec_ram
@@ -207,26 +255,69 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       asa' = Verilog.merge_arrs nasa3 basa3 ->
       asr'!(m.(mod_st)) = Some (posToValue pstval) ->
       (Z.pos pstval <= Integers.Int.max_unsigned)%Z ->
-      step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
+      step g
+           (State sf mid m st     asr  asa) Events.E0
+           (State sf mid m pstval asr' asa')
 | step_finish :
-    forall g m st asr asa retval sf,
+    forall g m st asr asa retval sf mid,
     asr!(m.(mod_finish)) = Some (ZToValue 1) ->
     asr!(m.(mod_return)) = Some retval ->
-    step g (State sf m st asr asa) Events.E0 (Returnstate sf retval)
+
+    step g
+         (State sf mid m st asr asa) Events.E0
+         (Returnstate sf mid retval)
+| step_initcall :
+    forall g callerid caller st asr asa sf callee_id callee callee_reset callee_params callee_param_vals,
+    find_func g callee_id = Some (AST.Internal callee) ->
+
+    caller.(mod_externctrl)!callee_reset = Some (callee_id, ctrl_reset) ->
+    (forall n param, nth_error callee_params n = Some param ->
+          caller.(mod_externctrl)!param = Some (callee_id, ctrl_param n)) ->
+
+    (* The fact that this is the only condition on the current state to trigger
+       a call introduces non-determinism into the semantics. The semantics
+       permit initiating a call from any state where a reset has been set to 0.
+     *)
+    asr!callee_reset = Some (ZToValue 0) ->
+    callee_param_vals = List.map (fun p => asr#p) callee_params ->
+
+    step g
+         (State sf callerid caller st asr asa) Events.E0
+         (Callstate (Stackframe callerid caller st asr asa :: sf)
+                    callee_id callee callee_param_vals)
+
 | step_call :
-    forall g m args res,
-      step g (Callstate res m args) Events.E0
-           (State res m m.(mod_entrypoint)
+    forall g mid m args res,
+      step g
+           (Callstate res mid m args) Events.E0
+           (State res mid m m.(mod_entrypoint)
              (AssocMap.set (mod_reset m) (ZToValue 0)
               (AssocMap.set (mod_finish m) (ZToValue 0)
                (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint))
                 (init_regs args m.(mod_params)))))
              (empty_stack m))
+
 | step_return :
-    forall g m asr asa i r sf pc mst,
-      mst = mod_st m ->
-      step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
-           (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa).
+    forall g callerid caller asr asa callee_id callee_return callee_finish i sf pc mst,
+      mst = mod_st caller ->
+
+      caller.(mod_externctrl)!callee_return = Some (callee_id, ctrl_return) ->
+      caller.(mod_externctrl)!callee_finish = Some (callee_id, ctrl_finish) ->
+
+      step g
+           (Returnstate (Stackframe callerid caller pc asr asa :: sf) callee_id i) Events.E0
+           (State sf callerid caller pc
+                  (asr # mst <- (posToValue pc) # callee_finish <- (ZToValue 1) # callee_return <- i)
+                  asa)
+| step_finish_reset :
+    forall g sf mid mid' m st asr asa fin,
+      asr ! fin = Some (ZToValue 1) ->
+      (mod_externctrl m) ! fin = Some (mid', ctrl_finish) ->
+      step g
+           (State sf mid m st asr                        asa) Events.E0
+           (State sf mid m st (asr # fin <- (ZToValue 0)) asa).
+
+
 #[export] Hint Constructors step : htl.
 
 Inductive initial_state (p: program): state -> Prop :=
@@ -235,12 +326,12 @@ Inductive initial_state (p: program): state -> Prop :=
       Globalenvs.Genv.init_mem p = Some m0 ->
       Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
       Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) ->
-      initial_state p (Callstate nil m nil).
+      initial_state p (Callstate nil p.(AST.prog_main) m nil).
 
 Inductive final_state : state -> Integers.int -> Prop :=
-| final_state_intro : forall retval retvali,
+| final_state_intro : forall retval mid retvali,
     retvali = valueToInt retval ->
-    final_state (Returnstate nil retval) retvali.
+    final_state (Returnstate nil mid retval) retvali.
 
 Definition semantics (m : program) :=
   Smallstep.Semantics step (initial_state m) final_state
@@ -352,3 +443,39 @@ Definition max_list_dec (l: list reg) (st: reg) : {Forall (Pos.gt st) l} + {True
     ); auto.
   apply max_list_correct. apply Pos.ltb_lt in e. lia.
 Qed.
+
+Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}.
+  refine (match bool_dec ((a <? b) && (b <? c) && (c <? d)
+                          && (d <? e) && (e <? f) && (f <? g))%positive true with
+          | left t => left _
+          | _ => _
+          end); auto.
+  simplify; repeat match goal with
+                   | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H
+                   end; unfold module_ordering; auto.
+Defined.
+
+Definition decide_ram_ordering a b c d e f : {ram_ordering a b c d e f} + {True}.
+  refine (match bool_dec ((a <? b) && (b <? c) && (c <? d)
+                          && (d <? e) && (e <? f))%positive true with
+          | left t => left _
+          | _ => _
+          end); auto.
+  simplify; repeat match goal with
+                   | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H
+                   end; unfold ram_ordering; auto.
+Defined.
+
+Definition decide_ram_wf (clk : reg) (mr : option HTL.ram) :
+  {forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive} + {True}.
+  refine (
+      match mr with
+      | Some r =>
+        match (plt clk (ram_addr r)) with
+        | left LE => left _
+        | _ => right I
+        end
+      | None => left _
+      end).
+  all: crush.
+Defined.