Merge branch 'develop' into arrays-proof

5 files changed, 756 insertions, 177 deletions

diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
new file mode 100644
index 0000000..88b13a6
--- /dev/null
+++ b/src/verilog/AssocMap.v
@@ -0,0 +1,210 @@
+(*
+ * 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 compcert Require Import Maps.
+
+Definition reg := positive.
+
+Module AssocMap := Maps.PTree.
+
+Module AssocMapExt.
+  Import AssocMap.
+
+  Hint Resolve elements_correct elements_complete
+       elements_keys_norepet : assocmap.
+  Hint Resolve gso gss : assocmap.
+
+  Section Operations.
+
+    Variable A : Type.
+
+    Definition get_default (a : A) (k : reg) (m : t A) : A :=
+      match get k m with
+      | None => a
+      | Some v => v
+      end.
+
+    Fixpoint merge (m1 m2 : t A) : t A :=
+      match m1, m2 with
+      | Node l1 (Some a) r1, Node l2 _ r2 => Node (merge l1 l2) (Some a) (merge r1 r2)
+      | Node l1 None r1, Node l2 o r2 => Node (merge l1 l2) o (merge r1 r2)
+      | Leaf, _ => m2
+      | _, _ => m1
+      end.
+
+    Lemma merge_base_1 :
+      forall am,
+      merge (empty A) am = am.
+    Proof. auto. Qed.
+    Hint Resolve merge_base_1 : assocmap.
+
+    Lemma merge_base_2 :
+      forall am,
+      merge am (empty A) = am.
+    Proof.
+      unfold merge.
+      destruct am; trivial.
+      destruct o; trivial.
+    Qed.
+    Hint Resolve merge_base_2 : assocmap.
+
+    Lemma merge_add_assoc :
+      forall r am am' v,
+      merge (set r v am) am' = set r v (merge am am').
+    Proof.
+      induction r; intros; destruct am; destruct am'; try (destruct o); simpl;
+        try rewrite IHr; try reflexivity.
+    Qed.
+    Hint Resolve merge_add_assoc : assocmap.
+
+    Lemma merge_correct_1 :
+      forall am bm k v,
+      get k am = Some v ->
+      get k (merge am bm) = Some v.
+    Proof.
+      induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
+        try rewrite gempty in H; try discriminate; try assumption; auto.
+    Qed.
+    Hint Resolve merge_correct_1 : assocmap.
+
+    Lemma merge_correct_2 :
+      forall am bm k v,
+      get k am = None ->
+      get k bm = Some v ->
+      get k (merge am bm) = Some v.
+    Proof.
+      induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
+        try rewrite gempty in H; try discriminate; try assumption; auto.
+    Qed.
+    Hint Resolve merge_correct_2 : assocmap.
+
+    Definition merge_fold (am bm : t A) : t A :=
+      fold_right (fun p a => set (fst p) (snd p) a) bm (elements am).
+
+    Lemma add_assoc :
+      forall (k : elt) (v : A) l bm,
+      List.In (k, v) l ->
+      list_norepet (List.map fst l) ->
+      @get A k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v.
+    Proof.
+      induction l; intros.
+      - contradiction.
+      - destruct a as [k' v'].
+        destruct (peq k k').
+        + inversion H. inversion H1. inversion H0. subst.
+          simpl. auto with assocmap.
+
+          inversion H0; subst. apply in_map with (f:=fst) in H1. contradiction.
+
+        + inversion H. inversion H1. inversion H0. subst. simpl. rewrite gso; try assumption.
+          apply IHl. contradiction. contradiction.
+          simpl. rewrite gso; try assumption. apply IHl. assumption. inversion H0. subst. assumption.
+    Qed.
+    Hint Resolve add_assoc : assocmap.
+
+    Lemma not_in_assoc :
+      forall k v l bm,
+      ~ List.In k (List.map (@fst elt A) l) ->
+      @get A k bm = Some v ->
+      get k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v.
+    Proof.
+      induction l; intros.
+      - assumption.
+      - destruct a as [k' v'].
+        destruct (peq k k'); subst;
+          simpl in *; apply Decidable.not_or in H; destruct H. contradiction.
+        rewrite AssocMap.gso; auto.
+    Qed.
+    Hint Resolve not_in_assoc : assocmap.
+
+    Lemma elements_iff :
+      forall am k,
+      (exists v, get k am = Some v) <->
+      List.In k (List.map (@fst _ A) (elements am)).
+    Proof.
+      split; intros.
+      destruct H. apply elements_correct in H. apply in_map with (f := fst) in H. apply H.
+      apply list_in_map_inv in H. destruct H. destruct H. subst.
+      exists (snd x). apply elements_complete. assert (x = (fst x, snd x)) by apply surjective_pairing.
+      rewrite H in H0; assumption.
+    Qed.
+    Hint Resolve elements_iff : assocmap.
+
+    Lemma elements_correct' :
+      forall am k,
+      ~ (exists v, get k am = Some v) <->
+      ~ List.In k (List.map (@fst _ A) (elements am)).
+    Proof. auto using not_iff_compat with assocmap. Qed.
+    Hint Resolve elements_correct' : assocmap.
+
+    Lemma elements_correct_none :
+      forall am k,
+      get k am = None ->
+      ~ List.In k (List.map (@fst _ A) (elements am)).
+    Proof.
+      intros. apply elements_correct'. unfold not. intros.
+      destruct H0. rewrite H in H0. discriminate.
+    Qed.
+    Hint Resolve elements_correct_none : assocmap.
+
+    Lemma merge_fold_add :
+      forall k v am bm,
+      am ! k = Some v ->
+      (merge_fold am bm) ! k = Some v.
+    Proof. unfold merge_fold; auto with assocmap. Qed.
+    Hint Resolve merge_fold_add : assocmap.
+
+    Lemma merge_fold_not_in :
+      forall k v am bm,
+      get k am = None ->
+      get k bm = Some v ->
+      get k (merge_fold am bm) = Some v.
+    Proof. intros. apply not_in_assoc; auto with assocmap. Qed.
+    Hint Resolve merge_fold_not_in : assocmap.
+
+    Lemma merge_fold_base :
+      forall am,
+      merge_fold (empty A) am = am.
+    Proof. auto. Qed.
+    Hint Resolve merge_fold_base : assocmap.
+
+  End Operations.
+
+End AssocMapExt.
+Import AssocMapExt.
+
+Definition assocmap := AssocMap.t value.
+
+Definition find_assocmap (n : nat) : reg -> assocmap -> value :=
+  get_default value (ZToValue n 0).
+
+Definition empty_assocmap : assocmap := AssocMap.empty value.
+
+Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value.
+
+Ltac unfold_merge :=
+  unfold merge_assocmap; try (repeat (rewrite merge_add_assoc));
+  rewrite AssocMapExt.merge_base_1.
+
+Module AssocMapNotation.
+  Notation "a ! b" := (AssocMap.get 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 1d156ad..a21064c 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -16,89 +16,83 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(** The purpose of the hardware transfer language (HTL) is to create a more
-  * hardware-like layout that is still similar to the register transfer language
-  * (RTL) that it came from. The main change is that function calls become
-  * module instantiations and that we now describe a state machine instead of a
-  * control-flow graph.
-  *)
-
-From coqup.common Require Import Coquplib.
-
+From Coq Require Import FSets.FMapPositive.
+From coqup Require Import Coquplib Value AssocMap.
+From coqup Require Verilog.
+From compcert Require Events Globalenvs Smallstep Integers.
 From compcert Require Import Maps.
-From compcert Require Op AST Memory Registers.
-
-Definition node := positive.
 
-Definition reg := Registers.reg.
-
-Definition ident := AST.ident.
-
-Inductive instruction : Type :=
-| Hnop : node -> instruction
-| Hnonblock : Op.operation -> list reg -> reg -> node -> instruction
-  (** [Hnonblock op args res next] Defines a nonblocking assignment to a
-      register, using the operation defined in Op.v. *)
-| Hload : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction
-| Hstore : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction
-| Hinst : AST.signature -> ident -> reg -> node -> instruction
-  (** [Hinst sig fun args rst strt end res next] Defines the start of a
-      module instantiation, meaning the function will run until the result is
-      returned. *)
-| Htailcall : AST.signature -> ident -> list reg -> instruction
-| Hcond : Op.condition -> list reg -> node -> node -> instruction
-| Hjumptable : reg -> list node -> instruction
-| Hfinish : option reg -> instruction.
-
-Record inst : Type :=
-  mkinst {
-    inst_moddecl : ident;
-    inst_args : list reg
-  }.
+Import HexNotationValue.
 
-Definition code : Type := PTree.t instruction.
+(** The purpose of the hardware transfer language (HTL) is to create a more
+hardware-like layout that is still similar to the register transfer language
+(RTL) that it came from. The main change is that function calls become module
+instantiations and that we now describe a state machine instead of a
+control-flow graph. *)
 
-Definition instances : Type := PTree.t inst.
+Definition reg := positive.
+Definition node := positive.
 
-Definition empty_instances : instances := PTree.empty inst.
+Definition datapath := PTree.t Verilog.stmnt.
+Definition controllogic := PTree.t Verilog.stmnt.
 
-(** Function declaration for VTL also contain a construction which describes the
-    functions that are called in the current function. This information is used
-    to print out *)
-Record module : Type :=
+Record module: Type :=
   mkmodule {
-    mod_sig : AST.signature;
     mod_params : list reg;
-    mod_stacksize : Z;
-    mod_code : code;
-    mod_insts : instances;
-    mod_entrypoint : node
+    mod_datapath : datapath;
+    mod_controllogic : controllogic;
+    mod_entrypoint : node;
+    mod_st : reg;
+    mod_finish : reg;
+    mod_return : reg
   }.
 
-Definition moddecl := AST.fundef module.
-
-Definition design := AST.program moddecl unit.
-
-Definition modsig (md : moddecl) :=
-  match md with
-  | AST.Internal m => mod_sig m
-  | AST.External ef => AST.ef_sig ef
-  end.
-
-(** Describes various transformations that can be applied to HTL. This applies
-    the transformation to each instruction in the function and returns the new
-    function with the modified instructions. *)
-Section TRANSF.
-
-  Variable transf_instr : node -> instruction -> instruction.
-
-  Definition transf_module (m : module) : module :=
-    mkmodule
-      m.(mod_sig)
-      m.(mod_params)
-      m.(mod_stacksize)
-      (PTree.map transf_instr m.(mod_code))
-      m.(mod_insts)
-      m.(mod_entrypoint).
-
-End TRANSF.
+(** * Operational Semantics *)
+
+Definition genv := Globalenvs.Genv.t unit unit.
+Definition genv_empty := Globalenvs.Genv.empty_genv unit unit nil.
+
+Inductive state : Type :=
+| State :
+    forall (m : module)
+           (st : node)
+           (assoc : assocmap),
+  state
+| Returnstate : forall v : value, state.
+
+Inductive step : genv -> state -> Events.trace -> state -> Prop :=
+| step_module :
+    forall g t m st ctrl data assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f stval pstval,
+      m.(mod_controllogic)!st = Some ctrl ->
+      m.(mod_datapath)!st = Some data ->
+      Verilog.stmnt_runp f
+        (Verilog.mkassociations assoc0 empty_assocmap)
+        ctrl
+        (Verilog.mkassociations assoc1 nbassoc0) ->
+      Verilog.stmnt_runp f
+        (Verilog.mkassociations assoc1 nbassoc0)
+        data
+        (Verilog.mkassociations assoc2 nbassoc1) ->
+      assoc3 = merge_assocmap nbassoc1 assoc2 ->
+      assoc3!(m.(mod_st)) = Some stval ->
+      valueToPos stval = pstval ->
+      step g (State m st assoc0) t (State m pstval assoc3)
+| step_finish :
+    forall g t m st assoc retval,
+    assoc!(m.(mod_finish)) = Some (1'h"1") ->
+    assoc!(m.(mod_return)) = Some retval ->
+    step g (State m st assoc) t (Returnstate retval).
+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 empty_assocmap).
+
+Inductive final_state : state -> Integers.int -> Prop :=
+| final_state_intro : forall retval retvali,
+    value_int_eqb retval retvali = true ->
+    final_state (Returnstate retval) retvali.
+
+Definition semantics (m : module) :=
+  Smallstep.Semantics step (initial_state m) final_state genv_empty.
diff --git a/src/verilog/Test.v b/src/verilog/Test.v
new file mode 100644
index 0000000..90c5312
--- /dev/null
+++ b/src/verilog/Test.v
@@ -0,0 +1,99 @@
+(*
+ * 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/Value.v b/src/verilog/Value.v
index fe53dbc..34cb0d2 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq -*-
+(*
  * CoqUp: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
@@ -18,8 +18,9 @@
 
 (* begin hide *)
 From bbv Require Import Word.
-From Coq Require Import ZArith.ZArith.
-From compcert Require Import lib.Integers.
+From bbv Require HexNotation WordScope.
+From Coq Require Import ZArith.ZArith FSets.FMapPositive.
+From compcert Require Import lib.Integers common.Values.
 (* end hide *)
 
 (** * Value
@@ -47,7 +48,7 @@ Definition wordToValue : forall sz : nat, word sz -> value := mkvalue.
 
 Definition valueToWord : forall v : value, word (vsize v) := vword.
 
-Definition valueToNat (v : value) : nat :=
+Definition valueToNat (v :value) : nat :=
   wordToNat (vword v).
 
 Definition natToValue sz (n : nat) : value :=
@@ -59,13 +60,6 @@ Definition valueToN (v : value) : N :=
 Definition NToValue sz (n : N) : value :=
   mkvalue sz (NToWord sz n).
 
-Definition posToValue sz (p : positive) : value :=
-  mkvalue sz (posToWord sz p).
-
-Definition posToValueAuto (p : positive) : value :=
-  let size := Z.to_nat (Z.succ (log_inf p)) in
-  mkvalue size (Word.posToWord size p).
-
 Definition ZToValue (s : nat) (z : Z) : value :=
   mkvalue s (ZToWord s z).
 
@@ -75,9 +69,29 @@ Definition valueToZ (v : value) : Z :=
 Definition uvalueToZ (v : value) : Z :=
   uwordToZ (vword v).
 
+Definition posToValue sz (p : positive) : value :=
+  ZToValue sz (Zpos p).
+
+Definition posToValueAuto (p : positive) : value :=
+  let size := Pos.to_nat (Pos.size p) in
+  ZToValue size (Zpos p).
+
+Definition valueToPos (v : value) : positive :=
+  Z.to_pos (uvalueToZ v).
+
 Definition intToValue (i : Integers.int) : value :=
   ZToValue Int.wordsize (Int.unsigned i).
 
+Definition valueToInt (i : value) : Integers.int :=
+  Int.repr (valueToZ i).
+
+Definition valToValue (v : Values.val) : option value :=
+  match v with
+  | Values.Vint i => Some (intToValue i)
+  | Values.Vundef => Some (ZToValue 32 0%Z)
+  | _ => None
+  end.
+
 (** Convert a [value] to a [bool], so that choices can be made based on the
 result. This is also because comparison operators will give back [value] instead
 of [bool], so if they are in a condition, they will have to be converted before
@@ -91,8 +105,8 @@ Definition boolToValue (sz : nat) (b : bool) : value :=
 
 (** ** Arithmetic operations *)
 
-Lemma unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
-Proof. intros; subst; assumption. Qed.
+Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
+intros; subst; assumption. Defined.
 
 Definition value_eq_size:
   forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }.
@@ -137,6 +151,64 @@ Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value)
   | _ => None
   end.
 
+Lemma eqvalue {sz : nat} (x y : word sz) : x = y <-> mkvalue sz x = mkvalue sz y.
+Proof.
+  split; intros.
+  subst. reflexivity. inversion H. apply existT_wordToZ in H1.
+  apply wordToZ_inj. assumption.
+Qed.
+
+Lemma eqvaluef {sz : nat} (x y : word sz) : x = y -> mkvalue sz x = mkvalue sz y.
+Proof. apply eqvalue. Qed.
+
+Lemma nevalue {sz : nat} (x y : word sz) : x <> y <-> mkvalue sz x <> mkvalue sz y.
+Proof. split; intros; intuition. apply H. apply eqvalue. assumption.
+       apply H. rewrite H0. trivial.
+Qed.
+
+Lemma nevaluef {sz : nat} (x y : word sz) : x <> y -> mkvalue sz x <> mkvalue sz y.
+Proof. apply nevalue. Qed.
+
+(*Definition rewrite_word_size (initsz finalsz : nat) (w : word initsz)
+  : option (word finalsz) :=
+  match Nat.eqb initsz finalsz return option (word finalsz) with
+  | true => Some _
+  | false => None
+  end.*)
+
+Definition valueeq (sz : nat) (x y : word sz) :
+  {mkvalue sz x = mkvalue sz y} + {mkvalue sz x <> mkvalue sz y} :=
+  match weq x y with
+  | left eq => left (eqvaluef x y eq)
+  | right ne => right (nevaluef x y ne)
+  end.
+
+Definition valueeqb (x y : value) : bool :=
+  match value_eq_size x y with
+  | left EQ =>
+    weqb (vword x) (unify_word (vsize x) (vsize y) (vword y) EQ)
+  | right _ => false
+  end.
+
+Definition value_projZ_eqb (v1 v2 : value) : bool := Z.eqb (valueToZ v1) (valueToZ v2).
+
+Theorem value_projZ_eqb_true :
+  forall v1 v2,
+  v1 = v2 -> value_projZ_eqb v1 v2 = true.
+Proof. intros. subst. unfold value_projZ_eqb. apply Z.eqb_eq. trivial. Qed.
+
+Theorem valueeqb_true_iff :
+  forall v1 v2,
+  valueeqb v1 v2 = true <-> v1 = v2.
+Proof.
+  split; intros.
+  unfold valueeqb in H. destruct (value_eq_size v1 v2) eqn:?.
+  - destruct v1, v2. simpl in H.
+Abort.
+
+Definition value_int_eqb (v : value) (i : int) : bool :=
+  Z.eqb (valueToZ v) (Int.unsigned i).
+
 (** Arithmetic operations over [value], interpreting them as signed or unsigned
 depending on the operation.
 
@@ -208,3 +280,48 @@ Definition shift_map (sz : nat) (f : word sz -> nat -> word sz) (w1 w2 : word sz
 
 Definition vshl v1 v2 := map_word2 (fun sz => shift_map sz (@wlshift sz)) v1 v2.
 Definition vshr v1 v2 := map_word2 (fun sz => shift_map sz (@wrshift sz)) v1 v2.
+
+Module HexNotationValue.
+  Export HexNotation.
+  Import WordScope.
+
+  Notation "sz ''h' a" := (NToValue sz (hex a)) (at level 50).
+
+End HexNotationValue.
+
+Inductive val_value_lessdef: val -> value -> Prop :=
+| val_value_lessdef_int:
+    forall i v',
+    Integers.Int.unsigned i = valueToZ v' ->
+    val_value_lessdef (Vint i) v'
+| lessdef_undef: forall v, val_value_lessdef Vundef v.
+
+Lemma valueToZ_ZToValue :
+  forall n z,
+  (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z ->
+  valueToZ (ZToValue (S n) z) = z.
+Proof.
+  unfold valueToZ, ZToValue. simpl.
+  auto using wordToZ_ZToWord.
+Qed.
+
+Lemma uvalueToZ_ZToValue :
+  forall n z,
+  (0 <= z < 2 ^ Z.of_nat n)%Z ->
+  uvalueToZ (ZToValue n z) = z.
+Proof.
+  unfold uvalueToZ, ZToValue. simpl.
+  auto using uwordToZ_ZToWord.
+Qed.
+
+Lemma valueToPos_posToValueAuto :
+  forall p, valueToPos (posToValueAuto p) = p.
+Proof.
+  intros. unfold valueToPos, posToValueAuto.
+  rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z.
+  split. apply Zle_0_pos.
+
+  assert (p < 2 ^ (Pos.size p))%positive. apply Pos.size_gt.
+  inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1.
+  simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.
+Qed.
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index dfb6255..e2b85b2 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>
  *
@@ -27,18 +27,22 @@ 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.
 
-From compcert Require Integers.
-From compcert Require Import Errors.
-
-Notation "a ! b" := (PositiveMap.find b a) (at level 1).
+Import HexNotationValue.
+Import AssocMapNotation.
 
 Definition reg : Type := positive.
 Definition node : Type := positive.
 Definition szreg : Type := reg * nat.
 
-Definition assoclist : Type := PositiveMap.t value.
+Record associations : Type :=
+  mkassociations {
+    assoc_blocking : assocmap;
+    assoc_nonblocking : assocmap
+  }.
 
 (** * Verilog AST
 
@@ -51,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 := assoclist * assoclist.
-
 (** ** Binary Operators
 
 These are the binary operations that can be represented in Verilog. Ideally,
@@ -159,10 +161,10 @@ 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;
-}.
-
+                        }.
 (** Convert a [positive] to an expression directly, setting it to the right
     size. *)
 Definition posToLit (p : positive) : expr :=
@@ -171,15 +173,41 @@ 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.
 
-Inductive state: Type :=
-  State:
-    forall (assoc : assoclist)
-           (nbassoc : assoclist)
+(** ** 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.
+- 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 :=
+| State:
+    forall (m : module)
+           (assoc : assocmap)
+           (nbassoc : assocmap)
            (f : fextclk)
-           (cycle : positive),
+           (cycle : nat)
+           (stvar : value),
+    state
+| Finishstate:
+    forall v : value,
     state.
 
 Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value :=
@@ -214,40 +242,48 @@ Definition unop_run (op : unop) : value -> value :=
   | Vnot => vbitneg
   end.
 
-Inductive expr_runp : state -> expr -> value -> Prop :=
+Inductive expr_runp : fext -> assocmap -> 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 (State assoc na f c) (Vvar r) 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 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 resv,
+      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)
+      resv = oper lv rv EQ ->
+      expr_runp fext assoc (Vbinop op l r) resv
   | erun_Vunop :
-      forall s u vu op oper,
-      expr_runp s u vu ->
+      forall fext assoc u vu op oper resv,
+      expr_runp fext assoc u vu ->
       oper = unop_run op ->
-      expr_runp s (Vunop op u) (oper vu)
+      resv = oper vu ->
+      expr_runp fext assoc (Vunop op u) resv
   | 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.
+Hint Constructors expr_runp : verilog.
 
 Definition handle_opt {A : Type} (err : errmsg) (val : option A)
   : res A :=
@@ -265,22 +301,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
-  | State _ _ 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 AssocMap.get 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 : assocmap) (e : expr)
          {struct e} : res value :=
   match e with
   | Vlit v => OK v
   | Vvar r => match s with
-              | State assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r
+              | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r
+              | _ => Error (msg "Verilog: Wrong state")
               end
   | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled")
   | Vinputvar r => access_fext s r
@@ -299,7 +333,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. *)
@@ -310,6 +344,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
@@ -348,35 +391,85 @@ 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 =>
+      | State m 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 (State m (PositiveMap.add name rhse assoc) nbassoc f c)
+      | _ => Error (msg "Verilog: Wrong state")
       end
     | Vnonblock lhs rhs =>
       match s with
-      | State assoc nbassoc f c =>
+      | State m 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 (State m assoc (PositiveMap.add name rhse nbassoc) f c)
+      | _ => Error (msg "Verilog: Wrong state")
       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.
-
-Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
+  stmnt_run' (stmnt_height st) s st. *)
+
+Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop :=
+| stmnt_runp_Vskip:
+    forall f a, stmnt_runp f a Vskip a
+| stmnt_runp_Vseq:
+    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 as0 as1 f c vc stt stf,
+    expr_runp f as0.(assoc_blocking) c vc ->
+    valueToBool vc = true ->
+    stmnt_runp f as0 stt as1 ->
+    stmnt_runp f as0 (Vcond c stt stf) as1
+| stmnt_runp_Vcond_false:
+    forall as0 as1 f c vc stt stf,
+    expr_runp f as0.(assoc_blocking) c vc ->
+    valueToBool vc = false ->
+    stmnt_runp f as0 stf as1 ->
+    stmnt_runp f as0 (Vcond c stt stf) as1
+| stmnt_runp_Vcase_nomatch:
+    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 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 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 f as0 sc as1 ->
+    stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1
+| stmnt_runp_Vcase_default:
+    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 assoc assoc' nbassoc f,
+    assign_name lhs = OK name ->
+    expr_runp f assoc rhs rhsval ->
+    assoc' = (AssocMap.set name rhsval assoc) ->
+    stmnt_runp f (mkassociations assoc nbassoc)
+                 (Vblock lhs rhs)
+                 (mkassociations assoc' nbassoc)
+| stmnt_runp_Vnonblock:
+    forall lhs name rhs rhsval assoc nbassoc nbassoc' f,
+    assign_name lhs = OK name ->
+    expr_runp f assoc rhs rhsval ->
+    nbassoc' = (AssocMap.set name rhsval nbassoc) ->
+    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 :=
   let run := fun st ls =>
               do s' <- stmnt_run s st;
               mi_step s' ls
@@ -388,41 +481,69 @@ Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
   | (Vdecl _ _)::ls => mi_step s ls
   | (Vdeclarr _ _ _)::ls => mi_step s ls
   | nil => OK s
-  end.
-
-Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist :=
-  PositiveMap.add r v assoc.
-
-Definition merge_assoclist (nbassoc assoc : assoclist) : assoclist :=
-  PositiveMap.fold add_assoclist nbassoc assoc.
-
-Definition empty_assoclist : assoclist := PositiveMap.empty value.
-
-Definition mi_step_commit (s : state) (m : list module_item) : res state :=
+  end.*)
+
+Inductive mi_stepp : fext -> associations -> module_item -> associations -> Prop :=
+| mi_stepp_Valways :
+    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 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 f s0 st s1 c,
+    stmnt_runp f s0 st s1 ->
+    mi_stepp f s0 (Valways_comb c st) s1
+| mi_stepp_Vdecl :
+    forall f s lhs rhs,
+    mi_stepp f s (Vdecl lhs rhs) s.
+Hint Constructors mi_stepp : verilog.
+
+Inductive mis_stepp : fext -> associations -> list module_item -> associations -> Prop :=
+| mis_stepp_Cons :
+    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 f s,
+    mis_stepp f s nil s.
+Hint Constructors mis_stepp : verilog.
+
+(*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 (State m assoc nbassoc f c) =>
+    OK (State m (merge_assocmap nbassoc assoc) empty_assocmap 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 : 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_assoclist 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
   | O => OK assoc
-  end.
+  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.
+(** 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 => (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 :=
+  mi_run (initial_fextclk m) empty_assocmap (mod_body m) n.*)
 
 Local Close Scope error_monad_scope.
 
@@ -463,4 +584,42 @@ Proof.
       assumption.
 Qed.
 
+ *)
+
+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_assocmap)
+              m.(mod_body)
+              (mkassociations assoc1 nbassoc) ->
+    assoc2 = merge_assocmap nbassoc assoc1 ->
+    Some stvar' = assoc2!(fst m.(mod_state)) ->
+    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_assocmap f cycle stvar)
+         (Finishstate result).
+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).
 *)