Merge branch 'master' into arrays-proof

5 files changed, 149 insertions, 188 deletions

diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 82aac41..c509248 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -48,7 +48,12 @@ Record module: Type :=
     mod_stk : reg;
     mod_stk_len : nat;
     mod_finish : reg;
-    mod_return : reg
+    mod_return : reg;
+    mod_start : reg;
+    mod_reset : reg;
+    mod_clk : reg;
+    mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl);
+    mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl);
   }.
 
 Definition fundef := AST.fundef module.
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index bdd8581..700b8e3 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -21,6 +21,7 @@ open Value
 open Datatypes
 
 open Camlcoq
+open AST
 
 open Printf
 
@@ -107,21 +108,30 @@ let pprint_edge_top i = function
   | Valledge -> "@*"
   | Voredge (e1, e2) -> concat ["@("; pprint_edge e1; " or "; pprint_edge e2; ")"]
 
-let declare i t =
+let declare t =
   function (r, sz) ->
-    concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
+    concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
              register r; ";\n" ]
 
-let declarearr i t =
+let declarearr t =
   function (r, sz, ln) ->
-    concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
+    concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
              register r;
              " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ]
 
+let print_io = function
+  | Some Vinput -> "input"
+  | Some Voutput -> "output reg"
+  | Some Vinout -> "inout"
+  | None -> "reg"
+
+let decl i = function
+  | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)]
+  | Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)]
+
 (* TODO Fix always blocks, as they currently always print the same. *)
 let pprint_module_item i = function
-  | Vdecl (r, sz) -> declare i "reg" (r, sz)
-  | Vdeclarr (r, sz, ln) -> declarearr i "reg" (r, sz, ln)
+  | Vdeclaration d -> decl i d
   | Valways (e, s) ->
     concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
   | Valways_ff (e, s) ->
@@ -138,10 +148,6 @@ let make_io i io r = concat [indent i; io; " "; register r; ";\n"]
 
 let compose f g x = g x |> f
 
-let init_inputs i r = declare i "input" r
-
-let init_outputs i r = declare i "output reg" r
-
 let testbench = "module testbench;
    reg start, reset, clk;
    wire finish;
@@ -171,17 +177,12 @@ endmodule
 let pprint_module i n m =
   let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in
   let outputs = [m.mod_finish; m.mod_return] in
-  concat [ indent i; "module "; n;
-           "("; concat (intersperse ", " (List.map (compose register fst) (inputs @ outputs))); ");\n";
-           fold_map (init_inputs (i+1)) inputs;
-           fold_map (init_outputs (i+1)) outputs;
+  concat [ indent i; "module "; (extern_atom n);
+           "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n";
            fold_map (pprint_module_item (i+1)) m.mod_body;
-           indent i; "endmodule\n\n";
-           testbench
+           indent i; "endmodule\n\n"
          ]
 
-let print_program pp v = pstr pp (pprint_module 0 "main" v)
-
 let print_result pp lst =
   let rec print_result_in pp = function
     | [] -> fprintf pp "]\n"
@@ -192,3 +193,12 @@ let print_result pp lst =
   print_result_in pp lst
 
 let print_value pp v = fprintf pp "%s" (literal v)
+
+let print_globdef pp (id, gd) =
+  match gd with
+  | Gfun(Internal f) -> pstr pp (pprint_module 0 id f)
+  | _ -> ()
+
+let print_program pp prog =
+  List.iter (print_globdef pp) prog.prog_defs;
+  pstr pp testbench
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index c9fca8e..0df9d06 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -18,6 +18,6 @@
 
 val print_value : out_channel -> Value.value -> unit
 
-val print_program : out_channel -> Verilog.coq_module -> unit
+val print_program : out_channel -> Verilog.program -> unit
 
 val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit
diff --git a/src/verilog/Test.v b/src/verilog/Test.v
deleted file mode 100644
index 90c5312..0000000
--- a/src/verilog/Test.v
+++ /dev/null
@@ -1,99 +0,0 @@
-(*
- * CoqUp: Verified high-level synthesis.
- * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
- *
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
-
-From coqup Require Import Verilog Veriloggen Coquplib Value.
-From compcert Require Import AST Errors Maps Op Integers.
-From compcert Require RTL.
-From Coq Require Import FSets.FMapPositive.
-From bbv Require Import Word.
-Import ListNotations.
-Import HexNotationValue.
-Import WordScope.
-
-Local Open Scope word_scope.
-
-Definition test_module : module :=
-  let mods := [
-      Valways (Vposedge 3%positive) (Vseq (Vnonblock (Vvar 6%positive) (Vlit (ZToValue 32 5)))
-                                          (Vnonblock (Vvar 7%positive)
-                                                     (Vvar 6%positive)))
-      ] in
-  mkmodule (1%positive, 1%nat)
-           (2%positive, 1%nat)
-           (3%positive, 1%nat)
-           (4%positive, 1%nat)
-           (5%positive, 32%nat)
-           (6%positive, 32%nat)
-           nil
-           mods.
-
-Definition test_input : RTL.function :=
-  let sig := mksignature nil Tvoid cc_default in
-  let params := nil in
-  let stacksize := 0 in
-  let entrypoint := 3%positive in
-  let code := PTree.set 1%positive (RTL.Ireturn (Some 1%positive))
-               (PTree.set 3%positive (RTL.Iop (Ointconst (Int.repr 5)) nil 1%positive 1%positive)
-                          (PTree.empty RTL.instruction)) in
-  RTL.mkfunction sig params stacksize code entrypoint.
-
-Definition test_input_program : RTL.program :=
-  mkprogram [(1%positive, Gfun (Internal test_input))] nil 1%positive.
-
-Compute transf_program test_input_program.
-
-Definition test_output_module : module :=
-  {| mod_start := (4%positive, 1%nat);
-     mod_reset := (5%positive, 1%nat);
-     mod_clk := (6%positive, 1%nat);
-     mod_finish := (2%positive, 1%nat);
-     mod_return := (3%positive, 32%nat);
-     mod_state := (7%positive, 32%nat);
-     mod_args := [];
-     mod_body :=
-       [Valways_ff (Vposedge 6%positive)
-                   (Vcond (Vbinop Veq (Vinputvar 5%positive) (1'h"1"))
-                          (Vnonblock (Vvar 7%positive) (32'h"3"))
-                          (Vcase (Vvar 7%positive)
-                                 [(Vlit (32'h"1"), Vnonblock (Vvar 7%positive) (32'h"1"));
-                                 (Vlit (32'h"3"), Vnonblock (Vvar 7%positive) (32'h"1"))]
-                                 (Some Vskip)));
-       Valways_ff (Vposedge 6%positive)
-                  (Vcase (Vvar 7%positive)
-                         [(Vlit (32'h"1"), Vseq (Vblock (Vvar 2%positive) (Vlit (1'h"1")))
-                                                (Vblock (Vvar 3%positive) (Vvar 1%positive)));
-                         (Vlit (32'h"3"), Vblock (Vvar 1%positive) (Vlit (32'h"5")))]
-                         (Some Vskip));
-       Vdecl 1%positive 32; Vdecl 7%positive 32] |}.
-
-Lemma valid_test_output :
-  transf_program test_input_program = OK test_output_module.
-Proof. trivial. Qed.
-
-Definition test_fextclk := initial_fextclk test_output_module.
-
-Lemma manual_simulation :
-  step (State test_output_module empty_assocmap empty_assocmap
-              test_fextclk 1 (32'h"1"))
-       (State test_output_module (add_assocmap 7%positive (32'h"3") empty_assocmap)
-              empty_assocmap test_fextclk 2 (32'h"3")).
-Proof.
-  repeat (econstructor; eauto);
-  try (unfold ZToValue; instantiate (1 := eq_refl (vsize (1'h"1"))); auto);
-  apply nevalue; apply weqb_false; trivial. Unshelve. exact 0%nat.
-Qed.
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 0e999de..8b83d49 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -87,6 +87,8 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
 Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
   mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)).
 
+Inductive scl_decl : Type := Scalar (sz : nat).
+Inductive arr_decl : Type := Array (sz : nat) (ln : nat).
 
 (** * Verilog AST
 
@@ -181,9 +183,17 @@ Module items can either be declarations ([Vdecl]) or always blocks ([Valways]).
 The declarations are always register declarations as combinational logic can be
 done using combinational always block instead of continuous assignments. *)
 
+Inductive io : Type :=
+| Vinput : io
+| Voutput : io
+| Vinout : io.
+
+Inductive declaration : Type :=
+| Vdecl : option io -> reg -> nat -> declaration
+| Vdeclarr : option io -> reg -> nat -> nat -> declaration.
+
 Inductive module_item : Type :=
-| Vdecl : reg -> nat -> module_item
-| Vdeclarr : reg -> nat -> nat -> module_item
+| Vdeclaration : declaration -> module_item
 | Valways : edge -> stmnt -> module_item
 | Valways_ff : edge -> stmnt -> module_item
 | Valways_comb : edge -> stmnt -> module_item.
@@ -200,15 +210,22 @@ Inductive module_item : Type :=
 *)
 
 Record module : Type := mkmodule {
-  mod_start : szreg;
-  mod_reset : szreg;
-  mod_clk : szreg;
-  mod_finish : szreg;
-  mod_return : szreg;
-  mod_state : szreg; (**r Variable that defines the current state, it should be internal. *)
-  mod_args : list szreg;
+  mod_start : reg;
+  mod_reset : reg;
+  mod_clk : reg;
+  mod_finish : reg;
+  mod_return : reg;
+  mod_st : reg; (**r Variable that defines the current state, it should be internal. *)
+  mod_stk : reg;
+  mod_args : list reg;
   mod_body : list module_item;
-                        }.
+  mod_entrypoint : node;
+}.
+
+Definition fundef := AST.fundef module.
+
+Definition program := AST.program fundef unit.
+
 (** Convert a [positive] to an expression directly, setting it to the right
     size. *)
 Definition posToLit (p : positive) : expr :=
@@ -241,18 +258,28 @@ retrieved and set appropriately.
   which determines which part of the Verilog is executed.  This is then the part
   of the Verilog that should match with the RTL. *)
 
+Inductive stackframe : Type :=
+  Stackframe :
+    forall  (res : reg)
+            (m : module)
+            (pc : node)
+            (assoc : assocmap),
+      stackframe.
+
 Inductive state : Type :=
-| State:
-    forall (m : module)
-           (assoc : reg_associations)
-           (assoc : arr_associations)
-           (f : fextclk)
-           (cycle : nat)
-           (stvar : value),
-    state
-| Finishstate:
-    forall v : value,
-    state.
+| State :
+    forall (stack : list stackframe)
+           (m : module)
+           (st : node)
+           (reg_assoc : assocmap)
+           (arr_assoc : AssocMap.t (list value)), state
+| Returnstate :
+    forall (res : list stackframe)
+           (v : value), state
+| Callstate :
+    forall (stack : list stackframe)
+           (m : module)
+           (args : list value), state.
 
 Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value :=
   match op with
@@ -383,14 +410,14 @@ Definition access_fext (f : fext) (r : reg) : res value :=
 (** Return the location of the lhs of an assignment. *)
 
 Inductive location : Type :=
-| Reg (_ : reg)
-| Array (_ : reg) (_ : nat).
+| LocReg (_ : reg)
+| LocArray (_ : reg) (_ : nat).
 
 Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop :=
-| Base : forall f asr asa r, location_is f asr asa (Vvar r) (Reg r)
+| Base : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r)
 | Indexed : forall f asr asa r iexp iv,
   expr_runp f asr asa iexp iv ->
-  location_is f asr asa (Vvari r iexp) (Array r (valueToNat iv)).
+  location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)).
 
 (* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l)  (e : expr) : res reg := *)
 (*   match e with *)
@@ -508,28 +535,28 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations ->
     stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1
 | stmnt_runp_Vblock_reg:
     forall lhs r rhs rhsval asr asa f,
-    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Reg r) ->
+    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) ->
     expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
     stmnt_runp f asr asa
                  (Vblock lhs rhs)
                  (block_reg r asr rhsval) asa
 | stmnt_runp_Vnonblock_reg:
     forall lhs r rhs rhsval asr asa f,
-    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Reg r) ->
+    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) ->
     expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
     stmnt_runp f asr asa
                  (Vnonblock lhs rhs)
                  (nonblock_reg r asr rhsval) asa
 | stmnt_runp_Vblock_arr:
     forall lhs r i rhs rhsval asr asa f,
-    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Array r i) ->
+    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) ->
     expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
     stmnt_runp f asr asa
                  (Vblock lhs rhs)
                  asr (block_arr r i asa rhsval)
 | stmnt_runp_Vnonblock_arr:
     forall lhs r i rhs rhsval asr asa f,
-    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Array r i) ->
+    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) ->
     expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
     stmnt_runp f asr asa
                  (Vnonblock lhs rhs)
@@ -565,8 +592,8 @@ Inductive mi_stepp : fext -> reg_associations -> arr_associations ->
     stmnt_runp f sr0 sa0 st sr1 sa1 ->
     mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1
 | mi_stepp_Vdecl :
-    forall f sr sa lhs rhs,
-    mi_stepp f sr sa (Vdecl lhs rhs) sr sa.
+    forall f sr sa lhs rhs io,
+    mi_stepp f sr sa (Vdeclaration (Vdecl io lhs rhs)) sr sa.
 Hint Constructors mi_stepp : verilog.
 
 Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
@@ -607,8 +634,8 @@ other arguments to the module are also to be supported. *)
 
 Definition initial_fextclk (m : module) : fextclk :=
   fun x => match x with
-           | S O => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap)
-           | _ => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap)
+           | S O => (AssocMap.set (mod_reset m) (ZToValue 1 1) empty_assocmap)
+           | _ => (AssocMap.set (mod_reset m) (ZToValue 1 0) empty_assocmap)
            end.
 
 (*Definition module_run (n : nat) (m : module) : res assocmap :=
@@ -655,42 +682,60 @@ Qed.
 
  *)
 
-Definition genv := Genv.t unit unit.
-
-Inductive step : state -> state -> Prop :=
-| step_module :
-    forall m stvar stvar' cycle f
-      asr0 asa0 asr1 asa1
-      asr' asa',
-    mis_stepp (f cycle) asr0 asa0
-              m.(mod_body) asr1 asa1 ->
-    asr' = merge_associations asr1 ->
-    asa' = merge_associations asa1 ->
-    Some stvar' = asr'.(assoc_blocking)!(fst m.(mod_state)) ->
-    step (State m asr0 asa0 f cycle stvar)
-         (State m asr' asa' f (S cycle) stvar')
+Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} :=
+  match rl, vl with
+  | r :: rl', v :: vl' => AssocMap.set r v (init_params vl' rl')
+  | _, _ => empty_assocmap
+  end.
+
+Definition genv := Globalenvs.Genv.t fundef unit.
+
+Inductive step : genv -> state -> Events.trace -> state -> Prop :=
+  | step_module :
+      forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g,
+      mis_stepp f (mkassociations asr empty_assocmap)
+                  (mkassociations asa (AssocMap.empty (list value)))
+                  m.(mod_body)
+                  (mkassociations basr1 nasr1)
+                  (mkassociations basa1 nasa1)->
+      asr' = merge_assocmap nasr1 basr1 ->
+      asa' = AssocMapExt.merge (list value) nasa1 basa1 ->
+      asr'!(m.(mod_st)) = Some stval ->
+      valueToPos stval = pstval ->
+      step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
 | step_finish :
-    forall m asr asa f cycle stvar result,
-    asr.(assoc_blocking)!(fst m.(mod_finish)) = Some (1'h"1") ->
-    asr.(assoc_blocking)!(fst m.(mod_return)) = Some result ->
-    step (State m asr asa f cycle stvar)
-         (Finishstate result).
+    forall asr asa sf retval m st g,
+    asr!(m.(mod_finish)) = Some (1'h"1") ->
+    asr!(m.(mod_return)) = Some retval ->
+    step g (State sf m st asr asa) Events.E0 (Returnstate sf retval)
+| step_call :
+    forall g res m args,
+    step g (Callstate res m args) Events.E0
+         (State res m m.(mod_entrypoint)
+          (AssocMap.set m.(mod_st) (posToValue 32 m.(mod_entrypoint))
+           (init_params args m.(mod_args)))
+          (AssocMap.empty (list value)))
+| step_return :
+    forall g m asr i r sf pc mst,
+    mst = mod_st m ->
+    step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0
+         (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
+                (AssocMap.empty (list value))).
 Hint Constructors step : verilog.
 
-(*Inductive initial_state (m: module): state -> Prop :=
-| initial_state_intro:
-    forall hmi tmi,
-    hmi::tmi = mod_body m ->
-    initial_state m (State m hmi tmi empty_assocmap empty_assocmap (initial_fextclk m) O xH).
-
-(** A final state is a [Returnstate] with an empty call stack. *)
-
-Inductive final_state: state -> Integers.int -> Prop :=
-  | final_state_intro: forall v,
-      final_state (Finishstate v) (valueToInt v).
-
-(** The small-step semantics for a module. *)
-
-Definition semantics (p: module) :=
-  Semantics step (initial_state p) final_state (Genv.empty_genv unit unit nil).
-*)
+Inductive initial_state (p: program): state -> Prop :=
+  | initial_state_intro: forall b m0 m,
+      let ge := Globalenvs.Genv.globalenv p in
+      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).
+
+Inductive final_state : state -> Integers.int -> Prop :=
+| final_state_intro : forall retval retvali,
+    retvali = valueToInt retval ->
+    final_state (Returnstate nil retval) retvali.
+
+Definition semantics (m : program) :=
+  Smallstep.Semantics step (initial_state m) final_state
+                      (Globalenvs.Genv.globalenv m).