Add AssocMap

4 files changed, 93 insertions, 47 deletions

diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
new file mode 100644
index 0000000..e550072
--- /dev/null
+++ b/src/verilog/AssocMap.v
@@ -0,0 +1,60 @@
+(*
+ * 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 Coquplib Value.
+From Coq Require Import FSets.FMapPositive.
+
+Definition reg := positive.
+
+Module AssocMap := PositiveMap.
+
+Module AssocMapExt.
+  Import AssocMap.
+
+  Section Operations.
+
+    Variable elt : Type.
+
+    Definition merge : t elt -> t elt -> t elt := fold (@add elt).
+
+    Definition find_default (a : elt) (k : reg) (m : t elt) : elt :=
+      match find k m with
+      | None => a
+      | Some v => v
+      end.
+
+  End Operations.
+
+End AssocMapExt.
+Import AssocMapExt.
+
+Definition assocmap := AssocMap.t value.
+
+Definition find_assocmap (n : nat) : reg -> assocmap -> value :=
+  find_default value (ZToValue n 0).
+
+Definition empty_assocmap : assocmap := AssocMap.empty value.
+
+Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value.
+
+Module AssocMapNotation.
+  Notation "a ! b" := (AssocMap.find b a) (at level 1).
+  Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1).
+  Notation "a # b" := (find_assocmap 32 b a) (at level 1).
+  Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1).
+End AssocMapNotation.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 3d863b2..147d24b 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -17,7 +17,7 @@
  *)
 
 From Coq Require Import FSets.FMapPositive.
-From coqup Require Import Coquplib Value.
+From coqup Require Import Coquplib Value AssocMap.
 From coqup Require Verilog.
 From compcert Require Events Globalenvs Smallstep Integers.
 
@@ -57,7 +57,7 @@ Inductive state : Type :=
 | State :
     forall (m : module)
            (st : node)
-           (assoc : Verilog.assocset),
+           (assoc : assocmap),
   state
 | Returnstate : forall v : value, state.
 
@@ -67,14 +67,14 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       m.(mod_controllogic)!st = Some ctrl ->
       m.(mod_datapath)!st = Some data ->
       Verilog.stmnt_runp f
-        (Verilog.mkassociations assoc0 Verilog.empty_assocset)
+        (Verilog.mkassociations assoc0 empty_assocmap)
         ctrl
         (Verilog.mkassociations assoc1 nbassoc0) ->
       Verilog.stmnt_runp f
         (Verilog.mkassociations assoc1 nbassoc0)
         data
         (Verilog.mkassociations assoc2 nbassoc1) ->
-      assoc3 = Verilog.merge_assocset nbassoc1 assoc2 ->
+      assoc3 = merge_assocmap nbassoc1 assoc2 ->
       step g (State m st assoc0) t (State m st assoc3)
 | step_finish :
     forall g t m st assoc retval,
@@ -86,7 +86,7 @@ Hint Constructors step : htl.
 Inductive initial_state (m : module) : state -> Prop :=
 | initial_state_intro : forall st,
     st = m.(mod_entrypoint) ->
-    initial_state m (State m st Verilog.empty_assocset).
+    initial_state m (State m st empty_assocmap).
 
 Inductive final_state : state -> Integers.int -> Prop :=
 | final_state_intro : forall retval retvali,
diff --git a/src/verilog/Test.v b/src/verilog/Test.v
index f24612e..90c5312 100644
--- a/src/verilog/Test.v
+++ b/src/verilog/Test.v
@@ -88,10 +88,10 @@ Proof. trivial. Qed.
 Definition test_fextclk := initial_fextclk test_output_module.
 
 Lemma manual_simulation :
-  step (State test_output_module empty_assocset empty_assocset
+  step (State test_output_module empty_assocmap empty_assocmap
               test_fextclk 1 (32'h"1"))
-       (State test_output_module (add_assocset 7%positive (32'h"3") empty_assocset)
-              empty_assocset test_fextclk 2 (32'h"3")).
+       (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);
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index ba7e83d..c0bce25 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -27,24 +27,21 @@ From Coq Require Import
 
 Import ListNotations.
 
-From coqup Require Import common.Coquplib common.Show verilog.Value.
+From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap.
 From compcert Require Integers Events.
 From compcert Require Import Errors Smallstep Globalenvs.
 
 Import HexNotationValue.
-
-Notation "a ! b" := (PositiveMap.find b a) (at level 1).
+Import AssocMapNotation.
 
 Definition reg : Type := positive.
 Definition node : Type := positive.
 Definition szreg : Type := reg * nat.
 
-Definition assocset : Type := PositiveMap.t value.
-
 Record associations : Type :=
   mkassociations {
-    assoc_blocking : assocset;
-    assoc_nonblocking : assocset
+    assoc_blocking : assocmap;
+    assoc_nonblocking : assocmap
   }.
 
 (** * Verilog AST
@@ -58,8 +55,6 @@ The Verilog [value] is a bitvector containg a size and the actual bitvector. In
 this case, the [Word.word] type is used as many theorems about that bitvector
 have already been proven. *)
 
-Definition estate : Type := assocset * assocset.
-
 (** ** Binary Operators
 
 These are the binary operations that can be represented in Verilog. Ideally,
@@ -167,8 +162,7 @@ Record module : Type := mkmodule {
   mod_state : szreg; (**r Variable that defines the current state, it should be internal. *)
   mod_args : list szreg;
   mod_body : list module_item;
-}.
-
+                        }.
 (** Convert a [positive] to an expression directly, setting it to the right
     size. *)
 Definition posToLit (p : positive) : expr :=
@@ -204,8 +198,8 @@ retrieved and set appropriately.
 Inductive state : Type :=
 | State:
     forall (m : module)
-           (assoc : assocset)
-           (nbassoc : assocset)
+           (assoc : assocmap)
+           (nbassoc : assocmap)
            (f : fextclk)
            (cycle : nat)
            (stvar : value),
@@ -246,7 +240,7 @@ Definition unop_run (op : unop) : value -> value :=
   | Vnot => vbitneg
   end.
 
-Inductive expr_runp : fext -> assocset -> expr -> value -> Prop :=
+Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop :=
   | erun_Vlit :
       forall fext assoc v,
       expr_runp fext assoc (Vlit v) v
@@ -312,7 +306,7 @@ Definition access_fext (f : fext) (r : reg) : res value :=
   end.
 
 (* TODO FIX Vvar case without default *)
-(*Fixpoint expr_run (assoc : assocset) (e : expr)
+(*Fixpoint expr_run (assoc : assocmap) (e : expr)
          {struct e} : res value :=
   match e with
   | Vlit v => OK v
@@ -461,7 +455,7 @@ Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop :=
     assoc' = (PositiveMap.add name rhsval assoc) ->
     stmnt_runp f (mkassociations assoc nbassoc)
                  (Vblock lhs rhs)
-                 (mkassociations assoc nbassoc)
+                 (mkassociations assoc' nbassoc)
 | stmnt_runp_Vnonblock:
     forall lhs name rhs rhsval assoc nbassoc nbassoc' f,
     assign_name lhs = OK name ->
@@ -514,28 +508,20 @@ Inductive mis_stepp : fext -> associations -> list module_item -> associations -
     mis_stepp f s nil s.
 Hint Constructors mis_stepp : verilog.
 
-Definition add_assocset (r : reg) (v : value) (assoc : assocset) : assocset :=
-  PositiveMap.add r v assoc.
-
-Definition merge_assocset (nbassoc assoc : assocset) : assocset :=
-  PositiveMap.fold add_assocset nbassoc assoc.
-
-Definition empty_assocset : assocset := PositiveMap.empty value.
-
 (*Definition mi_step_commit (s : state) (m : list module_item) : res state :=
   match mi_step s m with
   | OK (State m assoc nbassoc f c) =>
-    OK (State m (merge_assocset nbassoc assoc) empty_assocset f c)
+    OK (State m (merge_assocmap nbassoc assoc) empty_assocmap f c)
   | Error msg => Error msg
   | _ => Error (msg "Verilog: Wrong state")
-  end.*)
+  end.
 
-(*Fixpoint mi_run (f : fextclk) (assoc : assocset) (m : list module_item) (n : nat)
-         {struct n} : res assocset :=
+Fixpoint mi_run (f : fextclk) (assoc : assocmap) (m : list module_item) (n : nat)
+         {struct n} : res assocmap :=
   match n with
   | S n' =>
     do assoc' <- mi_run f assoc m n';
-    match mi_step_commit (State assoc' empty_assocset f (Pos.of_nat n')) m with
+    match mi_step_commit (State assoc' empty_assocmap f (Pos.of_nat n')) m with
     | OK (State assoc _ _ _) => OK assoc
     | Error m => Error m
     end
@@ -548,12 +534,12 @@ other arguments to the module are also to be supported. *)
 
 Definition initial_fextclk (m : module) : fextclk :=
   fun x => match x with
-           | S O => (add_assocset (fst (mod_reset m)) (ZToValue 1 1) empty_assocset)
-           | _ => (add_assocset (fst (mod_reset m)) (ZToValue 1 0) empty_assocset)
+           | S O => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap)
+           | _ => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap)
            end.
 
-(*Definition module_run (n : nat) (m : module) : res assocset :=
-  mi_run (initial_fextclk m) empty_assocset (mod_body m) n.*)
+(*Definition module_run (n : nat) (m : module) : res assocmap :=
+  mi_run (initial_fextclk m) empty_assocmap (mod_body m) n.*)
 
 Local Close Scope error_monad_scope.
 
@@ -601,18 +587,18 @@ Definition genv := Genv.t unit unit.
 Inductive step : state -> state -> Prop :=
 | step_module :
     forall m stvar stvar' cycle f assoc0 assoc1 assoc2 nbassoc,
-    mis_stepp (f cycle) (mkassociations assoc0 empty_assocset)
+    mis_stepp (f cycle) (mkassociations assoc0 empty_assocmap)
               m.(mod_body)
               (mkassociations assoc1 nbassoc) ->
-    assoc2 = merge_assocset nbassoc assoc1 ->
+    assoc2 = merge_assocmap nbassoc assoc1 ->
     Some stvar' = assoc2!(fst m.(mod_state)) ->
-    step (State m assoc0 empty_assocset f cycle stvar)
-         (State m assoc2 empty_assocset f (S cycle) stvar')
+    step (State m assoc0 empty_assocmap f cycle stvar)
+         (State m assoc2 empty_assocmap f (S cycle) stvar')
 | step_finish :
     forall m assoc f cycle stvar result,
     assoc!(fst m.(mod_finish)) = Some (1'h"1") ->
     assoc!(fst m.(mod_return)) = Some result ->
-    step (State m assoc empty_assocset f cycle stvar)
+    step (State m assoc empty_assocmap f cycle stvar)
          (Finishstate result).
 Hint Constructors step : verilog.
 
@@ -620,7 +606,7 @@ Hint Constructors step : verilog.
 | initial_state_intro:
     forall hmi tmi,
     hmi::tmi = mod_body m ->
-    initial_state m (State m hmi tmi empty_assocset empty_assocset (initial_fextclk m) O xH).
+    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. *)