Add RTLBlock intermediate language

9 files changed, 0 insertions, 2674 deletions

diff --git a/src/verilog/Array.v b/src/verilog/Array.v
deleted file mode 100644
index fe0f6b2..0000000
--- a/src/verilog/Array.v
+++ /dev/null
@@ -1,337 +0,0 @@
-Set Implicit Arguments.
-
-Require Import Lia.
-Require Import Vericertlib.
-From Coq Require Import Lists.List Datatypes.
-
-Import ListNotations.
-
-Local Open Scope nat_scope.
-
-Record Array (A : Type) : Type :=
-  mk_array
-    { arr_contents : list A
-    ; arr_length : nat
-    ; arr_wf : length arr_contents = arr_length
-    }.
-
-Definition make_array {A : Type} (l : list A) : Array A :=
-  @mk_array A l (length l) eq_refl.
-
-Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) {struct l} : list A :=
-  match i, l with
-  | _, nil => nil
-  | S n, h :: t => h :: list_set n x t
-  | O, h :: t => x :: t
-  end.
-
-Lemma list_set_spec1 {A : Type} :
-  forall l i (x : A),
-    i < length l -> nth_error (list_set i x l) i = Some x.
-Proof.
-  induction l; intros; destruct i; crush; firstorder.
-Qed.
-Hint Resolve list_set_spec1 : array.
-
-Lemma list_set_spec2 {A : Type} :
-  forall l i (x : A) d,
-    i < length l -> nth i (list_set i x l) d = x.
-Proof.
-  induction l; intros; destruct i; crush; firstorder.
-Qed.
-Hint Resolve list_set_spec2 : array.
-
-Lemma list_set_spec3 {A : Type} :
-  forall l i1 i2 (x : A),
-    i1 <> i2 ->
-    nth_error (list_set i1 x l) i2 = nth_error l i2.
-Proof.
-  induction l; intros; destruct i1; destruct i2; crush; firstorder.
-Qed.
-Hint Resolve list_set_spec3 : array.
-
-Lemma array_set_wf {A : Type} :
-  forall l ln i (x : A),
-    length l = ln -> length (list_set i x l) = ln.
-Proof.
-  induction l; intros; destruct i; auto.
-
-  invert H; crush; auto.
-Qed.
-
-Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) :=
-  let l := a.(arr_contents) in
-  let ln := a.(arr_length) in
-  let WF := a.(arr_wf) in
-  @mk_array A (list_set i x l) ln (@array_set_wf A l ln i x WF).
-
-Lemma array_set_spec1 {A : Type} :
-  forall a i (x : A),
-    i < a.(arr_length) -> nth_error ((array_set i x a).(arr_contents)) i = Some x.
-Proof.
-  intros.
-
-  rewrite <- a.(arr_wf) in H.
-  unfold array_set. crush.
-  eauto with array.
-Qed.
-Hint Resolve array_set_spec1 : array.
-
-Lemma array_set_spec2 {A : Type} :
-  forall a i (x : A) d,
-    i < a.(arr_length) -> nth i ((array_set i x a).(arr_contents)) d = x.
-Proof.
-  intros.
-
-  rewrite <- a.(arr_wf) in H.
-  unfold array_set. crush.
-  eauto with array.
-Qed.
-Hint Resolve array_set_spec2 : array.
-
-Lemma array_set_len {A : Type} :
-  forall a i (x : A),
-    a.(arr_length) = (array_set i x a).(arr_length).
-Proof.
-  unfold array_set. crush.
-Qed.
-
-Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A :=
-  nth_error a.(arr_contents) i.
-
-Lemma array_get_error_equal {A : Type} :
-  forall (a b : Array A) i,
-    a.(arr_contents) = b.(arr_contents) ->
-    array_get_error i a = array_get_error i b.
-Proof.
-  unfold array_get_error. crush.
-Qed.
-
-Lemma array_get_error_bound {A : Type} :
-  forall (a : Array A) i,
-    i < a.(arr_length) -> exists x, array_get_error i a = Some x.
-Proof.
-  intros.
-
-  rewrite <- a.(arr_wf) in H.
-  assert (~ length (arr_contents a) <= i) by lia.
-
-  pose proof (nth_error_None a.(arr_contents) i).
-  apply not_iff_compat in H1.
-  apply <- H1 in H0.
-
-  destruct (nth_error (arr_contents a) i) eqn:EQ; try contradiction; eauto.
-Qed.
-
-Lemma array_get_error_set_bound {A : Type} :
-  forall (a : Array A) i x,
-    i < a.(arr_length) -> array_get_error i (array_set i x a) = Some x.
-Proof.
-  intros.
-
-  unfold array_get_error.
-  eauto with array.
-Qed.
-
-Lemma array_gso {A : Type} :
-  forall (a : Array A) i1 i2 x,
-    i1 <> i2 ->
-    array_get_error i2 (array_set i1 x a) = array_get_error i2 a.
-Proof.
-  intros.
-
-  unfold array_get_error.
-  unfold array_set.
-  crush.
-  eauto with array.
-Qed.
-
-Definition array_get {A : Type} (i : nat) (x : A) (a : Array A) : A :=
-  nth i a.(arr_contents) x.
-
-Lemma array_get_set_bound {A : Type} :
-  forall (a : Array A) i x d,
-    i < a.(arr_length) -> array_get i d (array_set i x a) = x.
-Proof.
-  intros.
-
-  unfold array_get.
-  eauto with array.
-Qed.
-
-Lemma array_get_get_error {A : Type} :
-  forall (a : Array A) i x d,
-    array_get_error i a = Some x ->
-    array_get i d a = x.
-Proof.
-  intros.
-  unfold array_get.
-  unfold array_get_error in H.
-  auto using nth_error_nth.
-Qed.
-
-(** Tail recursive version of standard library function. *)
-Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A :=
-  match n with
-  | O => acc
-  | S n => list_repeat' (a::acc) a n
-  end.
-
-Lemma list_repeat'_len {A : Type} : forall (a : A) n l,
-    length (list_repeat' l a n) = (n + Datatypes.length l)%nat.
-Proof.
-  induction n; intros; crush; try reflexivity.
-
-  specialize (IHn (a :: l)).
-  rewrite IHn.
-  crush.
-Qed.
-
-Lemma list_repeat'_app {A : Type} : forall (a : A) n l,
-    list_repeat' l a n = list_repeat' [] a n ++ l.
-Proof.
-  induction n; intros; crush; try reflexivity.
-
-  pose proof IHn.
-  specialize (H (a :: l)).
-  rewrite H. clear H.
-  specialize (IHn (a :: nil)).
-  rewrite IHn. clear IHn.
-  remember (list_repeat' [] a n) as l0.
-
-  rewrite <- app_assoc.
-  f_equal.
-Qed.
-
-Lemma list_repeat'_head_tail {A : Type} : forall n (a : A),
-  a :: list_repeat' [] a n = list_repeat' [] a n ++ [a].
-Proof.
-  induction n; intros; crush; try reflexivity.
-  rewrite list_repeat'_app.
-
-  replace (a :: list_repeat' [] a n ++ [a]) with (list_repeat' [] a n ++ [a] ++ [a]).
-  2: { rewrite app_comm_cons. rewrite IHn; auto.
-       rewrite app_assoc. reflexivity. }
-  rewrite app_assoc. reflexivity.
-Qed.
-
-Lemma list_repeat'_cons {A : Type} : forall (a : A) n,
-    list_repeat' [a] a n = a :: list_repeat' [] a n.
-Proof.
-  intros.
-
-  rewrite list_repeat'_head_tail; auto.
-  apply list_repeat'_app.
-Qed.
-
-Definition list_repeat {A : Type} : A -> nat -> list A := list_repeat' nil.
-
-Lemma list_repeat_len {A : Type} : forall n (a : A), length (list_repeat a n) = n.
-Proof.
-  intros.
-  unfold list_repeat.
-  rewrite list_repeat'_len.
-  crush.
-Qed.
-
-Lemma dec_list_repeat_spec {A : Type} : forall n (a : A) a',
-    (forall x x' : A, {x' = x} + {~ x' = x}) ->
-    In a' (list_repeat a n) -> a' = a.
-Proof.
-  induction n; intros; crush.
-
-  unfold list_repeat in *.
-  crush.
-
-  rewrite list_repeat'_app in H.
-  pose proof (X a a').
-  destruct H0; auto.
-
-  (* This is actually a degenerate case, not an unprovable goal. *)
-  pose proof (in_app_or (list_repeat' [] a n) ([a])).
-  apply H0 in H. invert H.
-
-  - eapply IHn in X; eassumption.
-  - invert H1; contradiction.
-Qed.
-
-Lemma list_repeat_head_tail {A : Type} : forall n (a : A),
-    a :: list_repeat a n = list_repeat a n ++ [a].
-Proof.
-  unfold list_repeat. apply list_repeat'_head_tail.
-Qed.
-
-Lemma list_repeat_cons {A : Type} : forall n (a : A),
-    list_repeat a (S n) = a :: list_repeat a n.
-Proof.
-  intros.
-
-  unfold list_repeat.
-  apply list_repeat'_cons.
-Qed.
-
-Lemma list_repeat_lookup {A : Type} :
-  forall n i (a : A),
-    i < n ->
-    nth_error (list_repeat a n) i = Some a.
-Proof.
-  induction n; intros.
-
-  destruct i; crush.
-
-  rewrite list_repeat_cons.
-  destruct i; crush; firstorder.
-Qed.
-
-Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n).
-
-Lemma arr_repeat_length {A : Type} : forall n (a : A), arr_length (arr_repeat a n) = n.
-Proof.
-  unfold list_repeat. crush. apply list_repeat_len.
-Qed.
-
-Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C :=
-  match x, y with
-  | a :: t, b :: t' => f a b :: list_combine f t t'
-  | _, _ => nil
-  end.
-
-Lemma list_combine_length {A B C : Type} (f : A -> B -> C) : forall (x : list A) (y : list B),
-    length (list_combine f x y) = min (length x) (length y).
-Proof.
-  induction x; intros; crush.
-
-  destruct y; crush; auto.
-Qed.
-
-Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C :=
-  make_array (list_combine f x.(arr_contents) y.(arr_contents)).
-
-Lemma combine_length {A B C: Type} : forall x y (f : A -> B -> C),
-    x.(arr_length) = y.(arr_length) -> arr_length (combine f x y) = x.(arr_length).
-Proof.
-  intros.
-
-  unfold combine.
-  unfold make_array.
-  crush.
-
-  rewrite <- (arr_wf x) in *.
-  rewrite <- (arr_wf y) in *.
-
-  destruct (arr_contents x); destruct (arr_contents y); crush.
-  rewrite list_combine_length.
-  destruct (Min.min_dec (length l) (length l0)); congruence.
-Qed.
-
-Ltac array :=
-  try match goal with
-      | [ |- context[arr_length (combine _ _ _)] ] =>
-        rewrite combine_length
-      | [ |- context[length (list_repeat _ _)] ] =>
-        rewrite list_repeat_len
-      | |- context[array_get_error _ (arr_repeat ?x _) = Some ?x] =>
-        unfold array_get_error, arr_repeat
-      | |- context[nth_error (list_repeat ?x _) _ = Some ?x] =>
-        apply list_repeat_lookup
-      end.
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
deleted file mode 100644
index 8d8788a..0000000
--- a/src/verilog/AssocMap.v
+++ /dev/null
@@ -1,217 +0,0 @@
-(*
- * Vericert: 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 vericert Require Import Vericertlib ValueInt.
-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 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.
-
-Declare Scope assocmap.
-Notation "a ! b" := (AssocMap.get b a) (at level 1) : assocmap.
-Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1) : assocmap.
-Notation "a # b" := (find_assocmap 32 b a) (at level 1) : assocmap.
-Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1) : assocmap.
-Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) : assocmap.
-
-Local Open Scope assocmap.
-Lemma find_get_assocmap :
-  forall assoc r v,
-  assoc ! r = Some v ->
-  assoc # r = v.
-Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
deleted file mode 100644
index 620ef14..0000000
--- a/src/verilog/HTL.v
+++ /dev/null
@@ -1,171 +0,0 @@
-(*
- * Vericert: 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 Coq Require Import FSets.FMapPositive.
-From vericert Require Import Vericertlib ValueInt AssocMap Array.
-From vericert Require Verilog.
-From compcert Require Events Globalenvs Smallstep Integers Values.
-From compcert Require Import Maps.
-
-(** 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. *)
-
-Local Open Scope assocmap.
-
-Definition reg := positive.
-Definition node := positive.
-
-Definition datapath := PTree.t Verilog.stmnt.
-Definition controllogic := PTree.t Verilog.stmnt.
-
-Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
-  forall p0 : positive,
-    In p0 (map fst (Maps.PTree.elements m)) ->
-    Z.pos p0 <= Integers.Int.max_unsigned.
-
-Record module: Type :=
-  mkmodule {
-    mod_params : list reg;
-    mod_datapath : datapath;
-    mod_controllogic : controllogic;
-    mod_entrypoint : node;
-    mod_st : reg;
-    mod_stk : reg;
-    mod_stk_len : nat;
-    mod_finish : reg;
-    mod_return : reg;
-    mod_start : reg;
-    mod_reset : reg;
-    mod_clk : reg;
-    mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl);
-    mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl);
-    mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath);
-  }.
-
-Definition fundef := AST.fundef module.
-
-Definition program := AST.program fundef unit.
-
-Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
-  match rl, vl with
-  | r :: rl', v :: vl' => AssocMap.set r v (init_regs vl' rl')
-  | _, _ => empty_assocmap
-  end.
-
-Definition empty_stack (m : module) : Verilog.assocmap_arr :=
-  (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)).
-
-(** * Operational Semantics *)
-
-Definition genv := Globalenvs.Genv.t fundef unit.
-
-Inductive stackframe : Type :=
-  Stackframe :
-    forall  (res : reg)
-            (m : module)
-            (pc : node)
-            (reg_assoc : Verilog.assocmap_reg)
-            (arr_assoc : Verilog.assocmap_arr),
-      stackframe.
-
-Inductive state : Type :=
-| State :
-    forall (stack : list stackframe)
-           (m : module)
-           (st : node)
-           (reg_assoc : Verilog.assocmap_reg)
-           (arr_assoc : Verilog.assocmap_arr), state
-| Returnstate :
-    forall (res : list stackframe)
-           (v : value), state
-| Callstate :
-    forall (stack : list stackframe)
-           (m : module)
-           (args : list value), state.
-
-Inductive step : genv -> state -> Events.trace -> state -> Prop :=
-| step_module :
-    forall g m st sf ctrl data
-      asr asa
-      basr1 basa1 nasr1 nasa1
-      basr2 basa2 nasr2 nasa2
-      asr' asa'
-      f pstval,
-      asr!(mod_reset m) = Some (ZToValue 0) ->
-      asr!(mod_finish m) = Some (ZToValue 0) ->
-      asr!(m.(mod_st)) = Some (posToValue st) ->
-      m.(mod_controllogic)!st = Some ctrl ->
-      m.(mod_datapath)!st = Some data ->
-      Verilog.stmnt_runp f
-        (Verilog.mkassociations asr empty_assocmap)
-        (Verilog.mkassociations asa (empty_stack m))
-        ctrl
-        (Verilog.mkassociations basr1 nasr1)
-        (Verilog.mkassociations basa1 nasa1) ->
-      basr1!(m.(mod_st)) = Some (posToValue st) ->
-      Verilog.stmnt_runp f
-        (Verilog.mkassociations basr1 nasr1)
-        (Verilog.mkassociations basa1 nasa1)
-        data
-        (Verilog.mkassociations basr2 nasr2)
-        (Verilog.mkassociations basa2 nasa2) ->
-      asr' = Verilog.merge_regs nasr2 basr2 ->
-      asa' = Verilog.merge_arrs nasa2 basa2 ->
-      asr'!(m.(mod_st)) = Some (posToValue pstval) ->
-      Z.pos pstval <= Integers.Int.max_unsigned ->
-      step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
-| step_finish :
-    forall g m st asr asa retval sf,
-    asr!(m.(mod_finish)) = Some (ZToValue 1) ->
-    asr!(m.(mod_return)) = Some retval ->
-    step g (State sf m st asr asa) Events.E0 (Returnstate sf retval)
-| step_call :
-    forall g m args res,
-      step g (Callstate res m args) Events.E0
-           (State res m m.(mod_entrypoint)
-             (AssocMap.set (mod_reset m) (ZToValue 0)
-              (AssocMap.set (mod_finish m) (ZToValue 0)
-               (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint))
-                (init_regs args m.(mod_params)))))
-             (empty_stack m))
-| step_return :
-    forall g m asr asa i r sf pc mst,
-      mst = mod_st m ->
-      step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
-           (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa).
-Hint Constructors step : htl.
-
-Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b m0 m,
-      let ge := Globalenvs.Genv.globalenv p in
-      Globalenvs.Genv.init_mem p = Some m0 ->
-      Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
-      Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) ->
-      initial_state p (Callstate nil m nil).
-
-Inductive final_state : state -> Integers.int -> Prop :=
-| final_state_intro : forall retval retvali,
-    retvali = valueToInt retval ->
-    final_state (Returnstate nil retval) retvali.
-
-Definition semantics (m : program) :=
-  Smallstep.Semantics step (initial_state m) final_state
-                      (Globalenvs.Genv.globalenv m).
diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml
deleted file mode 100644
index 44f8b01..0000000
--- a/src/verilog/PrintHTL.ml
+++ /dev/null
@@ -1,81 +0,0 @@
-(* -*- mode: tuareg -*-
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2019-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/>.
- *)
-
-open Value
-open Datatypes
-open Camlcoq
-open AST
-open Clflags
-open Printf
-open Maps
-open AST
-open HTL
-open PrintAST
-open PrintVerilog
-open VericertClflags
-
-let pstr pp = fprintf pp "%s"
-
-let reg pp r =
-  fprintf pp "x%d" (P.to_int r)
-
-let rec regs pp = function
-  | [] -> ()
-  | [r] -> reg pp r
-  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
-
-let print_instruction pp (pc, i) =
-  fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i)
-
-let print_module pp id f =
-  fprintf pp "%s(%a) {\n" (extern_atom id) regs f.mod_params;
-  let datapath =
-    List.sort
-      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
-      (List.rev_map
-        (fun (pc, i) -> (P.to_int pc, i))
-        (PTree.elements f.mod_datapath)) in
-  let controllogic =
-    List.sort
-      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
-      (List.rev_map
-        (fun (pc, i) -> (P.to_int pc, i))
-        (PTree.elements f.mod_controllogic)) in
-  fprintf pp "  datapath {\n";
-  List.iter (print_instruction pp) datapath;
-  fprintf pp "  }\n\n  controllogic {\n";
-  List.iter (print_instruction pp) controllogic;
-  fprintf pp "  }\n}\n\n"
-
-let print_globdef pp (id, gd) =
-  match gd with
-  | Gfun(Internal f) -> print_module pp id f
-  | _ -> ()
-
-let print_program pp prog =
-  List.iter (print_globdef pp) prog.prog_defs
-
-let destination : string option ref = ref None
-
-let print_if prog =
-  match !destination with
-  | None -> ()
-  | Some f ->
-    let oc = open_out f in
-    print_program oc prog;
-    close_out oc
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
deleted file mode 100644
index 0f64066..0000000
--- a/src/verilog/PrintVerilog.ml
+++ /dev/null
@@ -1,232 +0,0 @@
-(* -*- mode: tuareg -*-
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2019-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/>.
- *)
-
-open Verilog
-open ValueInt
-open Datatypes
-
-open Camlcoq
-open AST
-open Clflags
-
-open Printf
-
-open VericertClflags
-
-let concat = String.concat ""
-
-let indent i = String.make (2 * i) ' '
-
-let fold_map f s = List.map f s |> concat
-
-let pstr pp = fprintf pp "%s"
-
-let pprint_binop l r =
-  let unsigned op = sprintf "{%s %s %s}" l op r in
-  let signed op = sprintf "{$signed(%s) %s $signed(%s)}" l op r in
-  function
-  | Vadd -> unsigned "+"
-  | Vsub -> unsigned "-"
-  | Vmul -> unsigned "*"
-  | Vdiv -> signed "/"
-  | Vdivu -> unsigned "/"
-  | Vmod -> signed "%"
-  | Vmodu -> unsigned "%"
-  | Vlt -> signed "<"
-  | Vltu -> unsigned "<"
-  | Vgt -> signed ">"
-  | Vgtu -> unsigned ">"
-  | Vle -> signed "<="
-  | Vleu -> unsigned "<="
-  | Vge -> signed ">="
-  | Vgeu -> unsigned ">="
-  | Veq -> unsigned "=="
-  | Vne -> unsigned "!="
-  | Vand -> unsigned "&"
-  | Vor -> unsigned "|"
-  | Vxor -> unsigned "^"
-  | Vshl -> unsigned "<<"
-  | Vshr -> signed ">>>"
-  | Vshru -> unsigned ">>"
-
-let unop = function
-  | Vneg -> " ~ "
-  | Vnot -> " ! "
-
-let register a = sprintf "reg_%d" (P.to_int a)
-
-(*let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*)
-
-let literal l = sprintf "32'd%ld" (camlint_of_coqint l)
-
-let rec pprint_expr = function
-  | Vlit l -> literal l
-  | Vvar s -> register s
-  | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"]
-  | Vinputvar s -> register s
-  | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"]
-  | Vbinop (op, a, b) -> concat [pprint_binop (pprint_expr a) (pprint_expr b) op]
-  | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"]
-
-let rec pprint_stmnt i =
-  let pprint_case (e, s) = concat [ indent (i + 1); pprint_expr e; ": begin\n"; pprint_stmnt (i + 2) s;
-                                    indent (i + 1); "end\n"
-                                  ]
-  in function
-  | Vskip -> concat [indent i; ";\n"]
-  | Vseq (s1, s2) -> concat [ pprint_stmnt i s1; pprint_stmnt i s2]
-  | Vcond (e, st, sf) -> concat [ indent i; "if ("; pprint_expr e; ") begin\n";
-                                  pprint_stmnt (i + 1) st; indent i; "end else begin\n";
-                                  pprint_stmnt (i + 1) sf;
-                                  indent i; "end\n"
-                                ]
-  | Vcase (e, es, d) -> concat [ indent i; "case ("; pprint_expr e; ")\n";
-                              fold_map pprint_case es; indent (i+1); "default:;\n";
-                              indent i; "endcase\n"
-                            ]
-  | Vblock (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"]
-  | Vnonblock (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"]
-
-let rec pprint_edge = function
-  | Vposedge r -> concat ["posedge "; register r]
-  | Vnegedge r -> concat ["negedge "; register r]
-  | Valledge -> "*"
-  | Voredge (e1, e2) -> concat [pprint_edge e1; " or "; pprint_edge e2]
-
-let pprint_edge_top i = function
-  | Vposedge r -> concat ["@(posedge "; register r; ")"]
-  | Vnegedge r -> concat ["@(negedge "; register r; ")"]
-  | Valledge -> "@*"
-  | Voredge (e1, e2) -> concat ["@("; pprint_edge e1; " or "; pprint_edge e2; ")"]
-
-let declare t =
-  function (r, sz) ->
-    concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
-             register r; ";\n" ]
-
-let declarearr t =
-  function (r, sz, ln) ->
-    concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
-             register r;
-             " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ]
-
-let print_io = function
-  | Some Vinput -> "input"
-  | Some Voutput -> "output reg"
-  | Some Vinout -> "inout"
-  | None -> "reg"
-
-let decl i = function
-  | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)]
-  | Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)]
-
-(* TODO Fix always blocks, as they currently always print the same. *)
-let pprint_module_item i = function
-  | Vdeclaration d -> decl i d
-  | Valways (e, s) ->
-    concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
-  | Valways_ff (e, s) ->
-    concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
-  | Valways_comb (e, s) ->
-    concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
-
-let rec intersperse c = function
-  | [] -> []
-  | [x] -> [x]
-  | x :: xs -> x :: c :: intersperse c xs
-
-let make_io i io r = concat [indent i; io; " "; register r; ";\n"]
-
-let compose f g x = g x |> f
-
-let testbench = "module testbench;
-   reg start, reset, clk;
-   wire finish;
-   wire [31:0] return_val;
-
-   main m(start, reset, clk, finish, return_val);
-
-   initial begin
-      clk = 0;
-      start = 0;
-      reset = 0;
-      @(posedge clk) reset = 1;
-      @(posedge clk) reset = 0;
-   end
-
-   always #5 clk = ~clk;
-
-   always @(posedge clk) begin
-      if (finish == 1) begin
-         $display(\"finished: %d\", return_val);
-         $finish;
-      end
-   end
-endmodule
-"
-
-let debug_always i clk state = concat [
-    indent i; "reg [31:0] count;\n";
-    indent i; "initial count = 0;\n";
-    indent i; "always @(posedge " ^ register clk ^ ") begin\n";
-    indent (i+1); "if(count[0:0] == 10'd0) begin\n";
-    indent (i+2); "$display(\"Cycle count %d\", count);\n";
-    indent (i+2); "$display(\"State %d\\n\", " ^ register state ^ ");\n";
-    indent (i+1); "end\n";
-    indent (i+1); "count <= count + 1;\n";
-    indent i; "end\n"
-  ]
-
-let print_initial i n stk = concat [
-    indent i; "integer i;\n";
-    indent i; "initial for(i = 0; i < "; sprintf "%d" n; "; i++)\n";
-    indent (i+1); register stk; "[i] = 0;\n"
-  ]
-
-let pprint_module debug i n m =
-  if (extern_atom n) = "main" then
-    let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in
-    let outputs = [m.mod_finish; m.mod_return] in
-    concat [ indent i; "module "; (extern_atom n);
-             "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n";
-             fold_map (pprint_module_item (i+1)) m.mod_body;
-             if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else "";
-             if debug then debug_always i m.mod_clk m.mod_st else "";
-             indent i; "endmodule\n\n"
-           ]
-  else ""
-
-let print_result pp lst =
-  let rec print_result_in pp = function
-    | [] -> fprintf pp "]\n"
-    | (r, v) :: ls ->
-      fprintf pp "%s -> %s; " (register r) (literal v);
-      print_result_in pp ls in
-  fprintf pp "[ ";
-  print_result_in pp lst
-
-let print_value pp v = fprintf pp "%s" (literal v)
-
-let print_globdef debug pp (id, gd) =
-  match gd with
-  | Gfun(Internal f) -> pstr pp (pprint_module debug 0 id f)
-  | _ -> ()
-
-let print_program debug pp prog =
-  List.iter (print_globdef debug pp) prog.prog_defs;
-  pstr pp testbench
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
deleted file mode 100644
index 6a15ee9..0000000
--- a/src/verilog/PrintVerilog.mli
+++ /dev/null
@@ -1,25 +0,0 @@
-(* 
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2019-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/>.
- *)
-
-val pprint_stmnt : int -> Verilog.stmnt -> string
-
-val print_value : out_channel -> ValueInt.value -> unit
-
-val print_program : bool -> out_channel -> Verilog.program -> unit
-
-val print_result : out_channel -> (BinNums.positive * ValueInt.value) list -> unit
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
deleted file mode 100644
index d6a3d8b..0000000
--- a/src/verilog/Value.v
+++ /dev/null
@@ -1,551 +0,0 @@
-(*
- * Vericert: 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/>.
- *)
-
-(* begin hide *)
-From bbv Require Import Word.
-From bbv Require HexNotation WordScope.
-From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
-From compcert Require Import lib.Integers common.Values.
-From vericert Require Import Vericertlib.
-(* end hide *)
-
-(** * Value
-
-A [value] is a bitvector with a specific size. We are using the implementation
-of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse.
-However, we need to wrap it with an [Inductive] so that we can specify and match
-on the size of the [value]. This is necessary so that we can easily store
-[value]s of different sizes in a list or in a map.
-
-Using the default [word], this would not be possible, as the size is part of the type. *)
-
-Record value : Type :=
-  mkvalue {
-    vsize: nat;
-    vword: word vsize
-  }.
-
-(** ** Value conversions
-
-Various conversions to different number types such as [N], [Z], [positive] and
-[int], where the last one is a theory of integers of powers of 2 in CompCert. *)
-
-Definition wordToValue : forall sz : nat, word sz -> value := mkvalue.
-
-Definition valueToWord : forall v : value, word (vsize v) := vword.
-
-Definition valueToNat (v :value) : nat :=
-  wordToNat (vword v).
-
-Definition natToValue sz (n : nat) : value :=
-  mkvalue sz (natToWord sz n).
-
-Definition valueToN (v : value) : N :=
-  wordToN (vword v).
-
-Definition NToValue sz (n : N) : value :=
-  mkvalue sz (NToWord sz n).
-
-Definition ZToValue (s : nat) (z : Z) : value :=
-  mkvalue s (ZToWord s z).
-
-Definition valueToZ (v : value) : Z :=
-  wordToZ (vword v).
-
-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 (uvalueToZ i).
-
-Definition ptrToValue (i : Integers.ptrofs) : value :=
-  ZToValue Ptrofs.wordsize (Ptrofs.unsigned i).
-
-Definition valueToPtr (i : value) : Integers.ptrofs :=
-  Ptrofs.repr (uvalueToZ i).
-
-Definition valToValue (v : Values.val) : option value :=
-  match v with
-  | Values.Vint i => Some (intToValue i)
-  | Values.Vptr b off => if Z.eqb (Z.modulo (uvalueToZ (ptrToValue off)) 4) 0%Z
-                         then Some (ptrToValue off)
-                         else None
-  | 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
-they can be used. *)
-
-Definition valueToBool (v : value) : bool :=
-  negb (weqb (@wzero (vsize v)) (vword v)).
-
-Definition boolToValue (sz : nat) (b : bool) : value :=
-  natToValue sz (if b then 1 else 0).
-
-(** ** Arithmetic operations *)
-
-Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
-intros; subst; assumption. Defined.
-
-Lemma unify_word_unfold :
-  forall sz w,
-  unify_word sz sz w eq_refl = w.
-Proof. auto. Qed.
-
-Definition value_eq_size:
-  forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }.
-Proof.
-  intros; destruct (Nat.eqb (vsize v1) (vsize v2)) eqn:?.
-  left; apply Nat.eqb_eq in Heqb; assumption.
-  right; trivial.
-Defined.
-
-Definition map_any {A : Type} (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A)
-           (EQ : vsize v1 = vsize v2) : A :=
-    let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in
-    f (vword v1) w2.
-
-Definition map_any_opt {A : Type} (sz : nat) (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A)
-  : option A :=
-  match value_eq_size v1 v2 with
-  | left EQ =>
-    Some (map_any v1 v2 f EQ)
-  | _ => None
-  end.
-
-Definition map_word (f : forall sz : nat, word sz -> word sz) (v : value) : value :=
-  mkvalue (vsize v) (f (vsize v) (vword v)).
-
-Definition map_word2 (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value)
-           (EQ : (vsize v1 = vsize v2)) : value :=
-    let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in
-    mkvalue (vsize v1) (f (vsize v1) (vword v1) w2).
-
-Definition map_word2_opt (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value)
-  : option value :=
-  match value_eq_size v1 v2 with
-  | left EQ => Some (map_word2 f v1 v2 EQ)
-  | _ => None
-  end.
-
-Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value)
-  : option value :=
-  match value_eq_size v1 v2 with
-  | left EQ => Some (f EQ)
-  | _ => 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.
-
-The arithmetic operations over [word] are over [N] by default, however, can also
-be called over [Z] explicitly, which is where the bits are interpreted in a
-signed manner. *)
-
-Definition vplus v1 v2 := map_word2 wplus v1 v2.
-Definition vplus_opt v1 v2 := map_word2_opt wplus v1 v2.
-Definition vminus v1 v2 := map_word2 wminus v1 v2.
-Definition vmul v1 v2 := map_word2 wmult v1 v2.
-Definition vdiv v1 v2 := map_word2 wdiv v1 v2.
-Definition vmod v1 v2 := map_word2 wmod v1 v2.
-
-Definition vmuls v1 v2 := map_word2 wmultZ v1 v2.
-Definition vdivs v1 v2 := map_word2 wdivZ v1 v2.
-Definition vmods v1 v2 := map_word2 wremZ v1 v2.
-
-(** ** Bitwise operations
-
-Bitwise operations over [value], which is independent of whether the number is
-signed or unsigned. *)
-
-Definition vnot v := map_word wnot v.
-Definition vneg v := map_word wneg v.
-Definition vbitneg v := boolToValue (vsize v) (negb (valueToBool v)).
-Definition vor v1 v2 := map_word2 wor v1 v2.
-Definition vand v1 v2 := map_word2 wand v1 v2.
-Definition vxor v1 v2 := map_word2 wxor v1 v2.
-
-(** ** Comparison operators
-
-Comparison operators that return a bool, there should probably be an equivalent
-which returns another number, however I might just add that as an explicit
-conversion. *)
-
-Definition veqb v1 v2 := map_any v1 v2 (@weqb (vsize v1)).
-Definition vneb v1 v2 EQ := negb (veqb v1 v2 EQ).
-
-Definition veq v1 v2 EQ := boolToValue (vsize v1) (veqb v1 v2 EQ).
-Definition vne v1 v2 EQ := boolToValue (vsize v1) (vneb v1 v2 EQ).
-
-Definition vltb v1 v2 := map_any v1 v2 wltb.
-Definition vleb v1 v2 EQ := negb (map_any v2 v1 wltb (eq_sym EQ)).
-Definition vgtb v1 v2 EQ := map_any v2 v1 wltb (eq_sym EQ).
-Definition vgeb v1 v2 EQ := negb (map_any v1 v2 wltb EQ).
-
-Definition vltsb v1 v2 := map_any v1 v2 wsltb.
-Definition vlesb v1 v2 EQ := negb (map_any v2 v1 wsltb (eq_sym EQ)).
-Definition vgtsb v1 v2 EQ := map_any v2 v1 wsltb (eq_sym EQ).
-Definition vgesb v1 v2 EQ := negb (map_any v1 v2 wsltb EQ).
-
-Definition vlt v1 v2 EQ := boolToValue (vsize v1) (vltb v1 v2 EQ).
-Definition vle v1 v2 EQ := boolToValue (vsize v1) (vleb v1 v2 EQ).
-Definition vgt v1 v2 EQ := boolToValue (vsize v1) (vgtb v1 v2 EQ).
-Definition vge v1 v2 EQ := boolToValue (vsize v1) (vgeb v1 v2 EQ).
-
-Definition vlts v1 v2 EQ := boolToValue (vsize v1) (vltsb v1 v2 EQ).
-Definition vles v1 v2 EQ := boolToValue (vsize v1) (vlesb v1 v2 EQ).
-Definition vgts v1 v2 EQ := boolToValue (vsize v1) (vgtsb v1 v2 EQ).
-Definition vges v1 v2 EQ := boolToValue (vsize v1) (vgesb v1 v2 EQ).
-
-(** ** Shift operators
-
-Shift operators on values. *)
-
-Definition shift_map (sz : nat) (f : word sz -> nat -> word sz) (w1 w2 : word sz) :=
-  f w1 (wordToNat w2).
-
-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',
-    i = valueToInt v' ->
-    val_value_lessdef (Vint i) v'
-| val_value_lessdef_ptr:
-    forall b off v',
-    off = valueToPtr v' ->
-    (Z.modulo (uvalueToZ v') 4) = 0%Z ->
-    val_value_lessdef (Vptr b off) v'
-| lessdef_undef: forall v, val_value_lessdef Vundef v.
-
-Inductive opt_val_value_lessdef: option val -> value -> Prop :=
-| opt_lessdef_some:
-    forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v'
-| opt_lessdef_none: forall v, opt_val_value_lessdef None 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 uvalueToZ_ZToValue_full :
-  forall sz : nat,
-  (0 < sz)%nat ->
-  forall z : Z, uvalueToZ (ZToValue sz z) = (z mod 2 ^ Z.of_nat sz)%Z.
-Proof. unfold uvalueToZ, ZToValue. simpl. auto using uwordToZ_ZToWord_full. Qed.
-
-Lemma ZToValue_uvalueToZ :
-  forall v,
-  ZToValue (vsize v) (uvalueToZ v) = v.
-Proof.
-  intros.
-  unfold ZToValue, uvalueToZ.
-  rewrite ZToWord_uwordToZ. destruct v; auto.
-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 by apply Pos.size_gt.
-  inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1.
-  simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.
-Qed.
-
-Lemma valueToPos_posToValue :
-  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 by apply Pos.size_gt.
-  inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1.
-  simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.
-Qed.
-
-Lemma valueToInt_intToValue :
-  forall v,
-  valueToInt (intToValue v) = v.
-Proof.
-  intros.
-  unfold valueToInt, intToValue. rewrite uvalueToZ_ZToValue. auto using Int.repr_unsigned.
-  split. apply Int.unsigned_range_2.
-  assert ((Int.unsigned v <= Int.max_unsigned)%Z) by apply Int.unsigned_range_2.
-  apply Z.lt_le_pred in H. apply H.
-Qed.
-
-Lemma valueToPtr_ptrToValue :
-  forall v,
-  valueToPtr (ptrToValue v) = v.
-Proof.
-  intros.
-  unfold valueToPtr, ptrToValue. rewrite uvalueToZ_ZToValue. auto using Ptrofs.repr_unsigned.
-  split. apply Ptrofs.unsigned_range_2.
-  assert ((Ptrofs.unsigned v <= Ptrofs.max_unsigned)%Z) by apply Ptrofs.unsigned_range_2.
-  apply Z.lt_le_pred in H. apply H.
-Qed.
-
-Lemma intToValue_valueToInt :
-  forall v,
-  vsize v = 32%nat ->
-  intToValue (valueToInt v) = v.
-Proof.
-  intros. unfold valueToInt, intToValue. rewrite Int.unsigned_repr_eq.
-  unfold ZToValue, uvalueToZ. unfold Int.modulus. unfold Int.wordsize. unfold Wordsize_32.wordsize.
-  pose proof (uwordToZ_bound (vword v)).
-  rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto.
-  rewrite <- H. rewrite two_power_nat_equiv. apply H0.
-Qed.
-
-Lemma ptrToValue_valueToPtr :
-  forall v,
-  vsize v = 32%nat ->
-  ptrToValue (valueToPtr v) = v.
-Proof.
-  intros. unfold valueToPtr, ptrToValue. rewrite Ptrofs.unsigned_repr_eq.
-  unfold ZToValue, uvalueToZ. unfold Ptrofs.modulus. unfold Ptrofs.wordsize. unfold Wordsize_Ptrofs.wordsize.
-  pose proof (uwordToZ_bound (vword v)).
-  rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto.
-  rewrite <- H. rewrite two_power_nat_equiv. apply H0.
-Qed.
-
-Lemma valToValue_lessdef :
-  forall v v',
-    valToValue v = Some v' ->
-    val_value_lessdef v v'.
-Proof.
-  intros.
-  destruct v; try discriminate; constructor.
-  unfold valToValue in H. inversion H.
-  symmetry. apply valueToInt_intToValue.
-  inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate.
-  inv H1. symmetry. apply valueToPtr_ptrToValue.
-  inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate.
-  inv H1. apply Z.eqb_eq. apply Heqb0.
-Qed.
-
-Lemma boolToValue_ValueToBool :
-  forall b,
-  valueToBool (boolToValue 32 b) = b.
-Proof. destruct b; auto. Qed.
-
-Local Open Scope Z.
-
-Ltac word_op_value H :=
-  intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold;
-  rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega.
-
-Lemma zadd_vplus :
-  forall sz z1 z2,
-  (sz > 0)%nat ->
-  uvalueToZ (vplus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 + z2) mod 2 ^ Z.of_nat sz.
-Proof. word_op_value ZToWord_plus. Qed.
-
-Lemma zadd_vplus2 :
-  forall z1 z2,
-  vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl = ZToValue 32 (z1 + z2).
-Proof.
-  intros. unfold vplus, ZToValue, map_word2. rewrite unify_word_unfold. simpl.
-  rewrite ZToWord_plus; auto.
-Qed.
-
-Lemma ZToValue_eq :
-  forall w1,
-  (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Abort.
-
-Lemma wordsize_32 :
-  Int.wordsize = 32%nat.
-Proof. auto. Qed.
-
-Lemma intadd_vplus :
-  forall i1 i2,
-  valueToInt (vplus (intToValue i1) (intToValue i2) eq_refl) = Int.add i1 i2.
-Proof.
-  intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus.
-  rewrite <- Int.unsigned_repr_eq.
-  rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega.
-Qed.
-
-(*Lemma intadd_vplus2 :
-  forall v1 v2 EQ,
-  vsize v1 = 32%nat ->
-  Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ).
-Proof.
-  intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr).
-  rewrite (@vadd_vplus v1 v2 EQ). trivial.
-  unfold uvalueToZ. pose proof (@uwordToZ_bound (vsize v2) (vword v2)).
-  rewrite H in EQ. rewrite <- EQ in H0 at 3.*)
-  (*rewrite zadd_vplus3. trivia*)
-
-Lemma valadd_vplus :
-  forall v1 v2 v1' v2' v v' EQ,
-  val_value_lessdef v1 v1' ->
-  val_value_lessdef v2 v2' ->
-  Val.add v1 v2 = v ->
-  vplus v1' v2' EQ = v' ->
-  val_value_lessdef v v'.
-Proof.
-  intros. inv H; inv H0; constructor; simplify.
-  Abort.
-
-Lemma zsub_vminus :
-  forall sz z1 z2,
-  (sz > 0)%nat ->
-  uvalueToZ (vminus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 - z2) mod 2 ^ Z.of_nat sz.
-Proof. word_op_value ZToWord_minus. Qed.
-
-Lemma zmul_vmul :
-  forall sz z1 z2,
-  (sz > 0)%nat ->
-  uvalueToZ (vmul (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 * z2) mod 2 ^ Z.of_nat sz.
-Proof. word_op_value ZToWord_mult. Qed.
-
-Local Open Scope N.
-Lemma zdiv_vdiv :
-  forall n1 n2,
-  n1 < 2 ^ 32 ->
-  n2 < 2 ^ 32 ->
-  n1 / n2 < 2 ^ 32 ->
-  valueToN (vdiv (NToValue 32 n1) (NToValue 32 n2) eq_refl) = n1 / n2.
-Proof.
-  intros; unfold valueToN, NToValue; simpl; rewrite unify_word_unfold. unfold wdiv.
-  unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto.
-Qed.
-
-Lemma ZToValue_valueToNat :
-  forall x sz,
-  (sz > 0)%nat ->
-  (0 <= x < 2^(Z.of_nat sz))%Z ->
-  valueToNat (ZToValue sz x) = Z.to_nat x.
-Proof.
-  destruct x; intros; unfold ZToValue, valueToNat; crush.
-  - rewrite wzero'_def. apply wordToNat_wzero.
-  - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial.
-    clear H1.
-    lazymatch goal with
-    | [ H : context[(_ < ?x)%Z] |- _ ] => replace x with (Z.of_nat (Z.to_nat x)) in H
-    end.
-    2: { apply Z2Nat.id; apply Z.pow_nonneg; lia. }
-
-    rewrite Z2Nat.inj_pow in H2; crush.
-    replace (Pos.to_nat 2) with 2%nat in H2 by reflexivity.
-    rewrite Nat2Z.id in H2.
-    rewrite <- positive_nat_Z in H2.
-    apply Nat2Z.inj_lt in H2.
-    assumption.
-Qed.
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v
deleted file mode 100644
index f1fd056..0000000
--- a/src/verilog/ValueInt.v
+++ /dev/null
@@ -1,167 +0,0 @@
-(*
- * Vericert: 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/>.
- *)
-
-(* begin hide *)
-From bbv Require Import Word.
-From bbv Require HexNotation WordScope.
-From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
-From compcert Require Import lib.Integers common.Values.
-From vericert Require Import Vericertlib.
-(* end hide *)
-
-(** * Value
-
-A [value] is a bitvector with a specific size. We are using the implementation
-of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse.
-However, we need to wrap it with an [Inductive] so that we can specify and match
-on the size of the [value]. This is necessary so that we can easily store
-[value]s of different sizes in a list or in a map.
-
-Using the default [word], this would not be possible, as the size is part of the type. *)
-
-Definition value : Type := int.
-
-(** ** Value conversions
-
-Various conversions to different number types such as [N], [Z], [positive] and
-[int], where the last one is a theory of integers of powers of 2 in CompCert. *)
-
-Definition valueToNat (v : value) : nat :=
-  Z.to_nat (Int.unsigned v).
-
-Definition natToValue (n : nat) : value :=
-  Int.repr (Z.of_nat n).
-
-Definition valueToN (v : value) : N :=
-  Z.to_N (Int.unsigned v).
-
-Definition NToValue (n : N) : value :=
-  Int.repr (Z.of_N n).
-
-Definition ZToValue (z : Z) : value :=
-  Int.repr z.
-
-Definition valueToZ (v : value) : Z :=
-  Int.signed v.
-
-Definition uvalueToZ (v : value) : Z :=
-  Int.unsigned v.
-
-Definition posToValue (p : positive) : value :=
-  Int.repr (Z.pos p).
-
-Definition valueToPos (v : value) : positive :=
-  Z.to_pos (Int.unsigned v).
-
-Definition intToValue (i : Integers.int) : value := i.
-
-Definition valueToInt (i : value) : Integers.int := i.
-
-Definition ptrToValue (i : ptrofs) : value := Ptrofs.to_int i.
-
-Definition valueToPtr (i : value) : Integers.ptrofs :=
-  Ptrofs.of_int i.
-
-Definition valToValue (v : Values.val) : option value :=
-  match v with
-  | Values.Vint i => Some (intToValue i)
-  | Values.Vptr b off => Some (ptrToValue off)
-  | Values.Vundef => Some (ZToValue 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
-they can be used. *)
-
-Definition valueToBool (v : value) : bool :=
-  if Z.eqb (uvalueToZ v) 0 then false else true.
-
-Definition boolToValue (b : bool) : value :=
-  natToValue (if b then 1 else 0).
-
-(** ** Arithmetic operations *)
-
-Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
-intros; subst; assumption. Defined.
-
-Lemma unify_word_unfold :
-  forall sz w,
-  unify_word sz sz w eq_refl = w.
-Proof. auto. Qed.
-
-Inductive val_value_lessdef: val -> value -> Prop :=
-| val_value_lessdef_int:
-    forall i v',
-    i = valueToInt v' ->
-    val_value_lessdef (Vint i) v'
-| val_value_lessdef_ptr:
-    forall b off v',
-    off = valueToPtr v' ->
-    val_value_lessdef (Vptr b off) v'
-| lessdef_undef: forall v, val_value_lessdef Vundef v.
-
-Inductive opt_val_value_lessdef: option val -> value -> Prop :=
-| opt_lessdef_some:
-    forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v'
-| opt_lessdef_none: forall v, opt_val_value_lessdef None v.
-
-Lemma valueToZ_ZToValue :
-  forall z,
-  (Int.min_signed <= z <= Int.max_signed)%Z ->
-  valueToZ (ZToValue z) = z.
-Proof. auto using Int.signed_repr. Qed.
-
-Lemma uvalueToZ_ZToValue :
-  forall z,
-  (0 <= z <= Int.max_unsigned)%Z ->
-  uvalueToZ (ZToValue z) = z.
-Proof. auto using Int.unsigned_repr. Qed.
-
-Lemma valueToPos_posToValue :
-  forall v,
-  0 <= Z.pos v <= Int.max_unsigned ->
-  valueToPos (posToValue v) = v.
-Proof.
-  unfold valueToPos, posToValue.
-  intros. rewrite Int.unsigned_repr.
-  apply Pos2Z.id. assumption.
-Qed.
-
-Lemma valueToInt_intToValue :
-  forall v,
-  valueToInt (intToValue v) = v.
-Proof. auto. Qed.
-
-Lemma valToValue_lessdef :
-  forall v v',
-    valToValue v = Some v' ->
-    val_value_lessdef v v'.
-Proof.
-  intros.
-  destruct v; try discriminate; constructor.
-  unfold valToValue in H. inversion H.
-  unfold valueToInt. unfold intToValue in H1. auto.
-  inv H. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial.
-Qed.
-
-Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue,
-                                       ptrToValue in *).
-
-Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption.
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
deleted file mode 100644
index 3b0dd0a..0000000
--- a/src/verilog/Verilog.v
+++ /dev/null
@@ -1,893 +0,0 @@
-(*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2019-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 Coq Require Import
-  Structures.OrderedTypeEx
-  FSets.FMapPositive
-  Program.Basics
-  PeanoNat
-  ZArith
-  Lists.List
-  Program.
-
-Require Import Lia.
-
-Import ListNotations.
-
-From vericert Require Import common.Vericertlib common.Show verilog.ValueInt AssocMap Array.
-From compcert Require Events.
-From compcert Require Import Integers Errors Smallstep Globalenvs.
-
-Local Open Scope assocmap.
-
-Set Implicit Arguments.
-
-Definition reg : Type := positive.
-Definition node : Type := positive.
-Definition szreg : Type := reg * nat.
-
-Record associations (A : Type) : Type :=
-  mkassociations {
-    assoc_blocking : AssocMap.t A;
-    assoc_nonblocking : AssocMap.t A
-  }.
-
-Definition arr := (Array (option value)).
-
-Definition reg_associations := associations value.
-Definition arr_associations := associations arr.
-
-Definition assocmap_reg := AssocMap.t value.
-Definition assocmap_arr := AssocMap.t arr.
-
-Definition merge_regs (new : assocmap_reg) (old : assocmap_reg) : assocmap_reg :=
-  AssocMapExt.merge value new old.
-
-Definition merge_cell (new : option value) (old : option value) : option value :=
-  match new, old with
-  | Some _, _ => new
-  | _, _ => old
-  end.
-
-Definition merge_arr (new : option arr) (old : option arr) : option arr :=
-  match new, old with
-  | Some new', Some old' => Some (combine merge_cell new' old')
-  | Some new', None => Some new'
-  | None, Some old' => Some old'
-  | None, None => None
-  end.
-
-Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr :=
-  AssocMap.combine merge_arr new old.
-
-Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
-  match a ! r with
-  | None => None
-  | Some arr => Some (Option.default (NToValue 0) (Option.join (array_get_error i arr)))
-  end.
-
-Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
-  match a ! r with
-  | None => a
-  | Some arr => a # r <- (array_set i (Some v) arr)
-  end.
-
-Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
-  mkassociations (arr_assocmap_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking).
-
-Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
-  mkassociations asa.(assoc_blocking) (arr_assocmap_set r i v asa.(assoc_nonblocking)).
-
-Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
-  mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking).
-
-Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
-  mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)).
-
-Inductive scl_decl : Type := VScalar (sz : nat).
-Inductive arr_decl : Type := VArray (sz : nat) (ln : nat).
-
-(** * Verilog AST
-
-The Verilog AST is defined here, which is the target language of the
-compilation.
-
-** Value
-
-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. *)
-
-(** ** Binary Operators
-
-These are the binary operations that can be represented in Verilog. Ideally,
-multiplication and division would be done by custom modules which could al so be
-scheduled properly. However, for now every Verilog operator is assumed to take
-one clock cycle. *)
-
-Inductive binop : Type :=
-| Vadd : binop  (** addition (binary [+]) *)
-| Vsub : binop  (** subtraction (binary [-]) *)
-| Vmul : binop  (** multiplication (binary [*]) *)
-| Vdiv : binop  (** division (binary [/]) *)
-| Vdivu : binop  (** division unsigned (binary [/]) *)
-| Vmod : binop  (** remainder ([%]) *)
-| Vmodu : binop  (** remainder unsigned ([%]) *)
-| Vlt : binop   (** less than ([<]) *)
-| Vltu : binop   (** less than unsigned ([<]) *)
-| Vgt : binop   (** greater than ([>]) *)
-| Vgtu : binop   (** greater than unsigned ([>]) *)
-| Vle : binop   (** less than or equal ([<=]) *)
-| Vleu : binop   (** less than or equal unsigned ([<=]) *)
-| Vge : binop   (** greater than or equal ([>=]) *)
-| Vgeu : binop   (** greater than or equal unsigned ([>=]) *)
-| Veq : binop   (** equal to ([==]) *)
-| Vne : binop   (** not equal to ([!=]) *)
-| Vand : binop  (** and (binary [&]) *)
-| Vor : binop   (** or (binary [|]) *)
-| Vxor : binop  (** xor (binary [^|]) *)
-| Vshl : binop  (** shift left ([<<]) *)
-| Vshr : binop (** shift right ([>>>]) *)
-| Vshru : binop. (** shift right unsigned ([>>]) *)
-(*| Vror : binop (** shift right unsigned ([>>]) *)*)
-
-(** ** Unary Operators *)
-
-Inductive unop : Type :=
-| Vneg  (** negation ([~]) *)
-| Vnot. (** not operation [!] *)
-
-(** ** Expressions *)
-
-Inductive expr : Type :=
-| Vlit : value -> expr
-| Vvar : reg -> expr
-| Vvari : reg -> expr -> expr
-| Vinputvar : reg -> expr
-| Vbinop : binop -> expr -> expr -> expr
-| Vunop : unop -> expr -> expr
-| Vternary : expr -> expr -> expr -> expr.
-
-Definition posToExpr (p : positive) : expr :=
-  Vlit (posToValue p).
-
-(** ** Statements *)
-
-Inductive stmnt : Type :=
-| Vskip : stmnt
-| Vseq : stmnt -> stmnt -> stmnt
-| Vcond : expr -> stmnt -> stmnt -> stmnt
-| Vcase : expr -> list (expr * stmnt) -> option stmnt -> stmnt
-| Vblock : expr -> expr -> stmnt
-| Vnonblock : expr -> expr -> stmnt.
-
-(** ** Edges
-
-These define when an always block should be triggered, for example if the always
-block should be triggered synchronously at the clock edge, or asynchronously for
-combinational logic.
-
-[edge] is not part of [stmnt] in this formalisation because is closer to the
-semantics that are used. *)
-
-Inductive edge : Type :=
-| Vposedge : reg -> edge
-| Vnegedge : reg -> edge
-| Valledge : edge
-| Voredge : edge -> edge -> edge.
-
-(** ** Module Items
-
-Module items can either be declarations ([Vdecl]) or always blocks ([Valways]).
-The declarations are always register declarations as combinational logic can be
-done using combinational always block instead of continuous assignments. *)
-
-Inductive io : Type :=
-| Vinput : io
-| Voutput : io
-| Vinout : io.
-
-Inductive declaration : Type :=
-| Vdecl : option io -> reg -> nat -> declaration
-| Vdeclarr : option io -> reg -> nat -> nat -> declaration.
-
-Inductive module_item : Type :=
-| Vdeclaration : declaration -> module_item
-| Valways : edge -> stmnt -> module_item
-| Valways_ff : edge -> stmnt -> module_item
-| Valways_comb : edge -> stmnt -> module_item.
-
-(** The main module type containing all the important control signals
-
-- [mod_start] If set, starts the computations in the module.
-- [mod_reset] If set, reset the state in the module.
-- [mod_clk] The clock that controls the computation in the module.
-- [mod_args] The arguments to the module.
-- [mod_finish] Bit that is set if the result is ready.
-- [mod_return] The return value that was computed.
-- [mod_body] The body of the module, including the state machine.
-*)
-
-Record module : Type := mkmodule {
-  mod_start : reg;
-  mod_reset : reg;
-  mod_clk : reg;
-  mod_finish : reg;
-  mod_return : reg;
-  mod_st : reg; (**r Variable that defines the current state, it should be internal. *)
-  mod_stk : reg;
-  mod_stk_len : nat;
-  mod_args : list reg;
-  mod_body : list module_item;
-  mod_entrypoint : node;
-}.
-
-Definition fundef := AST.fundef module.
-
-Definition program := AST.program fundef unit.
-
-(** Convert a [positive] to an expression directly, setting it to the right
-    size. *)
-Definition posToLit (p : positive) : expr :=
-  Vlit (posToValue p).
-
-Definition fext := unit.
-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.
-- 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 stackframe : Type :=
-  Stackframe :
-    forall  (res : reg)
-            (m : module)
-            (pc : node)
-            (reg_assoc : assocmap_reg)
-            (arr_assoc : assocmap_arr),
-      stackframe.
-
-Inductive state : Type :=
-| State :
-    forall (stack : list stackframe)
-           (m : module)
-           (st : node)
-           (reg_assoc : assocmap_reg)
-           (arr_assoc : assocmap_arr), state
-| Returnstate :
-    forall (res : list stackframe)
-           (v : value), state
-| Callstate :
-    forall (stack : list stackframe)
-           (m : module)
-           (args : list value), state.
-
-Definition binop_run (op : binop) (v1 v2 : value) : option value :=
-  match op with
-  | Vadd => Some (Int.add v1 v2)
-  | Vsub => Some (Int.sub v1 v2)
-  | Vmul => Some (Int.mul v1 v2)
-  | Vdiv => if Int.eq v2 Int.zero
-               || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone
-            then None
-            else Some (Int.divs v1 v2)
-  | Vdivu => if Int.eq v2 Int.zero then None else Some (Int.divu v1 v2)
-  | Vmod => if Int.eq v2 Int.zero
-               || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone
-            then None
-            else Some (Int.mods v1 v2)
-  | Vmodu => if Int.eq v2 Int.zero then None else Some (Int.modu v1 v2)
-  | Vlt => Some (boolToValue (Int.lt v1 v2))
-  | Vltu => Some (boolToValue (Int.ltu v1 v2))
-  | Vgt => Some (boolToValue (Int.lt v2 v1))
-  | Vgtu => Some (boolToValue (Int.ltu v2 v1))
-  | Vle => Some (boolToValue (negb (Int.lt v2 v1)))
-  | Vleu => Some (boolToValue (negb (Int.ltu v2 v1)))
-  | Vge => Some (boolToValue (negb (Int.lt v1 v2)))
-  | Vgeu => Some (boolToValue (negb (Int.ltu v1 v2)))
-  | Veq => Some (boolToValue (Int.eq v1 v2))
-  | Vne => Some (boolToValue (negb (Int.eq v1 v2)))
-  | Vand => Some (Int.and v1 v2)
-  | Vor => Some (Int.or v1 v2)
-  | Vxor => Some (Int.xor v1 v2)
-  | Vshl => Some (Int.shl v1 v2)
-  | Vshr => Some (Int.shr v1 v2)
-  | Vshru => Some (Int.shru v1 v2)
-  end.
-
-Definition unop_run (op : unop) (v1 : value) : value :=
-  match op with
-  | Vneg => Int.neg v1
-  | Vnot => Int.not v1
-  end.
-
-Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop :=
-  | erun_Vlit :
-      forall fext reg stack v,
-      expr_runp fext reg stack (Vlit v) v
-  | erun_Vvar :
-      forall fext reg stack v r,
-      reg#r = v ->
-      expr_runp fext reg stack (Vvar r) v
-  | erun_Vvari :
-      forall fext reg stack v iexp i r,
-      expr_runp fext reg stack iexp i ->
-      arr_assocmap_lookup stack r (valueToNat i) = Some v ->
-      expr_runp fext reg stack (Vvari r iexp) v
-  | erun_Vbinop :
-      forall fext reg stack op l r lv rv resv,
-      expr_runp fext reg stack l lv ->
-      expr_runp fext reg stack r rv ->
-      Some resv = binop_run op lv rv ->
-      expr_runp fext reg stack (Vbinop op l r) resv
-  | erun_Vunop :
-      forall fext reg stack u vu op oper resv,
-      expr_runp fext reg stack u vu ->
-      oper = unop_run op ->
-      resv = oper vu ->
-      expr_runp fext reg stack (Vunop op u) resv
-  | erun_Vternary_true :
-      forall fext reg stack c ts fs vc vt,
-      expr_runp fext reg stack c vc ->
-      expr_runp fext reg stack ts vt ->
-      valueToBool vc = true ->
-      expr_runp fext reg stack (Vternary c ts fs) vt
-  | erun_Vternary_false :
-      forall fext reg stack c ts fs vc vf,
-      expr_runp fext reg stack c vc ->
-      expr_runp fext reg stack fs vf ->
-      valueToBool vc = false ->
-      expr_runp fext reg stack (Vternary c ts fs) vf.
-Hint Constructors expr_runp : verilog.
-
-Definition handle_opt {A : Type} (err : errmsg) (val : option A)
-  : res A :=
-  match val with
-  | Some a => OK a
-  | None => Error err
-  end.
-
-Definition handle_def {A : Type} (a : A) (val : option A)
-  : res A :=
-  match val with
-  | Some a' => OK a'
-  | None => OK a
-  end.
-
-Local Open Scope error_monad_scope.
-
-(*Definition access_fext (f : fext) (r : reg) : res value :=
-  match AssocMap.get r f with
-  | Some v => OK v
-  | _ => OK (ZToValue 0)
-  end.*)
-
-(* TODO FIX Vvar case without default *)
-(*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
-              | _ => Error (msg "Verilog: Wrong state")
-              end
-  | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled")
-  | Vinputvar r => access_fext s r
-  | Vbinop op l r =>
-    let lv := expr_run s l in
-    let rv := expr_run s r in
-    let oper := binop_run op in
-    do lv' <- lv;
-    do rv' <- rv;
-    handle_opt (msg "Verilog: sizes are not equal")
-               (eq_to_opt lv' rv' (oper lv' rv'))
-  | Vunop op e =>
-    let oper := unop_run op in
-    do ev <- expr_run s e;
-    OK (oper ev)
-  | Vternary c te fe =>
-    do cv <- expr_run s c;
-    if valueToBool cv then expr_run s te else expr_run s fe
-  end.*)
-
-(** Return the location of the lhs of an assignment. *)
-
-Inductive location : Type :=
-| LocReg (_ : reg)
-| LocArray (_ : reg) (_ : nat).
-
-Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop :=
-| Base : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r)
-| Indexed : forall f asr asa r iexp iv,
-  expr_runp f asr asa iexp iv ->
-  location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)).
-
-(* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l)  (e : expr) : res reg := *)
-(*   match e with *)
-(*   | Vvar r => OK r *)
-(*   | _ => 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
-  | (e, st)::xs =>
-    match expr_run s e with
-    | OK v' =>
-      match eq_to_opt v v' (veq v v') with
-      | Some eq => if valueToBool eq then Some (OK st) else find_case_stmnt s v xs
-      | None => Some (Error (msg "Verilog: equality check sizes not equal"))
-      end
-    | Error msg => Some (Error msg)
-    end
-  | _ => None
-  end.
-
-Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
-  match n with
-  | S n' =>
-    match st with
-    | Vskip => OK s
-    | Vseq s1 s2 =>
-      do s' <- stmnt_run' n' s s1;
-      stmnt_run' n' s' s2
-    | Vcond c st sf =>
-      do cv <- expr_run s c;
-      if valueToBool cv
-      then stmnt_run' n' s st
-      else stmnt_run' n' s sf
-    | Vcase e cl defst =>
-      do v <- expr_run s e;
-      match find_case_stmnt s v cl with
-      | Some (OK st') => stmnt_run' n' s st'
-      | Some (Error msg) => Error msg
-      | None => do s' <- handle_opt (msg "Verilog: no case was matched")
-                                    (option_map (stmnt_run' n' s) defst); s'
-      end
-    | Vblock lhs rhs =>
-      match s with
-      | State m assoc nbassoc f c =>
-        do name <- assign_name lhs;
-        do rhse <- expr_run s rhs;
-        OK (State m (PositiveMap.add name rhse assoc) nbassoc f c)
-      | _ => Error (msg "Verilog: Wrong state")
-      end
-    | Vnonblock lhs rhs =>
-      match s with
-      | State m assoc nbassoc f c =>
-        do name <- assign_name lhs;
-        do rhse <- expr_run s rhs;
-        OK (State 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. *)
-
-Inductive stmnt_runp: fext -> reg_associations -> arr_associations ->
-                      stmnt -> reg_associations -> arr_associations -> Prop :=
-| stmnt_runp_Vskip:
-    forall f ar al, stmnt_runp f ar al Vskip ar al
-| stmnt_runp_Vseq:
-    forall f st1 st2 asr0 asa0 asr1 asa1 asr2 asa2,
-    stmnt_runp f asr0 asa0 st1 asr1 asa1 ->
-    stmnt_runp f asr1 asa1 st2 asr2 asa2 ->
-    stmnt_runp f asr0 asa0 (Vseq st1 st2) asr2 asa2
-| stmnt_runp_Vcond_true:
-    forall asr0 asa0 asr1 asa1 f c vc stt stf,
-    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc ->
-    valueToBool vc = true ->
-    stmnt_runp f asr0 asa0 stt asr1 asa1 ->
-    stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1
-| stmnt_runp_Vcond_false:
-    forall asr0 asa0 asr1 asa1 f c vc stt stf,
-    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc ->
-    valueToBool vc = false ->
-    stmnt_runp f asr0 asa0 stf asr1 asa1 ->
-    stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1
-| stmnt_runp_Vcase_nomatch:
-    forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def,
-    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
-    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve ->
-    mve <> ve ->
-    stmnt_runp f asr0 asa0 (Vcase e cs def) asr1 asa1 ->
-    stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1
-| stmnt_runp_Vcase_match:
-    forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def,
-    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
-    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve ->
-    mve = ve ->
-    stmnt_runp f asr0 asa0 sc asr1 asa1 ->
-    stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1
-| stmnt_runp_Vcase_default:
-    forall asr0 asa0 asr1 asa1 f st e ve,
-    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
-    stmnt_runp f asr0 asa0 st asr1 asa1 ->
-    stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1
-| stmnt_runp_Vblock_reg:
-    forall lhs r rhs rhsval asr asa f,
-    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) ->
-    expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
-    stmnt_runp f asr asa
-                 (Vblock lhs rhs)
-                 (block_reg r asr rhsval) asa
-| stmnt_runp_Vnonblock_reg:
-    forall lhs r rhs rhsval asr asa f,
-    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) ->
-    expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
-    stmnt_runp f asr asa
-                 (Vnonblock lhs rhs)
-                 (nonblock_reg r asr rhsval) asa
-| stmnt_runp_Vblock_arr:
-    forall lhs r i rhs rhsval asr asa f,
-    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) ->
-    expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
-    stmnt_runp f asr asa
-                 (Vblock lhs rhs)
-                 asr (block_arr r i asa rhsval)
-| stmnt_runp_Vnonblock_arr:
-    forall lhs r i rhs rhsval asr asa f,
-    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) ->
-    expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
-    stmnt_runp f asr asa
-                 (Vnonblock lhs rhs)
-                 asr (nonblock_arr r i asa rhsval).
-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
-  in
-  match m with
-  | (Valways _ st)::ls => run st ls
-  | (Valways_ff _ st)::ls => run st ls
-  | (Valways_comb _ st)::ls => run st ls
-  | (Vdecl _ _)::ls => mi_step s ls
-  | (Vdeclarr _ _ _)::ls => mi_step s ls
-  | nil => OK s
-  end.*)
-
-Inductive mi_stepp : fext -> reg_associations -> arr_associations ->
-                     module_item -> reg_associations -> arr_associations -> Prop :=
-| mi_stepp_Valways :
-    forall f sr0 sa0 st sr1 sa1 c,
-    stmnt_runp f sr0 sa0 st sr1 sa1 ->
-    mi_stepp f sr0 sa0 (Valways c st) sr1 sa1
-| mi_stepp_Valways_ff :
-    forall f sr0 sa0 st sr1 sa1 c,
-    stmnt_runp f sr0 sa0 st sr1 sa1 ->
-    mi_stepp f sr0 sa0 (Valways_ff c st) sr1 sa1
-| mi_stepp_Valways_comb :
-    forall f sr0 sa0 st sr1 sa1 c,
-    stmnt_runp f sr0 sa0 st sr1 sa1 ->
-    mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1
-| mi_stepp_Vdecl :
-    forall f sr sa d,
-    mi_stepp f sr sa (Vdeclaration d) sr sa.
-Hint Constructors mi_stepp : verilog.
-
-Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
-                      list module_item -> reg_associations -> arr_associations -> Prop :=
-| mis_stepp_Cons :
-    forall f mi mis sr0 sa0 sr1 sa1 sr2 sa2,
-    mi_stepp f sr0 sa0 mi sr1 sa1 ->
-    mis_stepp f sr1 sa1 mis sr2 sa2 ->
-    mis_stepp f sr0 sa0 (mi :: mis) sr2 sa2
-| mis_stepp_Nil :
-    forall f sr sa,
-    mis_stepp f sr sa nil sr sa.
-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 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 : 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_assocmap f (Pos.of_nat n')) m with
-    | OK (State 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 => (AssocMap.set (mod_reset m) (ZToValue 1) empty_assocmap)
-           | _ => (AssocMap.set (mod_reset m) (ZToValue 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.
-
-(*Theorem value_eq_size_if_eq:
-  forall lv rv EQ,
-  vsize lv = vsize rv -> value_eq_size lv rv = left EQ.
-Proof. intros. unfold value_eq_size.
-
-Theorem expr_run_same:
-  forall assoc e v, expr_run assoc e = OK v <-> expr_runp assoc e v.
-Proof.
-  split; generalize dependent v; generalize dependent assoc.
-  - induction e.
-    + intros. inversion H. constructor.
-    + intros. inversion H. constructor. assumption.
-    + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (expr_run assoc e2) eqn:?.
-      unfold eq_to_opt in H1. destruct (value_eq_size v0 v1) eqn:?. inversion H1.
-      constructor. apply IHe1. assumption. apply IHe2. assumption. reflexivity. discriminate. discriminate.
-      discriminate.
-    + intros. inversion H. destruct (expr_run assoc e) eqn:?. unfold option_map in H1.
-      inversion H1. constructor. apply IHe. assumption. reflexivity. discriminate.
-    + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (valueToBool v0) eqn:?.
-      eapply erun_Vternary_true. apply IHe1. eassumption. apply IHe2. eassumption. assumption.
-      eapply erun_Vternary_false. apply IHe1. eassumption. apply IHe3. eassumption. assumption.
-      discriminate.
-  - induction e.
-    + intros. inversion H. reflexivity.
-    + intros. inversion H. subst. simpl. assumption.
-    + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4.
-      apply IHe2 in H6. rewrite H6. unfold eq_to_opt. assert (vsize lv = vsize rv).
-      apply EQ. apply (value_eq_size_if_eq lv rv EQ) in H0. rewrite H0. reflexivity.
-    + intros. inversion H. subst. simpl. destruct (expr_run assoc e) eqn:?. simpl.
-      apply IHe in H3. rewrite Heqo in H3.
-      inversion H3. subst. reflexivity. apply IHe in H3. rewrite Heqo in H3. discriminate.
-    + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7.
-      apply IHe2 in H6. rewrite H6. reflexivity.
-      subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. apply IHe3.
-      assumption.
-Qed.
-
- *)
-
-Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} :=
-  match rl, vl with
-  | r :: rl', v :: vl' => AssocMap.set r v (init_params vl' rl')
-  | _, _ => empty_assocmap
-  end.
-
-Definition genv := Globalenvs.Genv.t fundef unit.
-Definition empty_stack (m : module) : assocmap_arr :=
-  (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty arr)).
-
-Inductive step : genv -> state -> Events.trace -> state -> Prop :=
-  | step_module :
-      forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist,
-      asr!(m.(mod_reset)) = Some (ZToValue 0) ->
-      asr!(m.(mod_finish)) = Some (ZToValue 0) ->
-      asr!(m.(mod_st)) = Some ist ->
-      valueToPos ist = st ->
-      mis_stepp f (mkassociations asr empty_assocmap)
-                  (mkassociations asa (empty_stack m))
-                  m.(mod_body)
-                  (mkassociations basr1 nasr1)
-                  (mkassociations basa1 nasa1)->
-      asr' = merge_regs nasr1 basr1 ->
-      asa' = merge_arrs nasa1 basa1 ->
-      asr'!(m.(mod_st)) = Some stval ->
-      valueToPos stval = pstval ->
-      step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
-| step_finish :
-    forall asr asa sf retval m st g,
-    asr!(m.(mod_finish)) = Some (ZToValue 1) ->
-    asr!(m.(mod_return)) = Some retval ->
-    step g (State sf m st asr asa) Events.E0 (Returnstate sf retval)
-| step_call :
-    forall g res m args,
-    step g (Callstate res m args) Events.E0
-         (State res m m.(mod_entrypoint)
-          (AssocMap.set (mod_reset m) (ZToValue 0)
-           (AssocMap.set (mod_finish m) (ZToValue 0)
-            (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint))
-             (init_params args m.(mod_args)))))
-          (empty_stack m))
-| step_return :
-    forall g m asr i r sf pc mst asa,
-    mst = mod_st m ->
-    step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
-         (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa).
-Hint Constructors step : verilog.
-
-Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b m0 m,
-      let ge := Globalenvs.Genv.globalenv p in
-      Globalenvs.Genv.init_mem p = Some m0 ->
-      Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
-      Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) ->
-      initial_state p (Callstate nil m nil).
-
-Inductive final_state : state -> Integers.int -> Prop :=
-| final_state_intro : forall retval retvali,
-    retvali = valueToInt retval ->
-    final_state (Returnstate nil retval) retvali.
-
-Definition semantics (m : program) :=
-  Smallstep.Semantics step (initial_state m) final_state
-                      (Globalenvs.Genv.globalenv m).
-
-Lemma expr_runp_determinate :
-  forall f e asr asa v,
-  expr_runp f asr asa e v ->
-  forall v',
-  expr_runp f asr asa e v' ->
-  v' = v.
-Proof.
-  induction e; intros;
-
-  repeat (try match goal with
-              | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => invert H
-
-              | [ H1 : forall asr asa v, expr_runp _ asr asa ?e v -> _,
-                  H2 : expr_runp _ _ _ ?e _ |- _ ] =>
-                learn (H1 _ _ _ H2)
-              | [ H1 : forall v, expr_runp _ ?asr ?asa ?e v -> _,
-                  H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] =>
-                learn (H1 _ H2)
-              end; crush).
-Qed.
-Hint Resolve expr_runp_determinate : verilog.
-
-Lemma location_is_determinate :
-  forall f asr asa e l,
-  location_is f asr asa e l ->
-  forall l',
-  location_is f asr asa e l' ->
-  l' = l.
-Proof.
-  induction 1; intros;
-
-  repeat (try match goal with
-              | [ H : location_is _ _ _ _ _ |- _ ] => invert H
-              | [ H1 : expr_runp _ ?asr ?asa ?e _,
-                  H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] =>
-                learn (expr_runp_determinate H1 H2)
-              end; crush).
-Qed.
-
-Lemma stmnt_runp_determinate :
-  forall f s asr0 asa0 asr1 asa1,
-  stmnt_runp f asr0 asa0 s asr1 asa1 ->
-  forall asr1' asa1',
-  stmnt_runp f asr0 asa0 s asr1' asa1' ->
-  asr1' = asr1 /\ asa1' = asa1.
-  induction 1; intros;
-
-  repeat (try match goal with
-             | [ H : stmnt_runp _ _ _ (Vseq _ _) _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ (Vnonblock _ _) _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ (Vcase _ (_ :: _) _) _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ (Vcase _ []  _) _ _ |- _ ] => invert H
-
-             | [ H1 : expr_runp _ ?asr ?asa ?e _,
-                 H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] =>
-               learn (expr_runp_determinate H1 H2)
-
-             | [ H1 : location_is _ ?asr ?asa ?e _,
-                 H2 : location_is _ ?asr ?asa ?e _ |- _ ] =>
-               learn (location_is_determinate H1 H2)
-
-             | [ H1 : forall asr1 asa1, stmnt_runp _ ?asr0 ?asa0 ?s asr1 asa1 -> _,
-                 H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] =>
-               learn (H1 _ _ H2)
-              end; crush).
-Qed.
-Hint Resolve stmnt_runp_determinate : verilog.
-
-Lemma mi_stepp_determinate :
-  forall f asr0 asa0 m asr1 asa1,
-  mi_stepp f asr0 asa0 m asr1 asa1 ->
-  forall asr1' asa1',
-  mi_stepp f asr0 asa0 m asr1' asa1' ->
-  asr1' = asr1 /\ asa1' = asa1.
-Proof.
-  intros. destruct m; invert H; invert H0;
-
-  repeat (try match goal with
-              | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _,
-                  H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] =>
-                learn (stmnt_runp_determinate H1 H2)
-              end; crush).
-Qed.
-
-Lemma mis_stepp_determinate :
-  forall f asr0 asa0 m asr1 asa1,
-  mis_stepp f asr0 asa0 m asr1 asa1 ->
-  forall asr1' asa1',
-  mis_stepp f asr0 asa0 m asr1' asa1' ->
-  asr1' = asr1 /\ asa1' = asa1.
-Proof.
-  induction 1; intros;
-
-  repeat (try match goal with
-              | [ H : mis_stepp _ _ _ [] _ _ |- _ ] => invert H
-              | [ H : mis_stepp _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H
-
-              | [ H1 : mi_stepp _ ?asr0 ?asa0 ?s _ _,
-                  H2 : mi_stepp _ ?asr0 ?asa0 ?s _ _ |- _ ] =>
-                learn (mi_stepp_determinate H1 H2)
-
-             | [ H1 : forall asr1 asa1, mis_stepp _ ?asr0 ?asa0 ?m asr1 asa1 -> _,
-                 H2 : mis_stepp _ ?asr0 ?asa0 ?m _ _ |- _ ] =>
-               learn (H1 _ _ H2)
-              end; crush).
-Qed.
-
-Lemma semantics_determinate :
-  forall (p: program), Smallstep.determinate (semantics p).
-Proof.
-  intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify.
-  - invert H; invert H0; constructor. (* Traces are always empty *)
-  - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst.
-    pose proof (mis_stepp_determinate H5 H15).
-    crush.
-  - constructor. invert H; crush.
-  - invert H; invert H0; unfold ge0, ge1 in *; crush.
-  - red; simplify; intro; invert H0; invert H; crush.
-  - invert H; invert H0; crush.
-Qed.