From fdf5e7378715ba1bd8552e2f005c4a15c834a038 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 22 Apr 2020 22:43:03 +0100
Subject: Add stmnt_runp inductive

---
 src/verilog/Verilog.v | 133 ++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 106 insertions(+), 27 deletions(-)

(limited to 'src/verilog/Verilog.v')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 4713c36..4ad297b 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -173,7 +173,7 @@ Definition fext := PositiveMap.t value.
 Definition fextclk := nat -> fext.
 
 Inductive state: Type :=
-  State:
+  Runstate:
     forall (assoc : assoclist)
            (nbassoc : assoclist)
            (f : fextclk)
@@ -219,7 +219,7 @@ Inductive expr_runp : state -> expr -> value -> Prop :=
   | erun_Vvar :
       forall assoc na f c v r,
       assoc!r = Some v ->
-      expr_runp (State assoc na f c) (Vvar r) v
+      expr_runp (Runstate assoc na f c) (Vvar r) v
   | erun_Vinputvar :
       forall s r v,
       expr_runp s (Vinputvar r) v
@@ -265,7 +265,7 @@ Local Open Scope error_monad_scope.
 
 Definition access_fext (s : state) (r : reg) : res value :=
   match s with
-  | State _ _ f c =>
+  | Runstate _ _ f c =>
     match PositiveMap.find r (f (Pos.to_nat c)) with
     | Some v => OK v
     | _ => OK (ZToValue 1 0)
@@ -278,7 +278,7 @@ Fixpoint expr_run (s : state) (e : expr)
   match e with
   | Vlit v => OK v
   | Vvar r => match s with
-              | State assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r
+              | Runstate assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r
               end
   | Vinputvar r => access_fext s r
   | Vbinop op l r =>
@@ -307,6 +307,15 @@ Definition assign_name (e : expr) : res reg :=
   | _ => Error (msg "Verilog: expression not supported on lhs of assignment")
   end.
 
+Fixpoint stmnt_height (st : stmnt) {struct st} : nat :=
+  match st with
+  | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2)
+  | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2))
+  | Vcase _ ls (Some st) =>
+    S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls)
+  | _ => 1
+  end.
+
 Fixpoint find_case_stmnt (s : state) (v : value) (cl : list (expr * stmnt))
          {struct cl} : option (res stmnt) :=
   match cl with
@@ -345,34 +354,83 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
       end
     | Vblock lhs rhs =>
       match s with
-      | State assoc nbassoc f c =>
+      | Runstate assoc nbassoc f c =>
         do name <- assign_name lhs;
         do rhse <- expr_run s rhs;
-        OK (State (PositiveMap.add name rhse assoc) nbassoc f c)
+        OK (Runstate (PositiveMap.add name rhse assoc) nbassoc f c)
       end
     | Vnonblock lhs rhs =>
       match s with
-      | State assoc nbassoc f c =>
+      | Runstate assoc nbassoc f c =>
         do name <- assign_name lhs;
         do rhse <- expr_run s rhs;
-        OK (State assoc (PositiveMap.add name rhse nbassoc) f c)
+        OK (Runstate assoc (PositiveMap.add name rhse nbassoc) f c)
       end
     end
   | _ => OK s
   end.
 
-Fixpoint stmnt_height (st : stmnt) {struct st} : nat :=
-  match st with
-  | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2)
-  | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2))
-  | Vcase _ ls (Some st) =>
-    S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls)
-  | _ => 1
-  end.
-
 Definition stmnt_run (s : state) (st : stmnt) : res state :=
   stmnt_run' (stmnt_height st) s st.
 
+Inductive not_matched (s : state) (caseval : value) (curr : expr * stmnt) : Prop :=
+  not_in:
+    forall currval,
+    expr_runp s (fst curr) currval ->
+    caseval <> currval ->
+    not_matched s caseval curr.
+
+Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
+| stmnt_run_Vskip:
+    forall s, stmnt_runp s Vskip s
+| stmnt_run_Vseq:
+    forall st1 st2 s0 s1 s2,
+    stmnt_runp s0 st1 s1 ->
+    stmnt_runp s1 st2 s2 ->
+    stmnt_runp s0 (Vseq st1 st2) s2
+| stmnt_runp_Vcond_true:
+    forall s0 s1 c vc stt stf,
+    expr_runp s0 c vc ->
+    valueToBool vc = true ->
+    stmnt_runp s0 stt s1 ->
+    stmnt_runp s0 (Vcond c stt stf) s1
+| stmnt_runp_Vcond_false:
+    forall s0 s1 c vc stt stf,
+    expr_runp s0 c vc ->
+    valueToBool vc = false ->
+    stmnt_runp s0 stf s1 ->
+    stmnt_runp s0 (Vcond c stt stf) s1
+| stmnt_runp_Vcase:
+    forall e ve s0 s1 me mve sc clst def,
+    expr_runp s0 e ve ->
+    expr_runp s0 me mve ->
+    mve = ve ->
+    In (me, sc) clst ->
+    stmnt_runp s0 sc s1 ->
+    stmnt_runp s0 (Vcase e clst def) s1
+| stmnt_runp_Vcase_default:
+    forall s0 st s1 e ve clst,
+    expr_runp s0 e ve ->
+    Forall (not_matched s0 ve) clst ->
+    stmnt_runp s0 st s1 ->
+    stmnt_runp s0 (Vcase e clst (Some st)) s1
+| stmnt_runp_Vblock:
+    forall lhs name rhs rhsval s assoc assoc' nbassoc f cycle,
+    assign_name lhs = OK name ->
+    expr_runp s rhs rhsval ->
+    assoc' = (PositiveMap.add name rhsval assoc) ->
+    stmnt_runp (Runstate assoc nbassoc f cycle)
+               (Vblock lhs rhs)
+               (Runstate assoc' nbassoc f cycle)
+| stmnt_runp_Vnonblock:
+    forall lhs name rhs rhsval s assoc nbassoc nbassoc' f cycle,
+    assign_name lhs = OK name ->
+    expr_runp s rhs rhsval ->
+    nbassoc' = (PositiveMap.add name rhsval nbassoc) ->
+    stmnt_runp (Runstate assoc nbassoc f cycle)
+               (Vblock lhs rhs)
+               (Runstate assoc nbassoc' f cycle).
+
 Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
   let run := fun st ls =>
               do s' <- stmnt_run s st;
@@ -396,8 +454,8 @@ Definition empty_assoclist : assoclist := PositiveMap.empty value.
 
 Definition mi_step_commit (s : state) (m : list module_item) : res state :=
   match mi_step s m with
-  | OK (State assoc nbassoc f c) =>
-    OK (State (merge_assoclist nbassoc assoc) empty_assoclist f c)
+  | OK (Runstate assoc nbassoc f c) =>
+    OK (Runstate (merge_assoclist nbassoc assoc) empty_assoclist f c)
   | Error msg => Error msg
   end.
 
@@ -406,19 +464,25 @@ Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : na
   match n with
   | S n' =>
     do assoc' <- mi_run f assoc m n';
-    match mi_step_commit (State assoc' empty_assoclist f (Pos.of_nat n')) m with
-    | OK (State assoc _ _ _) => OK assoc
+    match mi_step_commit (Runstate assoc' empty_assoclist f (Pos.of_nat n')) m with
+    | OK (Runstate assoc _ _ _) => OK assoc
     | Error m => Error m
     end
   | O => OK assoc
   end.
 
+(** Resets the module into a known state, so that it can be executed.  This is
+assumed to be the starting state of the module, and may have to be changed if
+other arguments to the module are also to be supported. *)
+
+Definition initial_fextclk (m : module) : fextclk :=
+  fun x => match x with
+           | S O => (add_assoclist (fst (mod_reset m)) (ZToValue 1 1) empty_assoclist)
+           | _ => (add_assoclist (fst (mod_reset m)) (ZToValue 1 0) empty_assoclist)
+           end.
+
 Definition module_run (n : nat) (m : module) : res assoclist :=
-  let f := fun x => match x with
-                    | S O => (add_assoclist (fst (mod_reset m)) (ZToValue 1 1) empty_assoclist)
-                    | _ => (add_assoclist (fst (mod_reset m)) (ZToValue 1 0) empty_assoclist)
-                    end in
-  mi_run f empty_assoclist (mod_body m) n.
+  mi_run (initial_fextclk m) empty_assoclist (mod_body m) n.
 
 Local Close Scope error_monad_scope.
 
@@ -459,4 +523,19 @@ Proof.
       assumption.
 Qed.
 
-*)
+ *)
+
+Inductive initial_state (m: module): state -> Prop :=
+| initial_state_intro:
+    initial_state m (Runstate empty_assoclist empty_assoclist (initial_fextclk m) xH).
+
+(** A final state is a [Returnstate] with an empty call stack. *)
+
+Inductive final_state: state -> int -> Prop :=
+  | final_state_intro: forall r m,
+      final_state (Returnstate nil (Vint r) m) r.
+
+(** The small-step semantics for a module. *)
+
+Definition semantics (p: module) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).
-- 
cgit 


From eee95c4fe9f8b0e1d24224f9c980c16156d9b80d Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 24 Apr 2020 22:16:15 +0100
Subject: Add CompCert semantics for Verilog

---
 src/verilog/Verilog.v | 233 ++++++++++++++++++++++++++++++++------------------
 1 file changed, 152 insertions(+), 81 deletions(-)

(limited to 'src/verilog/Verilog.v')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 4ad297b..a4504c2 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -28,9 +28,8 @@ From Coq Require Import
 Import ListNotations.
 
 From coqup Require Import common.Coquplib common.Show verilog.Value.
-
-From compcert Require Integers.
-From compcert Require Import Errors.
+From compcert Require Integers Events.
+From compcert Require Import Errors Smallstep Globalenvs.
 
 Notation "a ! b" := (PositiveMap.find b a) (at level 1).
 
@@ -157,6 +156,7 @@ Record module : Type := mkmodule {
   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_body : list module_item;
 }.
@@ -172,12 +172,40 @@ Coercion Vvar : reg >-> expr.
 Definition fext := PositiveMap.t value.
 Definition fextclk := nat -> fext.
 
-Inductive state: Type :=
-  Runstate:
-    forall (assoc : assoclist)
+(** ** State
+
+The [state] contains the following items:
+
+- Current [module] that is being worked on, so that the state variable can be
+retrieved and set appropriately.
+- Current [module_item] which is being worked on.
+- A contiunation ([cont]) which defines what to do next.  The option is to
+  either evaluate another module item or go to the next clock cycle.  Finally
+  it could also end if the finish flag of the module goes high.
+- Association list containing the blocking assignments made, or assignments made
+  in previous clock cycles.
+- Nonblocking association list containing all the nonblocking assignments made
+  in the current module.
+- The environment containing values for the input.
+- The program counter which determines the value for the state in this version of
+  Verilog, as the Verilog was generated by the RTL, which means that we have to
+  make an assumption about how it looks.  In this case, that it contains state
+  which determines which part of the Verilog is executed.  This is then the part
+  of the Verilog that should match with the RTL. *)
+
+Inductive state : Type :=
+| Runstate:
+    forall (m : module)
+           (mi : module_item)
+           (mis : list module_item)
+           (assoc : assoclist)
            (nbassoc : assoclist)
            (f : fextclk)
-           (cycle : positive),
+           (cycle : nat)
+           (pc : positive),
+    state
+| Finishstate:
+    forall v : value,
     state.
 
 Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value :=
@@ -212,40 +240,41 @@ Definition unop_run (op : unop) : value -> value :=
   | Vnot => vbitneg
   end.
 
-Inductive expr_runp : state -> expr -> value -> Prop :=
+Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop :=
   | erun_Vlit :
-      forall s v,
-      expr_runp s (Vlit v) v
+      forall fext assoc v,
+      expr_runp fext assoc (Vlit v) v
   | erun_Vvar :
-      forall assoc na f c v r,
+      forall fext assoc v r,
       assoc!r = Some v ->
-      expr_runp (Runstate assoc na f c) (Vvar r) v
+      expr_runp fext assoc (Vvar r) v
   | erun_Vinputvar :
-      forall s r v,
-      expr_runp s (Vinputvar r) v
+      forall fext assoc r v,
+      fext!r = Some v ->
+      expr_runp fext assoc (Vinputvar r) v
   | erun_Vbinop :
-      forall s op l r lv rv oper EQ,
-      expr_runp s l lv ->
-      expr_runp s r rv ->
+      forall fext assoc op l r lv rv oper EQ,
+      expr_runp fext assoc l lv ->
+      expr_runp fext assoc r rv ->
       oper = binop_run op ->
-      expr_runp s (Vbinop op l r) (oper lv rv EQ)
+      expr_runp fext assoc (Vbinop op l r) (oper lv rv EQ)
   | erun_Vunop :
-      forall s u vu op oper,
-      expr_runp s u vu ->
+      forall fext assoc u vu op oper,
+      expr_runp fext assoc u vu ->
       oper = unop_run op ->
-      expr_runp s (Vunop op u) (oper vu)
+      expr_runp fext assoc (Vunop op u) (oper vu)
   | erun_Vternary_true :
-      forall s c ts fs vc vt,
-      expr_runp s c vc ->
-      expr_runp s ts vt ->
+      forall fext assoc c ts fs vc vt,
+      expr_runp fext assoc c vc ->
+      expr_runp fext assoc ts vt ->
       valueToBool vc = true ->
-      expr_runp s (Vternary c ts fs) vt
+      expr_runp fext assoc (Vternary c ts fs) vt
   | erun_Vternary_false :
-      forall s c ts fs vc vf,
-      expr_runp s c vc ->
-      expr_runp s fs vf ->
+      forall fext assoc c ts fs vc vf,
+      expr_runp fext assoc c vc ->
+      expr_runp fext assoc fs vf ->
       valueToBool vc = false ->
-      expr_runp s (Vternary c ts fs) vf.
+      expr_runp fext assoc (Vternary c ts fs) vf.
 
 Definition handle_opt {A : Type} (err : errmsg) (val : option A)
   : res A :=
@@ -263,22 +292,20 @@ Definition handle_def {A : Type} (a : A) (val : option A)
 
 Local Open Scope error_monad_scope.
 
-Definition access_fext (s : state) (r : reg) : res value :=
-  match s with
-  | Runstate _ _ f c =>
-    match PositiveMap.find r (f (Pos.to_nat c)) with
-    | Some v => OK v
-    | _ => OK (ZToValue 1 0)
-    end
+Definition access_fext (f : fext) (r : reg) : res value :=
+  match PositiveMap.find r f with
+  | Some v => OK v
+  | _ => OK (ZToValue 1 0)
   end.
 
 (* TODO FIX Vvar case without default *)
-Fixpoint expr_run (s : state) (e : expr)
+(*Fixpoint expr_run (assoc : assoclist) (e : expr)
          {struct e} : res value :=
   match e with
   | Vlit v => OK v
   | Vvar r => match s with
-              | Runstate assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r
+              | Runstate _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r
+              | _ => Error (msg "Verilog: Wrong state")
               end
   | Vinputvar r => access_fext s r
   | Vbinop op l r =>
@@ -296,7 +323,7 @@ Fixpoint expr_run (s : state) (e : expr)
   | Vternary c te fe =>
     do cv <- expr_run s c;
     if valueToBool cv then expr_run s te else expr_run s fe
-  end.
+  end.*)
 
 (** Return the name of the lhs of an assignment. For now, this function is quite
 simple because only assignment to normal variables is supported and needed. *)
@@ -307,7 +334,7 @@ Definition assign_name (e : expr) : res reg :=
   | _ => Error (msg "Verilog: expression not supported on lhs of assignment")
   end.
 
-Fixpoint stmnt_height (st : stmnt) {struct st} : nat :=
+(*Fixpoint stmnt_height (st : stmnt) {struct st} : nat :=
   match st with
   | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2)
   | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2))
@@ -354,31 +381,38 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
       end
     | Vblock lhs rhs =>
       match s with
-      | Runstate assoc nbassoc f c =>
+      | Runstate m assoc nbassoc f c =>
         do name <- assign_name lhs;
         do rhse <- expr_run s rhs;
-        OK (Runstate (PositiveMap.add name rhse assoc) nbassoc f c)
+        OK (Runstate m (PositiveMap.add name rhse assoc) nbassoc f c)
+      | _ => Error (msg "Verilog: Wrong state")
       end
     | Vnonblock lhs rhs =>
       match s with
-      | Runstate assoc nbassoc f c =>
+      | Runstate m assoc nbassoc f c =>
         do name <- assign_name lhs;
         do rhse <- expr_run s rhs;
-        OK (Runstate assoc (PositiveMap.add name rhse nbassoc) f c)
+        OK (Runstate m assoc (PositiveMap.add name rhse nbassoc) f c)
+      | _ => Error (msg "Verilog: Wrong state")
       end
     end
   | _ => OK s
   end.
 
 Definition stmnt_run (s : state) (st : stmnt) : res state :=
-  stmnt_run' (stmnt_height st) s st.
+  stmnt_run' (stmnt_height st) s st. *)
 
-Inductive not_matched (s : state) (caseval : value) (curr : expr * stmnt) : Prop :=
+Inductive not_matched : state -> value -> expr * stmnt -> Prop :=
   not_in:
-    forall currval,
-    expr_runp s (fst curr) currval ->
+    forall caseval curr currval m mi c assoc nbassoc f cycle pc,
+    expr_runp (f cycle) assoc (fst curr) currval ->
     caseval <> currval ->
-    not_matched s caseval curr.
+    not_matched (Runstate m mi c assoc nbassoc f cycle pc) caseval curr.
+
+Inductive state_fext_assoc : state -> fext * assoclist -> Prop :=
+| get_state_fext_assoc :
+  forall m mi c assoc nbassoc f cycle pc,
+  state_fext_assoc (Runstate m mi c assoc nbassoc f cycle pc) (f cycle, assoc).
 
 Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
 | stmnt_run_Vskip:
@@ -389,49 +423,53 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
     stmnt_runp s1 st2 s2 ->
     stmnt_runp s0 (Vseq st1 st2) s2
 | stmnt_runp_Vcond_true:
-    forall s0 s1 c vc stt stf,
-    expr_runp s0 c vc ->
+    forall s0 f assoc s1 c vc stt stf,
+    state_fext_assoc s0 (f, assoc) ->
+    expr_runp f assoc c vc ->
     valueToBool vc = true ->
     stmnt_runp s0 stt s1 ->
     stmnt_runp s0 (Vcond c stt stf) s1
 | stmnt_runp_Vcond_false:
-    forall s0 s1 c vc stt stf,
-    expr_runp s0 c vc ->
+    forall s0 f assoc s1 c vc stt stf,
+    state_fext_assoc s0 (f, assoc) ->
+    expr_runp f assoc c vc ->
     valueToBool vc = false ->
     stmnt_runp s0 stf s1 ->
     stmnt_runp s0 (Vcond c stt stf) s1
 | stmnt_runp_Vcase:
-    forall e ve s0 s1 me mve sc clst def,
-    expr_runp s0 e ve ->
-    expr_runp s0 me mve ->
+    forall e ve s0 f assoc s1 me mve sc clst def,
+    state_fext_assoc s0 (f, assoc) ->
+    expr_runp f assoc e ve ->
+    expr_runp f assoc me mve ->
     mve = ve ->
     In (me, sc) clst ->
     stmnt_runp s0 sc s1 ->
     stmnt_runp s0 (Vcase e clst def) s1
 | stmnt_runp_Vcase_default:
-    forall s0 st s1 e ve clst,
-    expr_runp s0 e ve ->
+    forall s0 f assoc st s1 e ve clst,
+    state_fext_assoc s0 (f, assoc) ->
+    expr_runp f assoc e ve ->
     Forall (not_matched s0 ve) clst ->
     stmnt_runp s0 st s1 ->
     stmnt_runp s0 (Vcase e clst (Some st)) s1
 | stmnt_runp_Vblock:
-    forall lhs name rhs rhsval s assoc assoc' nbassoc f cycle,
+    forall lhs name rhs rhsval m mi c assoc assoc' nbassoc f cycle pc,
     assign_name lhs = OK name ->
-    expr_runp s rhs rhsval ->
+    expr_runp (f cycle) assoc rhs rhsval ->
     assoc' = (PositiveMap.add name rhsval assoc) ->
-    stmnt_runp (Runstate assoc nbassoc f cycle)
+    stmnt_runp (Runstate m mi c assoc nbassoc f cycle pc)
                (Vblock lhs rhs)
-               (Runstate assoc' nbassoc f cycle)
+               (Runstate m mi c assoc' nbassoc f cycle pc)
 | stmnt_runp_Vnonblock:
-    forall lhs name rhs rhsval s assoc nbassoc nbassoc' f cycle,
+    forall lhs name rhs rhsval m mi c assoc nbassoc nbassoc' f cycle pc,
     assign_name lhs = OK name ->
-    expr_runp s rhs rhsval ->
+    expr_runp (f cycle) assoc rhs rhsval ->
     nbassoc' = (PositiveMap.add name rhsval nbassoc) ->
-    stmnt_runp (Runstate assoc nbassoc f cycle)
+    stmnt_runp (Runstate m mi c assoc nbassoc f cycle pc)
                (Vblock lhs rhs)
-               (Runstate assoc nbassoc' f cycle).
+               (Runstate m mi c assoc nbassoc' f cycle pc).
 
-Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
+(*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
   let run := fun st ls =>
               do s' <- stmnt_run s st;
               mi_step s' ls
@@ -442,7 +480,24 @@ Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
   | (Valways_comb _ st)::ls => run st ls
   | (Vdecl _ _)::ls => mi_step s ls
   | nil => OK s
-  end.
+  end.*)
+
+Inductive mi_stepp : state -> module_item -> state -> Prop :=
+| mi_stepp_Valways :
+    forall s0 st s1 c,
+    stmnt_runp s0 st s1 ->
+    mi_stepp s0 (Valways c st) s1
+| mi_stepp_Valways_ff :
+    forall s0 st s1 c,
+    stmnt_runp s0 st s1 ->
+    mi_stepp s0 (Valways_ff c st) s1
+| mi_stepp_Valways_comb :
+    forall s0 st s1 c,
+    stmnt_runp s0 st s1 ->
+    mi_stepp s0 (Valways_comb c st) s1
+| mi_stepp_Vdecl :
+    forall s lhs rhs,
+    mi_stepp s (Vdecl lhs rhs) s.
 
 Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist :=
   PositiveMap.add r v assoc.
@@ -452,14 +507,15 @@ Definition merge_assoclist (nbassoc assoc : assoclist) : assoclist :=
 
 Definition empty_assoclist : assoclist := PositiveMap.empty value.
 
-Definition mi_step_commit (s : state) (m : list module_item) : res state :=
+(*Definition mi_step_commit (s : state) (m : list module_item) : res state :=
   match mi_step s m with
-  | OK (Runstate assoc nbassoc f c) =>
-    OK (Runstate (merge_assoclist nbassoc assoc) empty_assoclist f c)
+  | OK (Runstate m assoc nbassoc f c) =>
+    OK (Runstate m (merge_assoclist nbassoc assoc) empty_assoclist f c)
   | Error msg => Error msg
-  end.
+  | _ => Error (msg "Verilog: Wrong state")
+  end.*)
 
-Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : nat)
+(*Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : nat)
          {struct n} : res assoclist :=
   match n with
   | S n' =>
@@ -469,7 +525,7 @@ Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : na
     | Error m => Error m
     end
   | O => OK assoc
-  end.
+  end.*)
 
 (** Resets the module into a known state, so that it can be executed.  This is
 assumed to be the starting state of the module, and may have to be changed if
@@ -481,8 +537,8 @@ Definition initial_fextclk (m : module) : fextclk :=
            | _ => (add_assoclist (fst (mod_reset m)) (ZToValue 1 0) empty_assoclist)
            end.
 
-Definition module_run (n : nat) (m : module) : res assoclist :=
-  mi_run (initial_fextclk m) empty_assoclist (mod_body m) n.
+(*Definition module_run (n : nat) (m : module) : res assoclist :=
+  mi_run (initial_fextclk m) empty_assoclist (mod_body m) n.*)
 
 Local Close Scope error_monad_scope.
 
@@ -525,17 +581,32 @@ Qed.
 
  *)
 
+Definition genv := Genv.t unit unit.
+
+Inductive step : genv -> state -> Events.trace -> state -> Prop :=
+| step_module :
+    forall g m mi hmi tmi assoc nbassoc f cycle pc e,
+    step g (Runstate m mi (hmi::tmi) assoc nbassoc f cycle pc) e
+           (Runstate m hmi tmi assoc nbassoc f cycle pc)
+| step_module_empty :
+    forall g tmi hmi m mi assoc nbassoc f cycle pc e,
+    hmi::tmi = mod_body m ->
+    step g (Runstate m mi nil assoc nbassoc f cycle pc) e
+           (Runstate m hmi tmi assoc nbassoc f (S cycle) pc).
+
 Inductive initial_state (m: module): state -> Prop :=
 | initial_state_intro:
-    initial_state m (Runstate empty_assoclist empty_assoclist (initial_fextclk m) xH).
+    forall hmi tmi,
+    hmi::tmi = mod_body m ->
+    initial_state m (Runstate m hmi tmi empty_assoclist empty_assoclist (initial_fextclk m) O xH).
 
 (** A final state is a [Returnstate] with an empty call stack. *)
 
-Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall r m,
-      final_state (Returnstate nil (Vint r) m) r.
+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.globalenv p).
+  Semantics step (initial_state p) final_state (Genv.empty_genv unit unit nil).
-- 
cgit 


From 8f370a52a5424389d9f0b4b044020932a2febfd4 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 3 May 2020 17:12:09 +0100
Subject: Change to State

---
 src/verilog/Verilog.v | 43 ++++++++++++++++++++++---------------------
 1 file changed, 22 insertions(+), 21 deletions(-)

(limited to 'src/verilog/Verilog.v')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index a4504c2..7a3982c 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -194,7 +194,7 @@ retrieved and set appropriately.
   of the Verilog that should match with the RTL. *)
 
 Inductive state : Type :=
-| Runstate:
+| State:
     forall (m : module)
            (mi : module_item)
            (mis : list module_item)
@@ -304,7 +304,7 @@ Definition access_fext (f : fext) (r : reg) : res value :=
   match e with
   | Vlit v => OK v
   | Vvar r => match s with
-              | Runstate _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r
+              | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r
               | _ => Error (msg "Verilog: Wrong state")
               end
   | Vinputvar r => access_fext s r
@@ -381,18 +381,18 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
       end
     | Vblock lhs rhs =>
       match s with
-      | Runstate m assoc nbassoc f c =>
+      | State m assoc nbassoc f c =>
         do name <- assign_name lhs;
         do rhse <- expr_run s rhs;
-        OK (Runstate m (PositiveMap.add name rhse assoc) nbassoc f c)
+        OK (State m (PositiveMap.add name rhse assoc) nbassoc f c)
       | _ => Error (msg "Verilog: Wrong state")
       end
     | Vnonblock lhs rhs =>
       match s with
-      | Runstate m assoc nbassoc f c =>
+      | State m assoc nbassoc f c =>
         do name <- assign_name lhs;
         do rhse <- expr_run s rhs;
-        OK (Runstate m assoc (PositiveMap.add name rhse nbassoc) f c)
+        OK (State m assoc (PositiveMap.add name rhse nbassoc) f c)
       | _ => Error (msg "Verilog: Wrong state")
       end
     end
@@ -407,12 +407,12 @@ Inductive not_matched : state -> value -> expr * stmnt -> Prop :=
     forall caseval curr currval m mi c assoc nbassoc f cycle pc,
     expr_runp (f cycle) assoc (fst curr) currval ->
     caseval <> currval ->
-    not_matched (Runstate m mi c assoc nbassoc f cycle pc) caseval curr.
+    not_matched (State m mi c assoc nbassoc f cycle pc) caseval curr.
 
 Inductive state_fext_assoc : state -> fext * assoclist -> Prop :=
 | get_state_fext_assoc :
   forall m mi c assoc nbassoc f cycle pc,
-  state_fext_assoc (Runstate m mi c assoc nbassoc f cycle pc) (f cycle, assoc).
+  state_fext_assoc (State m mi c assoc nbassoc f cycle pc) (f cycle, assoc).
 
 Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
 | stmnt_run_Vskip:
@@ -457,17 +457,17 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
     assign_name lhs = OK name ->
     expr_runp (f cycle) assoc rhs rhsval ->
     assoc' = (PositiveMap.add name rhsval assoc) ->
-    stmnt_runp (Runstate m mi c assoc nbassoc f cycle pc)
+    stmnt_runp (State m mi c assoc nbassoc f cycle pc)
                (Vblock lhs rhs)
-               (Runstate m mi c assoc' nbassoc f cycle pc)
+               (State m mi c assoc' nbassoc f cycle pc)
 | stmnt_runp_Vnonblock:
     forall lhs name rhs rhsval m mi c assoc nbassoc nbassoc' f cycle pc,
     assign_name lhs = OK name ->
     expr_runp (f cycle) assoc rhs rhsval ->
     nbassoc' = (PositiveMap.add name rhsval nbassoc) ->
-    stmnt_runp (Runstate m mi c assoc nbassoc f cycle pc)
+    stmnt_runp (State m mi c assoc nbassoc f cycle pc)
                (Vblock lhs rhs)
-               (Runstate m mi c assoc nbassoc' f cycle pc).
+               (State m mi c assoc nbassoc' f cycle pc).
 
 (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
   let run := fun st ls =>
@@ -509,8 +509,8 @@ Definition empty_assoclist : assoclist := PositiveMap.empty value.
 
 (*Definition mi_step_commit (s : state) (m : list module_item) : res state :=
   match mi_step s m with
-  | OK (Runstate m assoc nbassoc f c) =>
-    OK (Runstate m (merge_assoclist nbassoc assoc) empty_assoclist f c)
+  | OK (State m assoc nbassoc f c) =>
+    OK (State m (merge_assoclist nbassoc assoc) empty_assoclist f c)
   | Error msg => Error msg
   | _ => Error (msg "Verilog: Wrong state")
   end.*)
@@ -520,8 +520,8 @@ Definition empty_assoclist : assoclist := PositiveMap.empty value.
   match n with
   | S n' =>
     do assoc' <- mi_run f assoc m n';
-    match mi_step_commit (Runstate assoc' empty_assoclist f (Pos.of_nat n')) m with
-    | OK (Runstate assoc _ _ _) => OK assoc
+    match mi_step_commit (State assoc' empty_assoclist f (Pos.of_nat n')) m with
+    | OK (State assoc _ _ _) => OK assoc
     | Error m => Error m
     end
   | O => OK assoc
@@ -583,22 +583,23 @@ Qed.
 
 Definition genv := Genv.t unit unit.
 
+
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
     forall g m mi hmi tmi assoc nbassoc f cycle pc e,
-    step g (Runstate m mi (hmi::tmi) assoc nbassoc f cycle pc) e
-           (Runstate m hmi tmi assoc nbassoc f cycle pc)
+    step_cc g (State m mi (hmi::tmi) assoc nbassoc f cycle pc) e
+            (State m hmi tmi assoc nbassoc f cycle pc)
 | step_module_empty :
     forall g tmi hmi m mi assoc nbassoc f cycle pc e,
     hmi::tmi = mod_body m ->
-    step g (Runstate m mi nil assoc nbassoc f cycle pc) e
-           (Runstate m hmi tmi assoc nbassoc f (S cycle) pc).
+    step_cc g (State m mi nil assoc nbassoc f cycle pc) e
+            (State m hmi tmi assoc nbassoc f (S cycle) pc).
 
 Inductive initial_state (m: module): state -> Prop :=
 | initial_state_intro:
     forall hmi tmi,
     hmi::tmi = mod_body m ->
-    initial_state m (Runstate m hmi tmi empty_assoclist empty_assoclist (initial_fextclk m) O xH).
+    initial_state m (State m hmi tmi empty_assoclist empty_assoclist (initial_fextclk m) O xH).
 
 (** A final state is a [Returnstate] with an empty call stack. *)
 
-- 
cgit 


From c106b109fa0d469568c4841f07f7243a4f7813a4 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 4 May 2020 12:08:04 +0100
Subject: Refine the semantics

---
 src/verilog/Verilog.v | 105 ++++++++++++++++++++++++++++++--------------------
 1 file changed, 63 insertions(+), 42 deletions(-)

(limited to 'src/verilog/Verilog.v')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 7a3982c..a927eac 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -31,6 +31,8 @@ From coqup Require Import common.Coquplib common.Show verilog.Value.
 From compcert Require Integers Events.
 From compcert Require Import Errors Smallstep Globalenvs.
 
+Import HexNotationValue.
+
 Notation "a ! b" := (PositiveMap.find b a) (at level 1).
 
 Definition reg : Type := positive.
@@ -196,13 +198,11 @@ retrieved and set appropriately.
 Inductive state : Type :=
 | State:
     forall (m : module)
-           (mi : module_item)
-           (mis : list module_item)
            (assoc : assoclist)
            (nbassoc : assoclist)
            (f : fextclk)
            (cycle : nat)
-           (pc : positive),
+           (stvar : value),
     state
 | Finishstate:
     forall v : value,
@@ -248,21 +248,27 @@ Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop :=
       forall fext assoc v r,
       assoc!r = Some v ->
       expr_runp fext assoc (Vvar r) v
+  | erun_Vvar_empty :
+      forall fext assoc r sz,
+      assoc!r = None ->
+      expr_runp fext assoc (Vvar r) (ZToValue sz 0)
   | erun_Vinputvar :
       forall fext assoc r v,
       fext!r = Some v ->
       expr_runp fext assoc (Vinputvar r) v
   | erun_Vbinop :
-      forall fext assoc op l r lv rv oper EQ,
+      forall fext assoc op l r lv rv oper EQ resv,
       expr_runp fext assoc l lv ->
       expr_runp fext assoc r rv ->
       oper = binop_run op ->
-      expr_runp fext assoc (Vbinop op l r) (oper lv rv EQ)
+      resv = oper lv rv EQ ->
+      expr_runp fext assoc (Vbinop op l r) resv
   | erun_Vunop :
-      forall fext assoc u vu op oper,
+      forall fext assoc u vu op oper resv,
       expr_runp fext assoc u vu ->
       oper = unop_run op ->
-      expr_runp fext assoc (Vunop op u) (oper vu)
+      resv = oper vu ->
+      expr_runp fext assoc (Vunop op u) resv
   | erun_Vternary_true :
       forall fext assoc c ts fs vc vt,
       expr_runp fext assoc c vc ->
@@ -402,17 +408,10 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
 Definition stmnt_run (s : state) (st : stmnt) : res state :=
   stmnt_run' (stmnt_height st) s st. *)
 
-Inductive not_matched : state -> value -> expr * stmnt -> Prop :=
-  not_in:
-    forall caseval curr currval m mi c assoc nbassoc f cycle pc,
-    expr_runp (f cycle) assoc (fst curr) currval ->
-    caseval <> currval ->
-    not_matched (State m mi c assoc nbassoc f cycle pc) caseval curr.
-
 Inductive state_fext_assoc : state -> fext * assoclist -> Prop :=
 | get_state_fext_assoc :
-  forall m mi c assoc nbassoc f cycle pc,
-  state_fext_assoc (State m mi c assoc nbassoc f cycle pc) (f cycle, assoc).
+  forall c assoc nbassoc f cycle pc,
+  state_fext_assoc (State c assoc nbassoc f cycle pc) (f cycle, assoc).
 
 Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
 | stmnt_run_Vskip:
@@ -436,38 +435,44 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
     valueToBool vc = false ->
     stmnt_runp s0 stf s1 ->
     stmnt_runp s0 (Vcond c stt stf) s1
-| stmnt_runp_Vcase:
-    forall e ve s0 f assoc s1 me mve sc clst def,
+| stmnt_runp_Vcase_match:
+    forall e ve s0 f assoc s1 me mve sc cs def,
     state_fext_assoc s0 (f, assoc) ->
     expr_runp f assoc e ve ->
     expr_runp f assoc me mve ->
     mve = ve ->
-    In (me, sc) clst ->
     stmnt_runp s0 sc s1 ->
-    stmnt_runp s0 (Vcase e clst def) s1
+    stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1
+| stmnt_runp_Vcase_nomatch:
+    forall e ve s0 f assoc s1 me mve sc cs def,
+    state_fext_assoc s0 (f, assoc) ->
+    expr_runp f assoc e ve ->
+    expr_runp f assoc me mve ->
+    mve <> ve ->
+    stmnt_runp s0 (Vcase e cs def) s1 ->
+    stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1
 | stmnt_runp_Vcase_default:
-    forall s0 f assoc st s1 e ve clst,
+    forall s0 f assoc st s1 e ve,
     state_fext_assoc s0 (f, assoc) ->
     expr_runp f assoc e ve ->
-    Forall (not_matched s0 ve) clst ->
     stmnt_runp s0 st s1 ->
-    stmnt_runp s0 (Vcase e clst (Some st)) s1
+    stmnt_runp s0 (Vcase e nil (Some st)) s1
 | stmnt_runp_Vblock:
-    forall lhs name rhs rhsval m mi c assoc assoc' nbassoc f cycle pc,
+    forall lhs name rhs rhsval c assoc assoc' nbassoc f cycle pc,
     assign_name lhs = OK name ->
     expr_runp (f cycle) assoc rhs rhsval ->
     assoc' = (PositiveMap.add name rhsval assoc) ->
-    stmnt_runp (State m mi c assoc nbassoc f cycle pc)
+    stmnt_runp (State c assoc nbassoc f cycle pc)
                (Vblock lhs rhs)
-               (State m mi c assoc' nbassoc f cycle pc)
+               (State c assoc' nbassoc f cycle pc)
 | stmnt_runp_Vnonblock:
-    forall lhs name rhs rhsval m mi c assoc nbassoc nbassoc' f cycle pc,
+    forall lhs name rhs rhsval c assoc nbassoc nbassoc' f cycle pc,
     assign_name lhs = OK name ->
     expr_runp (f cycle) assoc rhs rhsval ->
     nbassoc' = (PositiveMap.add name rhsval nbassoc) ->
-    stmnt_runp (State m mi c assoc nbassoc f cycle pc)
-               (Vblock lhs rhs)
-               (State m mi c assoc nbassoc' f cycle pc).
+    stmnt_runp (State c assoc nbassoc f cycle pc)
+               (Vnonblock lhs rhs)
+               (State c assoc nbassoc' f cycle pc).
 
 (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
   let run := fun st ls =>
@@ -499,6 +504,16 @@ Inductive mi_stepp : state -> module_item -> state -> Prop :=
     forall s lhs rhs,
     mi_stepp s (Vdecl lhs rhs) s.
 
+Inductive mis_stepp : state -> list module_item -> state -> Prop :=
+| mis_stepp_Cons :
+    forall mi mis s0 s1 s2,
+    mi_stepp s0 mi s1 ->
+    mis_stepp s1 mis s2 ->
+    mis_stepp s0 (mi :: mis) s2
+| mis_stepp_Nil :
+    forall s,
+    mis_stepp s nil s.
+
 Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist :=
   PositiveMap.add r v assoc.
 
@@ -583,19 +598,24 @@ Qed.
 
 Definition genv := Genv.t unit unit.
 
-
-Inductive step : genv -> state -> Events.trace -> state -> Prop :=
+Inductive step : state -> state -> Prop :=
 | step_module :
-    forall g m mi hmi tmi assoc nbassoc f cycle pc e,
-    step_cc g (State m mi (hmi::tmi) assoc nbassoc f cycle pc) e
-            (State m hmi tmi assoc nbassoc f cycle pc)
-| step_module_empty :
-    forall g tmi hmi m mi assoc nbassoc f cycle pc e,
-    hmi::tmi = mod_body m ->
-    step_cc g (State m mi nil assoc nbassoc f cycle pc) e
-            (State m hmi tmi assoc nbassoc f (S cycle) pc).
-
-Inductive initial_state (m: module): state -> Prop :=
+    forall m stvar stvar' cycle f assoc0 assoc1 assoc2 nbassoc,
+    mis_stepp (State m assoc0 empty_assoclist f cycle stvar)
+              m.(mod_body)
+              (State m assoc1 nbassoc f cycle stvar) ->
+    assoc2 = merge_assoclist nbassoc assoc1 ->
+    Some stvar' = assoc2!(fst m.(mod_state)) ->
+    step (State m assoc0 empty_assoclist f cycle stvar)
+         (State m assoc2 empty_assoclist 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_assoclist f cycle stvar)
+         (Finishstate result).
+
+(*Inductive initial_state (m: module): state -> Prop :=
 | initial_state_intro:
     forall hmi tmi,
     hmi::tmi = mod_body m ->
@@ -611,3 +631,4 @@ Inductive final_state: state -> Integers.int -> Prop :=
 
 Definition semantics (p: module) :=
   Semantics step (initial_state p) final_state (Genv.empty_genv unit unit nil).
+*)
-- 
cgit 


From 5cfa4af9c6e4d9703e3142c24ae78c7da0ac575f Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 4 May 2020 16:13:16 +0100
Subject: Add equality check for value

---
 src/verilog/Verilog.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/verilog/Verilog.v')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index a927eac..756dc12 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq -*-
+(*
  * CoqUp: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
  *
-- 
cgit 


From 5d4aed9030565349a83f9ede4bd35c020eb416b5 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 5 May 2020 00:38:19 +0100
Subject: Simplifications to proof

---
 src/verilog/Verilog.v | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'src/verilog/Verilog.v')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 756dc12..399bff7 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -281,6 +281,7 @@ Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop :=
       expr_runp fext assoc fs vf ->
       valueToBool vc = false ->
       expr_runp fext assoc (Vternary c ts fs) vf.
+Hint Constructors expr_runp : verilog.
 
 Definition handle_opt {A : Type} (err : errmsg) (val : option A)
   : res A :=
@@ -412,11 +413,12 @@ Inductive state_fext_assoc : state -> fext * assoclist -> Prop :=
 | get_state_fext_assoc :
   forall c assoc nbassoc f cycle pc,
   state_fext_assoc (State c assoc nbassoc f cycle pc) (f cycle, assoc).
+Hint Constructors state_fext_assoc : verilog.
 
 Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
-| stmnt_run_Vskip:
+| stmnt_runp_Vskip:
     forall s, stmnt_runp s Vskip s
-| stmnt_run_Vseq:
+| stmnt_runp_Vseq:
     forall st1 st2 s0 s1 s2,
     stmnt_runp s0 st1 s1 ->
     stmnt_runp s1 st2 s2 ->
@@ -473,6 +475,7 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
     stmnt_runp (State c assoc nbassoc f cycle pc)
                (Vnonblock lhs rhs)
                (State c assoc nbassoc' f cycle pc).
+Hint Constructors stmnt_runp : verilog.
 
 (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
   let run := fun st ls =>
@@ -503,6 +506,7 @@ Inductive mi_stepp : state -> module_item -> state -> Prop :=
 | mi_stepp_Vdecl :
     forall s lhs rhs,
     mi_stepp s (Vdecl lhs rhs) s.
+Hint Constructors mi_stepp : verilog.
 
 Inductive mis_stepp : state -> list module_item -> state -> Prop :=
 | mis_stepp_Cons :
@@ -513,6 +517,7 @@ Inductive mis_stepp : state -> list module_item -> state -> Prop :=
 | mis_stepp_Nil :
     forall s,
     mis_stepp s nil s.
+Hint Constructors mis_stepp : verilog.
 
 Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist :=
   PositiveMap.add r v assoc.
@@ -614,6 +619,7 @@ Inductive step : state -> state -> Prop :=
     assoc!(fst m.(mod_return)) = Some result ->
     step (State m assoc empty_assoclist f cycle stvar)
          (Finishstate result).
+Hint Constructors step : verilog.
 
 (*Inductive initial_state (m: module): state -> Prop :=
 | initial_state_intro:
-- 
cgit 


From 4d409fe68c693dd083295f35bd5af8bdec6d2632 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 5 May 2020 01:16:03 +0100
Subject: Minimised manual simulation

---
 src/verilog/Verilog.v | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'src/verilog/Verilog.v')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 399bff7..451b452 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -244,14 +244,14 @@ Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop :=
   | erun_Vlit :
       forall fext assoc v,
       expr_runp fext assoc (Vlit v) v
-  | erun_Vvar :
-      forall fext assoc v r,
-      assoc!r = Some v ->
-      expr_runp fext assoc (Vvar r) v
   | erun_Vvar_empty :
       forall fext assoc r sz,
       assoc!r = None ->
       expr_runp fext assoc (Vvar r) (ZToValue sz 0)
+  | erun_Vvar :
+      forall fext assoc v r,
+      assoc!r = Some v ->
+      expr_runp fext assoc (Vvar r) v
   | erun_Vinputvar :
       forall fext assoc r v,
       fext!r = Some v ->
@@ -437,21 +437,21 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
     valueToBool vc = false ->
     stmnt_runp s0 stf s1 ->
     stmnt_runp s0 (Vcond c stt stf) s1
-| stmnt_runp_Vcase_match:
+| stmnt_runp_Vcase_nomatch:
     forall e ve s0 f assoc s1 me mve sc cs def,
     state_fext_assoc s0 (f, assoc) ->
     expr_runp f assoc e ve ->
     expr_runp f assoc me mve ->
-    mve = ve ->
-    stmnt_runp s0 sc s1 ->
+    mve <> ve ->
+    stmnt_runp s0 (Vcase e cs def) s1 ->
     stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1
-| stmnt_runp_Vcase_nomatch:
+| stmnt_runp_Vcase_match:
     forall e ve s0 f assoc s1 me mve sc cs def,
     state_fext_assoc s0 (f, assoc) ->
     expr_runp f assoc e ve ->
     expr_runp f assoc me mve ->
-    mve <> ve ->
-    stmnt_runp s0 (Vcase e cs def) s1 ->
+    mve = ve ->
+    stmnt_runp s0 sc s1 ->
     stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1
 | stmnt_runp_Vcase_default:
     forall s0 f assoc st s1 e ve,
-- 
cgit 


From c8535e1f454c7014c7b794fc8be343e2fda97937 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 7 May 2020 17:21:51 +0100
Subject: Rename assoclist to assocset

---
 src/verilog/Verilog.v | 50 +++++++++++++++++++++++++-------------------------
 1 file changed, 25 insertions(+), 25 deletions(-)

(limited to 'src/verilog/Verilog.v')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 451b452..a35fb58 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -39,7 +39,7 @@ Definition reg : Type := positive.
 Definition node : Type := positive.
 Definition szreg : Type := reg * nat.
 
-Definition assoclist : Type := PositiveMap.t value.
+Definition assocset : Type := PositiveMap.t value.
 
 (** * Verilog AST
 
@@ -52,7 +52,7 @@ 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 := assoclist * assoclist.
+Definition estate : Type := assocset * assocset.
 
 (** ** Binary Operators
 
@@ -198,8 +198,8 @@ retrieved and set appropriately.
 Inductive state : Type :=
 | State:
     forall (m : module)
-           (assoc : assoclist)
-           (nbassoc : assoclist)
+           (assoc : assocset)
+           (nbassoc : assocset)
            (f : fextclk)
            (cycle : nat)
            (stvar : value),
@@ -240,7 +240,7 @@ Definition unop_run (op : unop) : value -> value :=
   | Vnot => vbitneg
   end.
 
-Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop :=
+Inductive expr_runp : fext -> assocset -> expr -> value -> Prop :=
   | erun_Vlit :
       forall fext assoc v,
       expr_runp fext assoc (Vlit v) v
@@ -306,7 +306,7 @@ Definition access_fext (f : fext) (r : reg) : res value :=
   end.
 
 (* TODO FIX Vvar case without default *)
-(*Fixpoint expr_run (assoc : assoclist) (e : expr)
+(*Fixpoint expr_run (assoc : assocset) (e : expr)
          {struct e} : res value :=
   match e with
   | Vlit v => OK v
@@ -409,7 +409,7 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
 Definition stmnt_run (s : state) (st : stmnt) : res state :=
   stmnt_run' (stmnt_height st) s st. *)
 
-Inductive state_fext_assoc : state -> fext * assoclist -> Prop :=
+Inductive state_fext_assoc : state -> fext * assocset -> Prop :=
 | get_state_fext_assoc :
   forall c assoc nbassoc f cycle pc,
   state_fext_assoc (State c assoc nbassoc f cycle pc) (f cycle, assoc).
@@ -519,28 +519,28 @@ Inductive mis_stepp : state -> list module_item -> state -> Prop :=
     mis_stepp s nil s.
 Hint Constructors mis_stepp : verilog.
 
-Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist :=
+Definition add_assocset (r : reg) (v : value) (assoc : assocset) : assocset :=
   PositiveMap.add r v assoc.
 
-Definition merge_assoclist (nbassoc assoc : assoclist) : assoclist :=
-  PositiveMap.fold add_assoclist nbassoc assoc.
+Definition merge_assocset (nbassoc assoc : assocset) : assocset :=
+  PositiveMap.fold add_assocset nbassoc assoc.
 
-Definition empty_assoclist : assoclist := PositiveMap.empty value.
+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_assoclist nbassoc assoc) empty_assoclist f c)
+    OK (State m (merge_assocset nbassoc assoc) empty_assocset f c)
   | Error msg => Error msg
   | _ => Error (msg "Verilog: Wrong state")
   end.*)
 
-(*Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : nat)
-         {struct n} : res assoclist :=
+(*Fixpoint mi_run (f : fextclk) (assoc : assocset) (m : list module_item) (n : nat)
+         {struct n} : res assocset :=
   match n with
   | S n' =>
     do assoc' <- mi_run f assoc m n';
-    match mi_step_commit (State assoc' empty_assoclist f (Pos.of_nat n')) m with
+    match mi_step_commit (State assoc' empty_assocset f (Pos.of_nat n')) m with
     | OK (State assoc _ _ _) => OK assoc
     | Error m => Error m
     end
@@ -553,12 +553,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_assoclist (fst (mod_reset m)) (ZToValue 1 1) empty_assoclist)
-           | _ => (add_assoclist (fst (mod_reset m)) (ZToValue 1 0) empty_assoclist)
+           | S O => (add_assocset (fst (mod_reset m)) (ZToValue 1 1) empty_assocset)
+           | _ => (add_assocset (fst (mod_reset m)) (ZToValue 1 0) empty_assocset)
            end.
 
-(*Definition module_run (n : nat) (m : module) : res assoclist :=
-  mi_run (initial_fextclk m) empty_assoclist (mod_body m) n.*)
+(*Definition module_run (n : nat) (m : module) : res assocset :=
+  mi_run (initial_fextclk m) empty_assocset (mod_body m) n.*)
 
 Local Close Scope error_monad_scope.
 
@@ -606,18 +606,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 (State m assoc0 empty_assoclist f cycle stvar)
+    mis_stepp (State m assoc0 empty_assocset f cycle stvar)
               m.(mod_body)
               (State m assoc1 nbassoc f cycle stvar) ->
-    assoc2 = merge_assoclist nbassoc assoc1 ->
+    assoc2 = merge_assocset nbassoc assoc1 ->
     Some stvar' = assoc2!(fst m.(mod_state)) ->
-    step (State m assoc0 empty_assoclist f cycle stvar)
-         (State m assoc2 empty_assoclist f (S cycle) stvar')
+    step (State m assoc0 empty_assocset f cycle stvar)
+         (State m assoc2 empty_assocset 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_assoclist f cycle stvar)
+    step (State m assoc empty_assocset f cycle stvar)
          (Finishstate result).
 Hint Constructors step : verilog.
 
@@ -625,7 +625,7 @@ Hint Constructors step : verilog.
 | initial_state_intro:
     forall hmi tmi,
     hmi::tmi = mod_body m ->
-    initial_state m (State m hmi tmi empty_assoclist empty_assoclist (initial_fextclk m) O xH).
+    initial_state m (State m hmi tmi empty_assocset empty_assocset (initial_fextclk m) O xH).
 
 (** A final state is a [Returnstate] with an empty call stack. *)
 
-- 
cgit 


From fa39e09d403cfba1b1e6c359362e54600dfc28b0 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 7 May 2020 23:12:59 +0100
Subject: Use associations instead of state

---
 src/verilog/Verilog.v | 135 ++++++++++++++++++++++++--------------------------
 1 file changed, 65 insertions(+), 70 deletions(-)

(limited to 'src/verilog/Verilog.v')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index a35fb58..ba7e83d 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -41,6 +41,12 @@ Definition szreg : Type := reg * nat.
 
 Definition assocset : Type := PositiveMap.t value.
 
+Record associations : Type :=
+  mkassociations {
+    assoc_blocking : assocset;
+    assoc_nonblocking : assocset
+  }.
+
 (** * Verilog AST
 
 The Verilog AST is defined here, which is the target language of the
@@ -409,72 +415,61 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
 Definition stmnt_run (s : state) (st : stmnt) : res state :=
   stmnt_run' (stmnt_height st) s st. *)
 
-Inductive state_fext_assoc : state -> fext * assocset -> Prop :=
-| get_state_fext_assoc :
-  forall c assoc nbassoc f cycle pc,
-  state_fext_assoc (State c assoc nbassoc f cycle pc) (f cycle, assoc).
-Hint Constructors state_fext_assoc : verilog.
-
-Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
+Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop :=
 | stmnt_runp_Vskip:
-    forall s, stmnt_runp s Vskip s
+    forall f a, stmnt_runp f a Vskip a
 | stmnt_runp_Vseq:
-    forall st1 st2 s0 s1 s2,
-    stmnt_runp s0 st1 s1 ->
-    stmnt_runp s1 st2 s2 ->
-    stmnt_runp s0 (Vseq st1 st2) s2
+    forall f st1 st2 as0 as1 as2,
+    stmnt_runp f as0 st1 as1 ->
+    stmnt_runp f as1 st2 as2 ->
+    stmnt_runp f as0 (Vseq st1 st2) as2
 | stmnt_runp_Vcond_true:
-    forall s0 f assoc s1 c vc stt stf,
-    state_fext_assoc s0 (f, assoc) ->
-    expr_runp f assoc c vc ->
+    forall as0 as1 f c vc stt stf,
+    expr_runp f as0.(assoc_blocking) c vc ->
     valueToBool vc = true ->
-    stmnt_runp s0 stt s1 ->
-    stmnt_runp s0 (Vcond c stt stf) s1
+    stmnt_runp f as0 stt as1 ->
+    stmnt_runp f as0 (Vcond c stt stf) as1
 | stmnt_runp_Vcond_false:
-    forall s0 f assoc s1 c vc stt stf,
-    state_fext_assoc s0 (f, assoc) ->
-    expr_runp f assoc c vc ->
+    forall as0 as1 f c vc stt stf,
+    expr_runp f as0.(assoc_blocking) c vc ->
     valueToBool vc = false ->
-    stmnt_runp s0 stf s1 ->
-    stmnt_runp s0 (Vcond c stt stf) s1
+    stmnt_runp f as0 stf as1 ->
+    stmnt_runp f as0 (Vcond c stt stf) as1
 | stmnt_runp_Vcase_nomatch:
-    forall e ve s0 f assoc s1 me mve sc cs def,
-    state_fext_assoc s0 (f, assoc) ->
-    expr_runp f assoc e ve ->
-    expr_runp f assoc me mve ->
+    forall e ve as0 f as1 me mve sc cs def,
+    expr_runp f as0.(assoc_blocking) e ve ->
+    expr_runp f as0.(assoc_blocking) me mve ->
     mve <> ve ->
-    stmnt_runp s0 (Vcase e cs def) s1 ->
-    stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1
+    stmnt_runp f as0 (Vcase e cs def) as1 ->
+    stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1
 | stmnt_runp_Vcase_match:
-    forall e ve s0 f assoc s1 me mve sc cs def,
-    state_fext_assoc s0 (f, assoc) ->
-    expr_runp f assoc e ve ->
-    expr_runp f assoc me mve ->
+    forall e ve as0 f as1 me mve sc cs def,
+    expr_runp f as0.(assoc_blocking) e ve ->
+    expr_runp f as0.(assoc_blocking) me mve ->
     mve = ve ->
-    stmnt_runp s0 sc s1 ->
-    stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1
+    stmnt_runp f as0 sc as1 ->
+    stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1
 | stmnt_runp_Vcase_default:
-    forall s0 f assoc st s1 e ve,
-    state_fext_assoc s0 (f, assoc) ->
-    expr_runp f assoc e ve ->
-    stmnt_runp s0 st s1 ->
-    stmnt_runp s0 (Vcase e nil (Some st)) s1
+    forall as0 as1 f st e ve,
+    expr_runp f as0.(assoc_blocking) e ve ->
+    stmnt_runp f as0 st as1 ->
+    stmnt_runp f as0 (Vcase e nil (Some st)) as1
 | stmnt_runp_Vblock:
-    forall lhs name rhs rhsval c assoc assoc' nbassoc f cycle pc,
+    forall lhs name rhs rhsval assoc assoc' nbassoc f,
     assign_name lhs = OK name ->
-    expr_runp (f cycle) assoc rhs rhsval ->
+    expr_runp f assoc rhs rhsval ->
     assoc' = (PositiveMap.add name rhsval assoc) ->
-    stmnt_runp (State c assoc nbassoc f cycle pc)
-               (Vblock lhs rhs)
-               (State c assoc' nbassoc f cycle pc)
+    stmnt_runp f (mkassociations assoc nbassoc)
+                 (Vblock lhs rhs)
+                 (mkassociations assoc nbassoc)
 | stmnt_runp_Vnonblock:
-    forall lhs name rhs rhsval c assoc nbassoc nbassoc' f cycle pc,
+    forall lhs name rhs rhsval assoc nbassoc nbassoc' f,
     assign_name lhs = OK name ->
-    expr_runp (f cycle) assoc rhs rhsval ->
+    expr_runp f assoc rhs rhsval ->
     nbassoc' = (PositiveMap.add name rhsval nbassoc) ->
-    stmnt_runp (State c assoc nbassoc f cycle pc)
-               (Vnonblock lhs rhs)
-               (State c assoc nbassoc' f cycle pc).
+    stmnt_runp f (mkassociations assoc nbassoc)
+                 (Vnonblock lhs rhs)
+                 (mkassociations assoc nbassoc').
 Hint Constructors stmnt_runp : verilog.
 
 (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
@@ -490,33 +485,33 @@ Hint Constructors stmnt_runp : verilog.
   | nil => OK s
   end.*)
 
-Inductive mi_stepp : state -> module_item -> state -> Prop :=
+Inductive mi_stepp : fext -> associations -> module_item -> associations -> Prop :=
 | mi_stepp_Valways :
-    forall s0 st s1 c,
-    stmnt_runp s0 st s1 ->
-    mi_stepp s0 (Valways c st) s1
+    forall f s0 st s1 c,
+    stmnt_runp f s0 st s1 ->
+    mi_stepp f s0 (Valways c st) s1
 | mi_stepp_Valways_ff :
-    forall s0 st s1 c,
-    stmnt_runp s0 st s1 ->
-    mi_stepp s0 (Valways_ff c st) s1
+    forall f s0 st s1 c,
+    stmnt_runp f s0 st s1 ->
+    mi_stepp f s0 (Valways_ff c st) s1
 | mi_stepp_Valways_comb :
-    forall s0 st s1 c,
-    stmnt_runp s0 st s1 ->
-    mi_stepp s0 (Valways_comb c st) s1
+    forall f s0 st s1 c,
+    stmnt_runp f s0 st s1 ->
+    mi_stepp f s0 (Valways_comb c st) s1
 | mi_stepp_Vdecl :
-    forall s lhs rhs,
-    mi_stepp s (Vdecl lhs rhs) s.
+    forall f s lhs rhs,
+    mi_stepp f s (Vdecl lhs rhs) s.
 Hint Constructors mi_stepp : verilog.
 
-Inductive mis_stepp : state -> list module_item -> state -> Prop :=
+Inductive mis_stepp : fext -> associations -> list module_item -> associations -> Prop :=
 | mis_stepp_Cons :
-    forall mi mis s0 s1 s2,
-    mi_stepp s0 mi s1 ->
-    mis_stepp s1 mis s2 ->
-    mis_stepp s0 (mi :: mis) s2
+    forall f mi mis s0 s1 s2,
+    mi_stepp f s0 mi s1 ->
+    mis_stepp f s1 mis s2 ->
+    mis_stepp f s0 (mi :: mis) s2
 | mis_stepp_Nil :
-    forall s,
-    mis_stepp s nil s.
+    forall f s,
+    mis_stepp f s nil s.
 Hint Constructors mis_stepp : verilog.
 
 Definition add_assocset (r : reg) (v : value) (assoc : assocset) : assocset :=
@@ -606,9 +601,9 @@ 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 (State m assoc0 empty_assocset f cycle stvar)
+    mis_stepp (f cycle) (mkassociations assoc0 empty_assocset)
               m.(mod_body)
-              (State m assoc1 nbassoc f cycle stvar) ->
+              (mkassociations assoc1 nbassoc) ->
     assoc2 = merge_assocset nbassoc assoc1 ->
     Some stvar' = assoc2!(fst m.(mod_state)) ->
     step (State m assoc0 empty_assocset f cycle stvar)
-- 
cgit 


From 32990af23915c15e5cfd4cfe32c47cafa508f11d Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 8 May 2020 23:34:15 +0100
Subject: Add AssocMap

---
 src/verilog/Verilog.v | 64 ++++++++++++++++++++-------------------------------
 1 file changed, 25 insertions(+), 39 deletions(-)

(limited to 'src/verilog/Verilog.v')

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. *)
 
-- 
cgit 


From 43f766ea8aff8309d94173cc1e2670eb8ddce68f Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 20 May 2020 10:51:14 +0100
Subject: Switch position of empty rule

---
 src/verilog/Verilog.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/verilog/Verilog.v')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index c0bce25..c1e0a79 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -244,14 +244,14 @@ Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop :=
   | erun_Vlit :
       forall fext assoc v,
       expr_runp fext assoc (Vlit v) v
-  | erun_Vvar_empty :
-      forall fext assoc r sz,
-      assoc!r = None ->
-      expr_runp fext assoc (Vvar r) (ZToValue sz 0)
   | erun_Vvar :
       forall fext assoc v r,
       assoc!r = Some v ->
       expr_runp fext assoc (Vvar r) v
+  | erun_Vvar_empty :
+      forall fext assoc r sz,
+      assoc!r = None ->
+      expr_runp fext assoc (Vvar r) (ZToValue sz 0)
   | erun_Vinputvar :
       forall fext assoc r v,
       fext!r = Some v ->
-- 
cgit 


From e06577fe952a3c268520b280b020bb2bff252529 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 29 May 2020 18:14:59 +0100
Subject: Fix compilation moving to PTree

---
 src/verilog/Verilog.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'src/verilog/Verilog.v')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index c1e0a79..ce7ddd9 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -171,13 +171,13 @@ Definition posToLit (p : positive) : expr :=
 Coercion Vlit : value >-> expr.
 Coercion Vvar : reg >-> expr.
 
-Definition fext := PositiveMap.t value.
+Definition fext := AssocMap.t value.
 Definition fextclk := nat -> fext.
 
 (** ** State
 
 The [state] contains the following items:
-
+n
 - Current [module] that is being worked on, so that the state variable can be
 retrieved and set appropriately.
 - Current [module_item] which is being worked on.
@@ -300,7 +300,7 @@ Definition handle_def {A : Type} (a : A) (val : option A)
 Local Open Scope error_monad_scope.
 
 Definition access_fext (f : fext) (r : reg) : res value :=
-  match PositiveMap.find r f with
+  match AssocMap.get r f with
   | Some v => OK v
   | _ => OK (ZToValue 1 0)
   end.
@@ -452,7 +452,7 @@ Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop :=
     forall lhs name rhs rhsval assoc assoc' nbassoc f,
     assign_name lhs = OK name ->
     expr_runp f assoc rhs rhsval ->
-    assoc' = (PositiveMap.add name rhsval assoc) ->
+    assoc' = (AssocMap.set name rhsval assoc) ->
     stmnt_runp f (mkassociations assoc nbassoc)
                  (Vblock lhs rhs)
                  (mkassociations assoc' nbassoc)
@@ -460,7 +460,7 @@ Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop :=
     forall lhs name rhs rhsval assoc nbassoc nbassoc' f,
     assign_name lhs = OK name ->
     expr_runp f assoc rhs rhsval ->
-    nbassoc' = (PositiveMap.add name rhsval nbassoc) ->
+    nbassoc' = (AssocMap.set name rhsval nbassoc) ->
     stmnt_runp f (mkassociations assoc nbassoc)
                  (Vnonblock lhs rhs)
                  (mkassociations assoc nbassoc').
@@ -534,8 +534,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.add (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap)
-           | _ => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap)
+           | S O => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap)
+           | _ => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap)
            end.
 
 (*Definition module_run (n : nat) (m : module) : res assocmap :=
-- 
cgit