From 8e012d446357cd4f7f1ef25814ea7891c45086ae Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 29 Apr 2020 18:04:27 +0100
Subject: Add documentation and conform to specification

---
 src/translation/Veriloggen.v | 65 ++++++++++++++++++++++++++++----------------
 1 file changed, 41 insertions(+), 24 deletions(-)

(limited to 'src')

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index 6aa94df..aa12a67 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -359,6 +359,10 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
     | _, _, _ => Error (Errors.msg "Veriloggen.add_instr")
     end.
 
+(** Add a register to the state without changing the [st_freshreg], as this
+should already be the right value.  This can be assumed because the max register
+is taken from the RTL code. *)
+
 Definition add_reg (r: reg) (s: state) : state :=
   mkstate (st_freshreg s)
           (st_freshstate s)
@@ -398,6 +402,9 @@ Lemma decl_io_state_incr:
          (st_wf s)).
 Proof. constructor; simpl; auto using Ple_succ with verilog_state. Qed.
 
+(** Declare a new register by incrementing the [st_freshreg] by one and
+returning the old [st_freshreg]. *)
+
 Definition decl_io (sz: nat): mon (reg * nat) :=
   fun s => let r := s.(st_freshreg) in
            OK (r, sz) (mkstate
@@ -409,6 +416,9 @@ Definition decl_io (sz: nat): mon (reg * nat) :=
                      (st_wf s))
               (decl_io_state_incr s).
 
+(** Declare a new register which is given, by changing [st_decl] and without
+affecting anything else. *)
+
 Definition declare_reg (r: reg) (sz: nat): mon (reg * nat) :=
   fun s => OK (r, sz) (mkstate
                       (st_freshreg s)
@@ -419,6 +429,9 @@ Definition declare_reg (r: reg) (sz: nat): mon (reg * nat) :=
                       (st_wf s))
               (change_decl_state_incr s (PositiveMap.add r sz s.(st_decl))).
 
+(** Declare a new fresh register by first getting a valid register to increment,
+and then adding it to the declaration list. *)
+
 Definition decl_fresh_reg (sz : nat) : mon (reg * nat) :=
   do (r, s) <- decl_io sz;
   declare_reg r s.
@@ -529,11 +542,8 @@ Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr *
 Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt :=
   Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)) (Some Vskip).
 
-Fixpoint allocate_regs (e : list (reg * nat)) {struct e} : list module_item :=
-  match e with
-  | (r, n)::es => Vdecl r n :: allocate_regs es
-  | nil => nil
-  end.
+Definition allocate_reg (e : reg * nat) : module_item :=
+  match e with (r, n) => Vdecl r n end.
 
 Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list module_item :=
   (Valways_ff (Vposedge clk)
@@ -541,7 +551,7 @@ Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list m
       (nonblock st (posToExpr 32 entry))
       (make_statetrans st s.(st_statetrans))))
   :: (Valways_ff (Vposedge clk) (make_stm st s.(st_stm)))
-  :: (allocate_regs (PositiveMap.elements s.(st_decl))).
+  :: (map allocate_reg (PositiveMap.elements s.(st_decl))).
 
 (** To start out with, the assumption is made that there is only one
     function/module in the original code. *)
@@ -549,27 +559,16 @@ Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list m
 Definition set_int_size (r: reg) : reg * nat := (r, 32%nat).
 
 Definition transf_module (f: function) : mon module :=
-  do fin <- decl_io 1%nat;
-  do rtrn <- decl_io 32%nat;
+  do fin <- decl_io 1;
+  do rtrn <- decl_io 32;
   do _ <- traverselist (transf_instr (fst fin) (fst rtrn)) (Maps.PTree.elements f.(fn_code));
-  do start <- decl_io 1%nat;
-  do rst <- decl_io 1%nat;
-  do clk <- decl_io 1%nat;
-  do st <- decl_fresh_reg 32%nat;
+  do start <- decl_io 1;
+  do rst <- decl_io 1;
+  do clk <- decl_io 1;
+  do st <- decl_fresh_reg 32;
   do current_state <- get;
   let mi := make_module_items f.(fn_entrypoint) (fst clk) (fst st) (fst rst) current_state in
-  ret (mkmodule start rst clk fin rtrn (map set_int_size f.(fn_params)) mi).
-
-Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit))
-{struct flist} : option function :=
-  match flist with
-  | (i, AST.Gfun (AST.Internal f)) :: xs =>
-    if Pos.eqb i main
-    then Some f
-    else main_function main xs
-  | _ :: xs => main_function main xs
-  | nil => None
-  end.
+  ret (mkmodule start rst clk fin rtrn st (map set_int_size f.(fn_params)) mi).
 
 Lemma max_state_valid_freshstate:
   forall f,
@@ -591,6 +590,24 @@ Definition max_state (f: function) : state :=
           (st_decl init_state)
           (max_state_st_wf f).
 
+Definition transl_module (f : function) : Errors.res module :=
+  run_mon (max_state f) (transf_module f).
+
+(** Retrieve the main function from the RTL, this should probably be replaced by
+retrieving a designated function instead.  This could be passed on the
+commandline and be assumed as a [Parameter] in this code. *)
+
+Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit))
+{struct flist} : option function :=
+  match flist with
+  | (i, AST.Gfun (AST.Internal f)) :: xs =>
+    if Pos.eqb i main
+    then Some f
+    else main_function main xs
+  | _ :: xs => main_function main xs
+  | nil => None
+  end.
+
 Definition transf_program (d : program) : Errors.res module :=
   match main_function d.(AST.prog_main) d.(AST.prog_defs) with
   | Some f => run_mon (max_state f) (transf_module f)
-- 
cgit