Merge branch 'develop' into arrays-proof

25 files changed, 2277 insertions, 369 deletions

diff --git a/.gitignore b/.gitignore
index 7c17072..b2cf595 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,6 +17,8 @@
 *.v.d
 *.vio
 *.vo
+*.vok
+*.vos
 .coq-native/
 .csdp.cache
 .lia.cache
diff --git a/Makefile b/Makefile
index 1d328ec..42e6a45 100644
--- a/Makefile
+++ b/Makefile
@@ -1,18 +1,23 @@
+UNAME_S := $(shell uname -s)
+ifeq ($(UNAME_S),Linux)
+	ARCH := x86_64-linux
+endif
+ifeq ($(UNAME_S),Darwin)
+	ARCH := x86_64-macosx
+endif
+
 COMPCERTRECDIRS := lib common x86_64 x86 backend cfrontend driver flocq exportclight \
   MenhirLib cparser
 
-COMPCERTCOQINCLUDES := $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d))
-
 COQINCLUDES := -R src/common coqup.common -R src/verilog coqup.verilog \
                -R src/extraction coqup.extraction -R src/translation coqup.translation \
-               -R src coqup $(COMPCERTCOQINCLUDES)
+               -R src coqup \
+               $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d))
 
 COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
-COQMAKE := "$(COQBIN)coq_makefile"
+COQMAKE := $(COQBIN)coq_makefile
 
-COQUPDIRS := translation common verilog
-VSSUBDIR := $(foreach d, $(COQUPDIRS), src/$(d)/*.v)
-VS := src/Compiler.v src/Simulator.v $(VSSUBDIR)
+VS := src/Compiler.v src/Simulator.v $(foreach d, translation common verilog, src/$(d)/*.v)
 
 PREFIX ?= .
 
@@ -23,7 +28,7 @@ all: lib/COMPCERTSTAMP
 	$(MAKE) compile
 
 lib/COMPCERTSTAMP:
-	(cd lib/CompCert && ./configure x86_64-linux)
+	(cd lib/CompCert && ./configure $(ARCH))
 	$(MAKE) -C lib/CompCert
 	touch $@
 
diff --git a/README.md b/README.md
index df65f8c..026266b 100644
--- a/README.md
+++ b/README.md
@@ -18,14 +18,6 @@ The project is written in Coq, a theorem prover, which is extracted to OCaml so
 
 These dependencies can be installed manually, or automatically through Nix.
 
-### Building on OSX
-
-To build the project on OSX, currently the makefile has to be manually edited so that CompCert builds for the correct architecture. To do this, simply execute the following `sed` command to change the instance of `x86_64-linux` into `x86_64-macosx`.
-
-``` shell
-sed -i'' 's/x86_64-linux/x86_64-macosx/' Makefile
-```
-
 ### Downloading CompCert
 
 CompCert is added as a submodule in the `lib/CompCert` directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run:
diff --git a/debug/CoqupTest.ml b/debug/CoqupTest.ml
new file mode 100644
index 0000000..f961f64
--- /dev/null
+++ b/debug/CoqupTest.ml
@@ -0,0 +1,59 @@
+open Coqup
+
+open Test
+open Camlcoq
+open FMapPositive
+
+let test_function_transf () =
+  print_endline "Testing transformation";
+  print_endline "TL PROGRAM: ";
+  PrintRTL.print_program stdout testinputprogram;
+  print_endline "VERILOG PROGRAM: ";
+
+  let v = match Veriloggen.transf_program testinputprogram with
+  | Errors.OK v -> v
+  | Errors.Error _ ->
+     raise (Failure "Error") in
+  PrintVerilog.print_program stdout v
+
+let cvalue n = Value.natToValue (Nat.of_int 32) (Nat.of_int n)
+
+let test_values () =
+  print_endline "Testing values";
+  let v1 = cvalue 138 in
+  let v2 = cvalue 12 in
+  let v3 = Value.natToValue (Nat.of_int 16) (Nat.of_int 21) in
+  PrintVerilog.print_value stdout v1;
+  print_newline();
+  PrintVerilog.print_value stdout v2;
+  print_newline();
+  PrintVerilog.print_value stdout v3;
+  print_newline();
+  print_string "Addition: ";
+  PrintVerilog.print_value stdout (Value.vplus v1 v2);
+  print_newline();
+  print_string "Wrong addition: ";
+  PrintVerilog.print_value stdout (Value.vplus v1 v3);
+  print_newline();
+  print_string "Opt addition: ";
+  match Value.vplus_opt v1 v2 with
+  | Some x -> begin
+      PrintVerilog.print_value stdout x;
+      print_endline "";
+      match Value.vplus_opt v1 v3 with
+      | Some x -> PrintVerilog.print_value stdout x; print_newline()
+      | None -> print_endline "Correctly failed in addition"
+    end
+  | None -> raise (Failure "Error")
+
+let simulate_test () =
+  print_endline "Simulation test";
+  let v =
+    match Veriloggen.transf_program testinputprogram with
+    | Errors.OK v -> v
+    | _ -> raise (Failure "HLS Error") in
+  match Verilog.module_run (Nat.of_int 10) v with
+  | Errors.OK lst -> PrintVerilog.print_result stdout (PositiveMap.elements lst)
+  | _ -> raise (Failure "Simulation error")
+
+let () = test_function_transf ()
diff --git a/debug/dune b/debug/dune
new file mode 100644
index 0000000..7f0c6a6
--- /dev/null
+++ b/debug/dune
@@ -0,0 +1,5 @@
+(include_subdirs no)
+
+(executable
+ (name CoqupTest)
+ (libraries coqup))
diff --git a/default.nix b/default.nix
index 961bdec..cd37308 100644
--- a/default.nix
+++ b/default.nix
@@ -1,8 +1,8 @@
 with import <nixpkgs> {};
 
 let
-  ncoq = coq_8_10;
-  ncoqPackages = coqPackages_8_10;
+  ncoq = coq_8_11;
+  ncoqPackages = coqPackages_8_11;
   bbv = ncoqPackages.callPackage
     ( { coq, stdenv, fetchFromGitHub }:
       stdenv.mkDerivation {
diff --git a/example/main.v b/example/main.sv
index 63130fe..8e97a43 100644
--- a/example/main.v
+++ b/example/main.sv
@@ -1,6 +1,4 @@
-// -*- mode: verilog -*-
-
-module main(input start, reset, clk, 
+module main(input start, reset, clk,
             output finished, output [31:0] return_val);
 
    reg [31:0]      x;
diff --git a/lib/CompCert b/lib/CompCert
-Subproject e13469254ced9e4980ee54769d5b8b8729efc85
+Subproject 8f8250d076c9bcb15954c978dd1c351dd948326
diff --git a/src/Compiler.v b/src/Compiler.v
index 697732d..e998521 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq -*-
+(*
  * CoqUp: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
  *
diff --git a/src/Simulator.v b/src/Simulator.v
index 6849f80..930971b 100644
--- a/src/Simulator.v
+++ b/src/Simulator.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq -*-
+(*
  * CoqUp: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
diff --git a/src/common/Maps.v b/src/common/Maps.v
index 7a542b7..3236417 100644
--- a/src/common/Maps.v
+++ b/src/common/Maps.v
@@ -40,10 +40,4 @@ Definition traverse (A B : Type) (f : positive -> A -> res B) m := xtraverse f m
 
 Definition traverse1 (A B : Type) (f : A -> res B) := traverse (fun _ => f).
 
-Lemma traverse1_inversion:
-  forall (A B : Type) (f : A -> res B) (i j : positive) (m : t A) (m' : t B),
-    traverse1 f m = OK m' ->
-    list_forall2 (fun x y => f (snd x) = OK (snd y) /\ fst x = fst y) (elements m) (elements m').
-Proof. Admitted.
-
 End PTree.
diff --git a/src/common/Monad.v b/src/common/Monad.v
new file mode 100644
index 0000000..8517186
--- /dev/null
+++ b/src/common/Monad.v
@@ -0,0 +1,48 @@
+From Coq Require Import Lists.List.
+
+Module Type Monad.
+
+  Parameter mon : Type -> Type.
+
+  Parameter ret : forall (A : Type) (x : A), mon A.
+  Arguments ret [A].
+
+  Parameter bind : forall (A B : Type) (f : mon A) (g : A -> mon B), mon B.
+  Arguments bind [A B].
+
+  Parameter bind2 : forall (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C), mon C.
+  Arguments bind2 [A B C].
+
+End Monad.
+
+Module MonadExtra(M : Monad).
+  Import M.
+
+  Module MonadNotation.
+
+    Notation "'do' X <- A ; B" :=
+      (bind A (fun X => B))
+        (at level 200, X ident, A at level 100, B at level 200).
+    Notation "'do' ( X , Y ) <- A ; B" :=
+      (bind2 A (fun X Y => B))
+        (at level 200, X ident, Y ident, A at level 100, B at level 200).
+
+  End MonadNotation.
+  Import MonadNotation.
+
+  Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) :=
+    match l with
+    | nil => ret nil
+    | x::xs =>
+      do r <- f x;
+      do rs <- traverselist f xs;
+      ret (r::rs)
+    end.
+
+  Fixpoint collectlist {A : Type} (f : A -> mon unit) (l : list A) {struct l} : mon unit :=
+    match l with
+    | nil => ret tt
+    | x::xs => do _ <- f x; collectlist f xs
+    end.
+
+End MonadExtra.
diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v
new file mode 100644
index 0000000..ed1b9e7
--- /dev/null
+++ b/src/common/Statemonad.v
@@ -0,0 +1,61 @@
+From compcert Require Errors.
+From coqup Require Import Monad.
+From Coq Require Import Lists.List.
+
+Module Type State.
+  Parameter st : Type.
+  Parameter st_prop : st -> st -> Prop.
+
+  Axiom st_refl : forall s, st_prop s s.
+  Axiom st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
+End State.
+
+Module Statemonad(S : State) <: Monad.
+
+  Inductive res (A: Type) (s: S.st): Type :=
+  | Error : Errors.errmsg -> res A s
+  | OK : A -> forall (s' : S.st), S.st_prop s s' -> res A s.
+
+  Arguments OK [A s].
+  Arguments Error [A s].
+
+  Definition mon (A: Type) : Type := forall (s: S.st), res A s.
+
+  Definition ret {A: Type} (x: A) : mon A :=
+    fun (s : S.st) => OK x s (S.st_refl s).
+
+  Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B :=
+    fun (s : S.st) =>
+      match f s with
+      | Error msg => Error msg
+      | OK a s' i =>
+        match g a s' with
+        | Error msg => Error msg
+        | OK b s'' i' => OK b s'' (S.st_trans s s' s'' i i')
+        end
+      end.
+
+  Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
+    bind f (fun xy => g (fst xy) (snd xy)).
+
+  Definition handle_error {A: Type} (f g: mon A) : mon A :=
+    fun (s : S.st) =>
+      match f s with
+      | OK a s' i => OK a s' i
+      | Error _ => g s
+      end.
+
+  Definition error {A: Type} (err: Errors.errmsg) : mon A := fun (s: S.st) => Error err.
+
+  Definition get : mon S.st := fun s => OK s s (S.st_refl s).
+
+  Definition set (s: S.st) (i: forall s', S.st_prop  s' s) : mon unit :=
+    fun s' => OK tt s (i s').
+
+  Definition run_mon {A: Type} (s: S.st) (m: mon A): Errors.res A :=
+    match m s with
+    | OK a s' i => Errors.OK a
+    | Error err => Errors.Error err
+    end.
+
+End Statemonad.
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 319e2eb..0028fcb 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq -*-
+(*
  * CoqUp: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
  *
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index d7f88c1..4564237 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -16,171 +16,374 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From coqup Require Import HTL Coquplib.
-
 From compcert Require Import Maps.
 From compcert Require Errors.
 From compcert Require Import AST RTL.
+From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad.
+
+Hint Resolve AssocMap.gempty : htlh.
+Hint Resolve AssocMap.gso : htlh.
+Hint Resolve AssocMap.gss : htlh.
+Hint Resolve Ple_refl : htlh.
+Hint Resolve Ple_succ : htlh.
 
 Record state: Type := mkstate {
-  st_nextinst: positive;
-  st_instances: instances;
+  st_st : reg;
+  st_freshreg: reg;
+  st_freshstate: node;
+  st_datapath: datapath;
+  st_controllogic: controllogic;
 }.
 
-Inductive res (A: Type) (S: Type): Type :=
-  | Error: Errors.errmsg -> res A S
-  | OK: A -> S -> res A S.
+Definition init_state (st : reg) : state :=
+  mkstate st
+          1%positive
+          1%positive
+          (AssocMap.empty stmnt)
+          (AssocMap.empty stmnt).
+
+Module HTLState <: State.
+
+  Definition st := state.
+
+  Inductive st_incr: state -> state -> Prop :=
+    state_incr_intro:
+      forall (s1 s2: state),
+        st_st s1 = st_st s2 ->
+        Ple s1.(st_freshreg) s2.(st_freshreg) ->
+        Ple s1.(st_freshstate) s2.(st_freshstate) ->
+        (forall n,
+            s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) ->
+        (forall n,
+            s1.(st_controllogic)!n = None
+            \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) ->
+        st_incr s1 s2.
+  Hint Constructors st_incr : htlh.
+
+  Definition st_prop := st_incr.
+  Hint Unfold st_prop : htlh.
+
+  Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed.
+
+  Lemma st_trans :
+    forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
+  Proof.
+    intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans.
+    - rewrite H1. rewrite H. reflexivity.
+    - intros. destruct H4 with n.
+      + left; assumption.
+      + destruct H8 with n;
+          [ rewrite <- H0; left; assumption
+          | right; rewrite <- H0; apply H10
+          ].
+    - intros. destruct H5 with n.
+      + left; assumption.
+      + destruct H9 with n.
+        * rewrite <- H0. left. assumption.
+        * right. rewrite <- H0. apply H10.
+  Qed.
+
+End HTLState.
+Export HTLState.
 
-Arguments OK [A S].
-Arguments Error [A S].
+Module HTLMonad := Statemonad(HTLState).
+Export HTLMonad.
 
-Definition mon (A: Type) : Type := res A state.
+Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
+Import HTLMonadExtra.
+Export MonadNotation.
 
-Definition ret {A: Type} (x: A) (s: state) : mon A := OK x s.
+Definition state_goto (st : reg) (n : node) : stmnt :=
+  Vnonblock (Vvar st) (Vlit (posToValue 32 n)).
 
-Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B :=
-    match f with
-    | Error msg => Error msg
-    | OK a s => g a
+Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
+  Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)).
+
+Definition check_empty_node_datapath:
+  forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }.
+Proof.
+  intros. case (s.(st_datapath)!n); intros. right; auto. left; auto.
+Defined.
+
+Definition check_empty_node_controllogic:
+  forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }.
+Proof.
+  intros. case (s.(st_controllogic)!n); intros. right; auto. left; auto.
+Defined.
+
+Lemma add_instr_state_incr :
+  forall s n n' st,
+    (st_datapath s)!n = None ->
+    (st_controllogic s)!n = None ->
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       (AssocMap.set n st s.(st_datapath))
+       (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
+Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
+  fun s =>
+    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+    | left STM, left TRANS =>
+      OK tt (mkstate
+               s.(st_st)
+               s.(st_freshreg)
+               (st_freshstate s)
+               (AssocMap.set n st s.(st_datapath))
+               (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic)))
+         (add_instr_state_incr s n n' st STM TRANS)
+    | _, _ => Error (Errors.msg "HTL.add_instr")
     end.
 
-Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
-  bind f (fun xy => g (fst xy) (snd xy)).
+Lemma add_instr_skip_state_incr :
+  forall s n st,
+    (st_datapath s)!n = None ->
+    (st_controllogic s)!n = None ->
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       (AssocMap.set n st s.(st_datapath))
+       (AssocMap.set n Vskip s.(st_controllogic))).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
+Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
+  fun s =>
+    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+    | left STM, left TRANS =>
+      OK tt (mkstate
+               s.(st_st)
+               s.(st_freshreg)
+               (st_freshstate s)
+               (AssocMap.set n st s.(st_datapath))
+               (AssocMap.set n Vskip s.(st_controllogic)))
+         (add_instr_skip_state_incr s n st STM TRANS)
+    | _, _ => Error (Errors.msg "HTL.add_instr")
+    end.
+
+Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
+Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
+
+Definition bop (op : binop) (r1 r2 : reg) : expr :=
+  Vbinop op (Vvar r1) (Vvar r2).
+
+Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=
+  Vbinop op (Vvar r) (Vlit (intToValue l)).
 
-Definition bindS {A B: Type} (f: mon A) (g: A -> state -> mon B) : mon B :=
-  match f with
-  | Error msg => Error msg
-  | OK a s => g a s
+Definition boplitz (op: binop) (r: reg) (l: Z) : expr :=
+  Vbinop op (Vvar r) (Vlit (ZToValue 32%nat l)).
+
+Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr :=
+  match c, args with
+  | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2)
+  | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2)
+  | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2)
+  | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2)
+  | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2)
+  | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2)
+  | _, _ => error (Errors.msg "Veriloggen: comparison instruction not implemented: other")
   end.
 
-Notation "'do' X <- A ; B" := (bind A (fun X => B))
-   (at level 200, X ident, A at level 100, B at level 200).
-Notation "'do' ( X , Y ) <- A ; B" := (bindS A (fun X Y => B))
-   (at level 200, X ident, Y ident, A at level 100, B at level 200).
+Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int)
+  : mon expr :=
+  match c, args with
+  | Integers.Ceq, r1::nil => ret (boplit Veq r1 i)
+  | Integers.Cne, r1::nil => ret (boplit Vne r1 i)
+  | Integers.Clt, r1::nil => ret (boplit Vlt r1 i)
+  | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i)
+  | Integers.Cle, r1::nil => ret (boplit Vle r1 i)
+  | Integers.Cge, r1::nil => ret (boplit Vge r1 i)
+  | _, _ => error (Errors.msg "Veriloggen: comparison_imm instruction not implemented: other")
+  end.
 
-Definition handle_error {A: Type} (f g: mon A) : mon A :=
-  match f with
-  | OK a s' => OK a s'
-  | Error _ => g
+Definition translate_condition (c : Op.condition) (args : list reg) : mon expr :=
+  match c, args with
+  | Op.Ccomp c, _ => translate_comparison c args
+  | Op.Ccompu c, _ => translate_comparison c args
+  | Op.Ccompimm c i, _ => translate_comparison_imm c args i
+  | Op.Ccompuimm c i, _ => translate_comparison_imm c args i
+  | Op.Cmaskzero n, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: Cmaskzero")
+  | Op.Cmasknotzero n, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: Cmasknotzero")
+  | _, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: other")
   end.
 
-Definition init_state : state :=
-  mkstate 1%positive empty_instances.
-
-Module PTree.
-  Export Maps.PTree.
-
-  Fixpoint xtraverse {A B : Type} (f : positive -> A -> state -> mon B)
-           (m : PTree.t A) (s : state) (i : positive)
-           {struct m} : mon (PTree.t B) :=
-    match m with
-    | Leaf => OK Leaf s
-    | Node l o r =>
-      let newo :=
-          match o with
-          | None => OK None s
-          | Some x =>
-            match f (prev i) x s with
-            | Error err => Error err
-            | OK val s' => OK (Some val) s'
-            end
-          end in
-      match newo with
-      | OK no s =>
-        do (nl, s') <- xtraverse f l s (xO i);
-        do (nr, s'') <- xtraverse f r s' (xI i);
-        OK (Node nl no nr) s''
-      | Error msg => Error msg
-      end
+Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=
+  match a, args with
+  | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off)
+  | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off))
+  | Op.Ascaled scale offset, r1::nil =>
+    ret (Vbinop Vadd (boplitz Vadd r1 scale) (Vlit (ZToValue 32%nat offset)))
+  | Op.Aindexed2scaled scale offset, r1::r2::nil =>
+    ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
+  | _, _ => error (Errors.msg "Veriloggen: eff_addressing instruction not implemented: other")
+  end.
+
+(** Translate an instruction to a statement. *)
+Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
+  match op, args with
+  | Op.Omove, r::nil => ret (Vvar r)
+  | Op.Ointconst n, _ => ret (Vlit (intToValue n))
+  | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r))
+  | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2)
+  | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2)
+  | Op.Omulimm n, r::nil => ret (boplit Vmul r n)
+  | Op.Omulhs, _ => error (Errors.msg "Veriloggen: Instruction not implemented: Omulhs")
+  | Op.Omulhu, _ => error (Errors.msg "Veriloggen: Instruction not implemented: Omulhu")
+  | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2)
+  | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2)
+  | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2)
+  | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2)
+  | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2)
+  | Op.Oandimm n, r::nil => ret (boplit Vand r n)
+  | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2)
+  | Op.Oorimm n, r::nil => ret (boplit Vor r n)
+  | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2)
+  | Op.Oxorimm n, r::nil => ret (boplit Vxor r n)
+  | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r))
+  | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2)
+  | Op.Oshlimm n, r::nil => ret (boplit Vshl r n)
+  | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2)
+  | Op.Oshrimm n, r::nil => ret (boplit Vshr r n)
+  | Op.Oshrximm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshrximm")
+  | Op.Oshru, r1::r2::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshru")
+  | Op.Oshruimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshruimm")
+  | Op.Ororimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Ororimm")
+  | Op.Oshldimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshldimm")
+  | Op.Ocmp c, _ => translate_condition c args
+  | Op.Olea a, _ => translate_eff_addressing a args
+  | _, _ => error (Errors.msg "Veriloggen: Instruction not implemented: other")
+  end.
+
+Lemma add_branch_instr_state_incr:
+  forall s e n n1 n2,
+    (st_datapath s) ! n = None ->
+    (st_controllogic s) ! n = None ->
+    st_incr s (mkstate
+                 s.(st_st)
+                (st_freshreg s)
+                (st_freshstate s)
+                (AssocMap.set n Vskip (st_datapath s))
+                (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
+Proof.
+  intros. apply state_incr_intro; simpl;
+            try (intros; destruct (peq n0 n); subst);
+            auto with htlh.
+Qed.
+
+Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
+  fun s =>
+    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+    | left NSTM, left NTRANS =>
+      OK tt (mkstate
+               s.(st_st)
+                (st_freshreg s)
+                (st_freshstate s)
+                (AssocMap.set n Vskip (st_datapath s))
+                (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
+         (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS)
+    | _, _ => Error (Errors.msg "Veriloggen: add_branch_instr")
     end.
 
-  Definition traverse {A B : Type} (f : positive -> A -> state -> mon B) m :=
-    xtraverse f m init_state xH.
-
-  Definition traverse1 {A B : Type} (f : A -> state -> mon B) := traverse (fun _ => f).
-
-End PTree.
-
-Definition transf_instr (pc: node) (rtl: RTL.instruction) (s: state)
-  : mon HTL.instruction :=
-  match rtl with
-  | RTL.Inop n =>
-    (** Nop instruction should just become a Skip in Verilog, which is just a
-        semicolon. *)
-    ret (HTL.Hnop n) s
-  | RTL.Iop op args res n =>
-    (** Perform an arithmetic operation over registers.  This will just become
-        one binary operation in Verilog.  This will contain a list of registers,
-        so these will just become a chain of binary operations in Verilog. *)
-    ret (HTL.Hnonblock op args res n) s
-  | RTL.Iload chunk addr args dst n =>
-    (** Load from memory, which will maybe become a load from RAM, however, I'm
-        not sure yet how memory will be implemented or how it will formalised
-        be. *)
-    ret (HTL.Hload chunk addr args dst n) s
-  | RTL.Istore chunk addr args src n =>
-    (** How memory will be laid out will also affect how stores are handled.  For
-        now hopefully these can be ignored, and hopefull they are not used that
-        often when they are not required in C. *)
-    ret (HTL.Hstore chunk addr args src n) s
-  | RTL.Icall sig ros args res n =>
-    (** Function call should become a module instantiation with start and end
-        signals appropriately wired up. *)
-    match ros with
-    | inr i =>
-      let inst := mkinst i args in
-      let newinstances := PTree.set s.(st_nextinst) inst s.(st_instances) in
-      ret (HTL.Hinst sig i res n)
-          (mkstate ((s.(st_nextinst) + 1)%positive)
-                   newinstances)
-    | _ => Error (Errors.msg "Function pointers are not supported.")
-    end
-  | RTL.Itailcall sig ros args =>
-    (** Should be converted into a reset of the modules state, setting the
-        initial variables correctly.  This would simulate a tailcall as it is
-        similar to jumping back to the top of the function in assembly. *)
-    match ros with
-    | inr i => ret (HTL.Htailcall sig i args) s
-    | _ => Error (Errors.msg "Function pointers are not supported.")
+Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit :=
+  match ni with
+    (n, i) =>
+    match i with
+    | Inop n' => add_instr n n' Vskip
+    | Iop op args dst n' =>
+      do instr <- translate_instr op args;
+      add_instr n n' (nonblock dst instr)
+    | Iload _ _ _ _ _ => error (Errors.msg "Loads are not implemented.")
+    | Istore _ _ _ _ _ => error (Errors.msg "Stores are not implemented.")
+    | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
+    | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
+    | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
+    | Icond cond args n1 n2 =>
+      do e <- translate_condition cond args;
+      add_branch_instr e n n1 n2
+    | Ijumptable _ _ => error (Errors.msg "Jumptable not implemented")
+    | Ireturn r =>
+      match r with
+      | Some r' =>
+        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r')))
+      | None =>
+        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z))))
+      end
     end
-  | RTL.Ibuiltin ef args res n =>
-    (** Builtin functions will have to supported manually, by implementing the
-        Verilog myself. *)
-    Error (Errors.msg "builtin functions are not supported.")
-  | RTL.Icond cond args n1 n2 =>
-    (** Will be converted into two separate processes that are combined by a mux
-        at the end, with a start flag that propagates in the construct that should
-        be chosen. *)
-    ret (HTL.Hcond cond args n1 n2) s
-  | RTL.Ijumptable arg tbl =>
-    (** A jump to a specific instruction in the list, this will require setting
-        the state in the state machine appropriately.  This is trivial to
-        implement if no scheduling is involved, but as soon as that isn't the
-        case it might be difficult to find that location.  It would help to
-        transform the CFG to a few basic blocks first which cannot have any
-        branching. *)
-    ret (HTL.Hjumptable arg tbl) s
-  | RTL.Ireturn r =>
-    (** The return value of the function, which will just mean that the finished
-        signal goes high and the result is stored in the result register. *)
-    ret (HTL.Hfinish r) s
   end.
 
-Definition transf_function (f: function) : Errors.res module :=
-  match (PTree.traverse transf_instr f.(fn_code)) with
-  | OK code s =>
-    Errors.OK (mkmodule
-          f.(fn_sig)
-          f.(fn_params)
-          f.(fn_stacksize)
-          code
-          s.(st_instances)
-          f.(fn_entrypoint))
-  | Error err => Errors.Error err
-  end.
+Lemma create_reg_state_incr:
+  forall s,
+    st_incr s (mkstate
+         s.(st_st)
+         (Pos.succ (st_freshreg s))
+         (st_freshstate s)
+         (st_datapath s)
+         (st_controllogic s)).
+Proof. constructor; simpl; auto with htlh. Qed.
+
+Definition create_reg: mon reg :=
+  fun s => let r := s.(st_freshreg) in
+           OK r (mkstate
+                   s.(st_st)
+                   (Pos.succ r)
+                   (st_freshstate s)
+                   (st_datapath s)
+                   (st_controllogic s))
+              (create_reg_state_incr s).
+
+Definition transf_module (f: function) : mon module :=
+  do fin <- create_reg;
+  do rtrn <- create_reg;
+  do _ <- collectlist (transf_instr fin rtrn) (Maps.PTree.elements f.(RTL.fn_code));
+  do start <- create_reg;
+  do rst <- create_reg;
+  do clk <- create_reg;
+  do current_state <- get;
+  ret (mkmodule
+         f.(RTL.fn_params)
+         current_state.(st_datapath)
+         current_state.(st_controllogic)
+         f.(fn_entrypoint)
+         current_state.(st_st)
+         fin
+         rtrn).
 
-Definition transf_fundef (fd: fundef) : Errors.res moddecl :=
-  transf_partial_fundef transf_function fd.
+Definition max_state (f: function) : state :=
+  let st := Pos.succ (max_reg_function f) in
+  mkstate st
+          (Pos.succ st)
+          (Pos.succ (max_pc_function f))
+          (st_datapath (init_state st))
+          (st_controllogic (init_state st)).
 
-Definition transf_program (p: program) : Errors.res design :=
-  transform_partial_program transf_fundef p.
+Definition transl_module (f : function) : Errors.res module :=
+  run_mon (max_state f) (transf_module f).
+
+Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit))
+{struct flist} : option function :=
+  match flist with
+  | (i, AST.Gfun (AST.Internal f)) :: xs =>
+    if Pos.eqb i main
+    then Some f
+    else main_function main xs
+  | _ :: xs => main_function main xs
+  | nil => None
+  end.
+
+Definition transf_program (d : program) : Errors.res module :=
+  match main_function d.(AST.prog_main) d.(AST.prog_defs) with
+  | Some f => transl_module f
+  | _ => Errors.Error (Errors.msg "HTL: could not find main function")
+  end.
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
new file mode 100644
index 0000000..2d2129c
--- /dev/null
+++ b/src/translation/HTLgenproof.v
@@ -0,0 +1,396 @@
+(*
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap.
+From coqup Require HTL Verilog.
+From compcert Require RTL Registers Globalenvs AST.
+
+Import AssocMapNotation.
+
+Hint Resolve Smallstep.forward_simulation_plus : htlproof.
+Hint Resolve AssocMap.gss : htlproof.
+Hint Resolve AssocMap.gso : htlproof.
+
+Hint Unfold find_assocmap AssocMapExt.get_default : htlproof.
+
+Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop :=
+  match_assocmap : forall f rs am,
+    (forall r, Ple r (RTL.max_reg_function f) ->
+               val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
+    match_assocmaps f rs am.
+Hint Constructors match_assocmaps : htlproof.
+
+Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
+  forall st assoc,
+  s = HTL.State m st assoc ->
+  assoc!(m.(HTL.mod_st)) = Some (posToValue 32 st).
+Hint Unfold state_st_wf : htlproof.
+
+Inductive match_states : RTL.state -> HTL.state -> Prop :=
+| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st
+    (MASSOC : match_assocmaps f rs assoc)
+    (TF : tr_module f m)
+    (WF : state_st_wf m (HTL.State m st assoc)),
+    match_states (RTL.State sf f sp st rs mem)
+                 (HTL.State m st assoc)
+| match_returnstate : forall v v' stack m,
+    val_value_lessdef v v' ->
+    match_states (RTL.Returnstate stack v m) (HTL.Returnstate v').
+Hint Constructors match_states : htlproof.
+
+Inductive match_program : RTL.program -> HTL.module -> Prop :=
+  match_program_intro :
+    forall ge p b m f,
+    ge = Globalenvs.Genv.globalenv p ->
+    Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
+    Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal f) ->
+    tr_module f m ->
+    match_program p m.
+Hint Constructors match_program : htlproof.
+
+Lemma regs_lessdef_add_greater :
+  forall f rs1 rs2 n v,
+    Plt (RTL.max_reg_function f) n ->
+    match_assocmaps f rs1 rs2 ->
+    match_assocmaps f rs1 (AssocMap.set n v rs2).
+Proof.
+  inversion 2; subst.
+  intros. constructor.
+  intros. unfold find_assocmap. unfold AssocMapExt.get_default.
+  rewrite AssocMap.gso. eauto.
+  apply Pos.le_lt_trans with _ _ n in H2.
+  unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption.
+Qed.
+Hint Resolve regs_lessdef_add_greater : htlproof.
+
+Lemma regs_lessdef_add_match :
+  forall f rs am r v v',
+    val_value_lessdef v v' ->
+    match_assocmaps f rs am ->
+    match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am).
+Proof.
+  inversion 2; subst.
+  constructor. intros.
+  destruct (peq r0 r); subst.
+  rewrite Registers.Regmap.gss.
+  unfold find_assocmap. unfold AssocMapExt.get_default.
+  rewrite AssocMap.gss. assumption.
+
+  rewrite Registers.Regmap.gso; try assumption.
+  unfold find_assocmap. unfold AssocMapExt.get_default.
+  rewrite AssocMap.gso; eauto.
+Qed.
+Hint Resolve regs_lessdef_add_match : htlproof.
+
+Lemma valToValue_lessdef :
+  forall v v',
+    valToValue v = Some v' <->
+    val_value_lessdef v v'.
+Proof.
+  split; intros.
+  destruct v; try discriminate; constructor.
+  unfold valToValue in H. inversion H.
+  Admitted.
+
+(* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
+Lemma assumption_32bit :
+  forall v,
+    valueToPos (posToValue 32 v) = v.
+Admitted.
+
+Lemma assumption_32bit_bool :
+  forall b,
+    valueToBool (boolToValue 32 b) = b.
+Admitted.
+
+Lemma st_greater_than_res :
+  forall m res : positive,
+    m <> res.
+Admitted.
+
+Lemma finish_not_return :
+  forall r f : positive,
+    r <> f.
+Admitted.
+
+Lemma finish_not_res :
+  forall f r : positive,
+    f <> r.
+Admitted.
+
+Ltac inv_state :=
+  match goal with
+    MSTATE : match_states _ _ |- _ =>
+    inversion MSTATE;
+    match goal with
+      TF : tr_module _ _ |- _ =>
+      inversion TF;
+      match goal with
+        TC : forall _ _,
+          Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _,
+        H : Maps.PTree.get _ _ = Some _ |- _ =>
+        apply TC in H; inversion H;
+        match goal with
+          TI : tr_instr _ _ _ _ _ _ |- _ =>
+          inversion TI
+        end
+      end
+    end
+  end; subst.
+
+Section CORRECTNESS.
+
+  Variable prog : RTL.program.
+  Variable tprog : HTL.module.
+
+  Hypothesis TRANSL : match_program prog tprog.
+
+  Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
+  Let tge : HTL.genv := HTL.genv_empty.
+
+  Lemma eval_correct :
+    forall sp op rs args m v v' e assoc f,
+      Op.eval_operation ge sp op
+(List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
+      tr_op op args e ->
+      valToValue v = Some v' ->
+      Verilog.expr_runp f assoc e v'.
+  Admitted.
+
+  Lemma eval_cond_correct :
+    forall cond (args : list Registers.reg) s1 c s' i rs args m b f assoc,
+    translate_condition cond args s1 = OK c s' i ->
+    Op.eval_condition cond (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some b ->
+    Verilog.expr_runp f assoc c (boolToValue 32 b).
+  Admitted.
+
+  (** The proof of semantic preservation for the translation of instructions
+      is a simulation argument based on diagrams of the following form:
+<<
+                      match_states
+    code st rs ---------------- State m st assoc
+         ||                             |
+         ||                             |
+         ||                             |
+         \/                             v
+    code st rs' --------------- State m st assoc'
+                      match_states
+>>
+      where [tr_code c data control fin rtrn st] is assumed to hold.
+
+      The precondition and postcondition is that that should hold is [match_assocmaps rs assoc].
+   *)
+
+  Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
+    forall m assoc fin rtrn st stmt trans,
+      tr_instr fin rtrn st instr stmt trans ->
+      exists assoc',
+        HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc').
+
+  Lemma greater_than_max_func :
+    forall f st,
+      Plt (RTL.max_reg_function f) st.
+  Proof. Admitted.
+
+  Theorem transl_step_correct:
+    forall (S1 : RTL.state) t S2,
+      RTL.step ge S1 t S2 ->
+      forall (R1 : HTL.state),
+        match_states S1 R1 ->
+        exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2.
+  Proof.
+    induction 1; intros R1 MSTATE; try inv_state.
+    - (* Inop *)
+      econstructor.
+      split.
+      apply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      (* processing of state *)
+      econstructor.
+      simpl. trivial.
+      econstructor. trivial.
+      econstructor.
+
+      (* prove stval *)
+      unfold_merge. simpl. apply AssocMap.gss.
+
+      (* prove match_state *)
+      rewrite assumption_32bit.
+      constructor; auto.
+      unfold_merge. simpl. apply regs_lessdef_regs. apply greater_than_max_func.
+      assumption.
+      unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss.
+    - (* Iop *)
+      econstructor.
+      split.
+      apply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      econstructor; simpl; trivial.
+      constructor; trivial.
+      econstructor; simpl; eauto.
+      eapply eval_correct; eauto.
+      unfold_merge. simpl.
+      rewrite AssocMap.gso.
+      apply AssocMap.gss.
+      apply st_greater_than_res.
+      trivial.
+
+      (* match_states *)
+      assert (pc' = valueToPos (posToValue 32 pc')). symmetry. apply assumption_32bit.
+      rewrite <- H1.
+      constructor. apply rs0.
+      unfold_merge.
+      apply regs_add_match.
+      apply regs_lessdef_regs.
+      assumption.
+      apply valToValue_lessdef.
+      assumption.
+
+      unfold state_st_wf. intros. inversion H2. subst.
+      unfold_merge.
+      rewrite AssocMap.gso.
+      apply AssocMap.gss.
+      apply st_greater_than_res.
+    - econstructor. split. apply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      eapply Verilog.stmnt_runp_Vnonblock with
+          (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
+      simpl. trivial.
+      destruct b.
+      eapply Verilog.erun_Vternary_true.
+      eapply eval_cond_correct; eauto.
+      constructor.
+      apply assumption_32bit_bool.
+      eapply Verilog.erun_Vternary_false.
+      eapply eval_cond_correct; eauto.
+      constructor.
+      apply assumption_32bit_bool.
+      trivial.
+      constructor.
+      trivial.
+      unfold_merge.
+      apply AssocMap.gss.
+      trivial.
+
+      destruct b.
+      rewrite assumption_32bit.
+      apply match_state. apply rs0.
+      unfold_merge.
+      apply regs_lessdef_regs. assumption.
+      assumption.
+
+      unfold state_st_wf. intros. inversion H1.
+      subst. unfold_merge.
+      apply AssocMap.gss.
+      rewrite assumption_32bit.
+      apply match_state. apply rs0.
+      unfold_merge.
+      apply regs_lessdef_regs. assumption.
+      assumption.
+
+      unfold state_st_wf. intros. inversion H1.
+      subst. unfold_merge.
+      apply AssocMap.gss.
+
+    - (* Return *)
+      econstructor. split.
+      eapply Smallstep.plus_two.
+      
+      eapply HTL.step_module; eauto.
+      constructor.
+      econstructor; simpl; trivial.
+      econstructor; simpl; trivial.
+      constructor.
+      econstructor; simpl; trivial.
+      constructor.
+      unfold_merge.
+      trivial.
+      rewrite AssocMap.gso.
+      rewrite AssocMap.gso.
+      unfold state_st_wf in WF. apply WF. trivial.
+      apply st_greater_than_res. apply st_greater_than_res. trivial.
+
+      apply HTL.step_finish.
+      unfold_merge; simpl.
+      rewrite AssocMap.gso.
+      apply AssocMap.gss.
+      apply finish_not_return.
+      apply AssocMap.gss.
+      rewrite Events.E0_left. trivial.
+
+      constructor. constructor.
+    - destruct (assoc!r) eqn:?.
+      inversion H11. subst.
+      econstructor. split.
+      eapply Smallstep.plus_two.
+      eapply HTL.step_module; eauto.
+      constructor.
+      econstructor; simpl; trivial.
+      econstructor; simpl; trivial.
+      constructor.
+      econstructor; simpl; trivial.
+      apply Verilog.erun_Vvar.
+      rewrite AssocMap.gso.
+      apply Heqo. apply not_eq_sym. apply finish_not_res.
+      unfold_merge.
+      trivial.
+      rewrite AssocMap.gso.
+      rewrite AssocMap.gso.
+      unfold state_st_wf in WF. apply WF. trivial.
+      apply st_greater_than_res. apply st_greater_than_res. trivial.
+
+      apply HTL.step_finish.
+      unfold_merge.
+      rewrite AssocMap.gso.
+      apply AssocMap.gss.
+      apply finish_not_return.
+      apply AssocMap.gss.
+      rewrite Events.E0_left. trivial.
+
+      constructor. simpl.
+      Admitted.
+  Hint Resolve transl_step_correct : htlproof.
+
+  Lemma senv_preserved :
+    forall id : AST.ident,
+      Globalenvs.Senv.public_symbol (Smallstep.symbolenv (HTL.semantics tprog)) id =
+      Globalenvs.Senv.public_symbol (Smallstep.symbolenv (RTL.semantics prog)) id.
+  Proof. Admitted.
+  Hint Resolve senv_preserved : htlproof.
+
+  Lemma transl_initial_states :
+    forall s1 : Smallstep.state (RTL.semantics prog),
+      Smallstep.initial_state (RTL.semantics prog) s1 ->
+      exists s2 : Smallstep.state (HTL.semantics tprog),
+        Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2.
+  Proof. Admitted.
+  Hint Resolve transl_initial_states : htlproof.
+
+  Lemma transl_final_states :
+    forall (s1 : Smallstep.state (RTL.semantics prog)) (s2 : Smallstep.state (HTL.semantics tprog))
+           (r : Integers.Int.int),
+      match_states s1 s2 ->
+      Smallstep.final_state (RTL.semantics prog) s1 r -> Smallstep.final_state (HTL.semantics tprog) s2 r.
+  Proof. Admitted.
+  Hint Resolve transl_final_states : htlproof.
+
+  Theorem transf_program_correct:
+    Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog).
+  Proof. eauto with htlproof. Qed.
+
+End CORRECTNESS.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
new file mode 100644
index 0000000..713a373
--- /dev/null
+++ b/src/translation/HTLgenspec.v
@@ -0,0 +1,359 @@
+(*
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+From compcert Require RTL Op Maps Errors.
+From compcert Require Import Maps.
+From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap.
+
+Hint Resolve Maps.PTree.elements_keys_norepet : htlspec.
+Hint Resolve Maps.PTree.elements_correct : htlspec.
+
+Remark bind_inversion:
+  forall (A B: Type) (f: mon A) (g: A -> mon B)
+         (y: B) (s1 s3: st) (i: st_incr s1 s3),
+    bind f g s1 = OK y s3 i ->
+    exists x, exists s2, exists i1, exists i2,
+            f s1 = OK x s2 i1 /\ g x s2 = OK y s3 i2.
+Proof.
+  intros until i. unfold bind. destruct (f s1); intros.
+  discriminate.
+  exists a; exists s'; exists s.
+  destruct (g a s'); inv H.
+  exists s0; auto.
+Qed.
+
+Remark bind2_inversion:
+  forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C)
+         (z: C) (s1 s3: st) (i: st_incr s1 s3),
+    bind2 f g s1 = OK z s3 i ->
+    exists x, exists y, exists s2, exists i1, exists i2,
+              f s1 = OK (x, y) s2 i1 /\ g x y s2 = OK z s3 i2.
+Proof.
+  unfold bind2; intros.
+  exploit bind_inversion; eauto.
+  intros [[x y] [s2 [i1 [i2 [P Q]]]]]. simpl in Q.
+  exists x; exists y; exists s2; exists i1; exists i2; auto.
+Qed.
+
+Ltac monadInv1 H :=
+  match type of H with
+  | (OK _ _ _ = OK _ _ _) =>
+    inversion H; clear H; try subst
+  | (Error _ _ = OK _ _ _) =>
+    discriminate
+  | (ret _ _ = OK _ _ _) =>
+    inversion H; clear H; try subst
+  | (error _ _ = OK _ _ _) =>
+    discriminate
+  | (bind ?F ?G ?S = OK ?X ?S' ?I) =>
+    let x := fresh "x" in (
+      let s := fresh "s" in (
+        let i1 := fresh "INCR" in (
+          let i2 := fresh "INCR" in (
+            let EQ1 := fresh "EQ" in (
+              let EQ2 := fresh "EQ" in (
+                destruct (bind_inversion _ _ F G X S S' I H) as [x [s [i1 [i2 [EQ1 EQ2]]]]];
+                clear H;
+                try (monadInv1 EQ2)))))))
+  | (bind2 ?F ?G ?S = OK ?X ?S' ?I) =>
+    let x1 := fresh "x" in (
+      let x2 := fresh "x" in (
+        let s := fresh "s" in (
+          let i1 := fresh "INCR" in (
+            let i2 := fresh "INCR" in (
+              let EQ1 := fresh "EQ" in (
+                let EQ2 := fresh "EQ" in (
+                  destruct (bind2_inversion _ _ _ F G X S S' I H) as [x1 [x2 [s [i1 [i2 [EQ1 EQ2]]]]]];
+                  clear H;
+                  try (monadInv1 EQ2))))))))
+  end.
+
+Ltac monadInv H :=
+  match type of H with
+  | (ret _ _ = OK _ _ _) => monadInv1 H
+  | (error _ _ = OK _ _ _) => monadInv1 H
+  | (bind ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H
+  | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H
+  | (?F _ _ _ _ _ _ _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ _ _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  end.
+
+(** * Relational specification of the translation *)
+
+(** We now define inductive predicates that characterise the fact that the
+statemachine that is created by the translation contains the correct
+translations for each of the elements *)
+
+Inductive tr_op : Op.operation -> list reg -> expr -> Prop :=
+| tr_op_Omove : forall r, tr_op Op.Omove (r::nil) (Vvar r)
+| tr_op_Ointconst : forall n l, tr_op (Op.Ointconst n) l (Vlit (intToValue n))
+| tr_op_Oneg : forall r, tr_op Op.Oneg (r::nil) (Vunop Vneg (Vvar r))
+| tr_op_Osub : forall r1 r2, tr_op Op.Osub (r1::r2::nil) (bop Vsub r1 r2)
+| tr_op_Omul : forall r1 r2, tr_op Op.Omul (r1::r2::nil) (bop Vmul r1 r2)
+| tr_op_Omulimm : forall r n, tr_op (Op.Omulimm n) (r::nil) (boplit Vmul r n)
+| tr_op_Odiv : forall r1 r2, tr_op Op.Odiv (r1::r2::nil) (bop Vdiv r1 r2)
+| tr_op_Odivu : forall r1 r2, tr_op Op.Odivu (r1::r2::nil) (bop Vdivu r1 r2)
+| tr_op_Omod : forall r1 r2, tr_op Op.Omod (r1::r2::nil) (bop Vmod r1 r2)
+| tr_op_Omodu : forall r1 r2, tr_op Op.Omodu (r1::r2::nil) (bop Vmodu r1 r2)
+| tr_op_Oand : forall r1 r2, tr_op Op.Oand (r1::r2::nil) (bop Vand r1 r2)
+| tr_op_Oandimm : forall n r, tr_op (Op.Oandimm n) (r::nil) (boplit Vand r n)
+| tr_op_Oor : forall r1 r2, tr_op Op.Oor (r1::r2::nil) (bop Vor r1 r2)
+| tr_op_Oorimm : forall n r, tr_op (Op.Oorimm n) (r::nil) (boplit Vor r n)
+| tr_op_Oxor : forall r1 r2, tr_op Op.Oxor (r1::r2::nil) (bop Vxor r1 r2)
+| tr_op_Oxorimm : forall n r, tr_op (Op.Oxorimm n) (r::nil) (boplit Vxor r n)
+| tr_op_Onot : forall r, tr_op Op.Onot (r::nil) (Vunop Vnot (Vvar r))
+| tr_op_Oshl : forall r1 r2, tr_op Op.Oshl (r1::r2::nil) (bop Vshl r1 r2)
+| tr_op_Oshlimm : forall n r, tr_op (Op.Oshlimm n) (r::nil) (boplit Vshl r n)
+| tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2)
+| tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n)
+| tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e
+| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e.
+Hint Constructors tr_op : htlspec.
+
+Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
+| tr_instr_Inop :
+    forall n,
+      tr_instr fin rtrn st (RTL.Inop n) Vskip (state_goto st n)
+| tr_instr_Iop :
+    forall n op args e dst,
+      tr_op op args e ->
+      tr_instr fin rtrn st (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
+| tr_instr_Icond :
+    forall n1 n2 cond args s s' i c,
+      translate_condition cond args s = OK c s' i ->
+      tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
+| tr_instr_Ireturn_None :
+    tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)))
+                                                  (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip
+| tr_instr_Ireturn_Some :
+    forall r,
+      tr_instr fin rtrn st (RTL.Ireturn (Some r))
+               (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
+Hint Constructors tr_instr : htlspec.
+
+Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
+          (fin rtrn st : reg) : Prop :=
+  tr_code_intro :
+    forall s t,
+      stmnts!pc = Some s ->
+      trans!pc = Some t ->
+      tr_instr fin rtrn st i s t ->
+      tr_code pc i stmnts trans fin rtrn st.
+Hint Constructors tr_code : htlspec.
+
+Inductive tr_module (f : RTL.function) : module -> Prop :=
+  tr_module_intro :
+    forall data control fin rtrn st m,
+      (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
+                    tr_code pc i data control fin rtrn st) ->
+      m = (mkmodule f.(RTL.fn_params)
+                        data
+                        control
+                        f.(RTL.fn_entrypoint)
+                            st fin rtrn) ->
+      tr_module f m.
+Hint Constructors tr_module : htlspec.
+
+Lemma create_reg_datapath_trans :
+  forall s s' x i,
+    create_reg s = OK x s' i ->
+    s.(st_datapath) = s'.(st_datapath).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_reg_datapath_trans : htlspec.
+
+Lemma create_reg_controllogic_trans :
+  forall s s' x i,
+    create_reg s = OK x s' i ->
+    s.(st_controllogic) = s'.(st_controllogic).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_reg_controllogic_trans : htlspec.
+
+Lemma get_refl_x :
+  forall s s' x i,
+    get s = OK x s' i ->
+    s = x.
+Proof. inversion 1. trivial. Qed.
+Hint Resolve get_refl_x : htlspec.
+
+Lemma get_refl_s :
+  forall s s' x i,
+    get s = OK x s' i ->
+    s = s'.
+Proof. inversion 1. trivial. Qed.
+Hint Resolve get_refl_s : htlspec.
+
+Ltac inv_incr :=
+  repeat match goal with
+  | [ H: create_reg ?s = OK _ ?s' _ |- _ ] =>
+    let H1 := fresh "H" in
+    assert (H1 := H); eapply create_reg_datapath_trans in H;
+    eapply create_reg_controllogic_trans in H1
+  | [ H: get ?s = OK _ _ _ |- _ ] =>
+    let H1 := fresh "H" in
+    assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1;
+    subst
+  | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H
+  | [ H: st_incr _ _ |- _ ] => destruct st_incr
+  end.
+
+Ltac rewrite_states :=
+  match goal with
+  | [ H: ?x ?s = ?x ?s' |- _ ] =>
+    let c1 := fresh "c" in
+    let c2 := fresh "c" in
+    remember (?x ?s) as c1; remember (?x ?s') as c2; try subst
+  end.
+
+Lemma translate_instr_tr_op :
+  forall op args s s' e i,
+    translate_instr op args s = OK e s' i ->
+    tr_op op args e.
+Proof.
+  intros.
+  destruct op eqn:?; eauto with htlspec; try discriminate; simpl in *;
+    try (match goal with
+           [ H: match ?args with _ => _ end _ = _ _ _ |- _ ] =>
+           repeat (destruct args; try discriminate)
+         end);
+    monadInv H; constructor.
+Qed.
+Hint Resolve translate_instr_tr_op : htlspec.
+
+Ltac unfold_match H :=
+  match type of H with
+  | context[match ?g with _ => _ end] => destruct g; try discriminate
+  end.
+
+Ltac inv_add_instr' H :=
+  match type of H with
+  | ?f _ _ _ = OK _ _ _ => unfold f in H
+  | ?f _ _ _ _ = OK _ _ _ => unfold f in H
+  | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H
+  end; repeat unfold_match H; inversion H.
+
+Ltac inv_add_instr :=
+  match goal with
+  | H: context[add_instr_skip _ _ _] |- _ =>
+    inv_add_instr' H
+  | H: context[add_instr_skip _ _] |- _ =>
+    monadInv H; inv_incr; inv_add_instr
+  | H: context[add_instr _ _ _ _] |- _ =>
+    inv_add_instr' H
+  | H: context[add_instr _ _ _] |- _ =>
+    monadInv H; inv_incr; inv_add_instr
+  | H: context[add_branch_instr _ _ _ _ _] |- _ =>
+    inv_add_instr' H
+  | H: context[add_branch_instr _ _ _ _] |- _ =>
+    monadInv H; inv_incr; inv_add_instr
+  end.
+
+Ltac destruct_optional :=
+  match goal with H: option ?r |- _ => destruct H end.
+
+Lemma iter_expand_instr_spec :
+  forall l fin rtrn s s' i x,
+    HTLMonadExtra.collectlist (transf_instr fin rtrn) l s = OK x s' i ->
+    list_norepet (List.map fst l) ->
+    (forall pc instr, In (pc, instr) l ->
+                      tr_code pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st)).
+Proof.
+  induction l; simpl; intros; try contradiction.
+  destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
+  destruct (peq pc pc1).
+  + subst.
+    destruct instr1 eqn:?; try discriminate; try destruct_optional; inv_add_instr; econstructor.
+
+    * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * destruct o0 with pc1; destruct  H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * inversion H1. inversion H7. rewrite H. apply tr_instr_Inop.
+      eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+    * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * inversion H1. inversion H7. unfold nonblock. rewrite <- e2. rewrite H. constructor.
+      eapply translate_instr_tr_op. apply EQ1.
+      eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+    * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * inversion H1. inversion H7. rewrite <- e2. rewrite H. econstructor. apply EQ1.
+      eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+    * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * inversion H1. inversion H7. constructor.
+      eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+    * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * inversion H1. inversion H7. constructor.
+      eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+  + eapply IHl. apply EQ0. assumption.
+    destruct H1. inversion H1. subst. contradiction.
+    assumption.
+Qed.
+Hint Resolve iter_expand_instr_spec : htlspec.
+
+Theorem transl_module_correct :
+  forall f m,
+    transl_module f = Errors.OK m -> tr_module f m.
+Proof.
+  intros until m.
+  unfold transl_module.
+  unfold run_mon.
+  destruct (transf_module f (max_state f)) eqn:?; try discriminate.
+  intros. inv H.
+  inversion s; subst.
+
+  unfold transf_module in *.
+  monadInv Heqr.
+  econstructor; simpl; trivial.
+  intros.
+  inv_incr.
+  assert (st_controllogic s8 = st_controllogic s2) by congruence.
+  rewrite <- H10.
+  assert (st_datapath s8 = st_datapath s2) by congruence.
+  assert (st_st s5 = st_st s2) by congruence.
+  rewrite H80. rewrite H81. rewrite H82.
+  eauto with htlspec.
+Qed.
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index 412dc28..4a6f23e 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq -*-
+(*
  * CoqUp: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
@@ -38,6 +38,18 @@ Inductive statetrans : Type :=
 | StateGoto (p : node)
 | StateCond (c : expr) (t f : node).
 
+Definition state_goto (st : reg) (n : node) : stmnt :=
+  Vnonblock (Vvar st) (Vlit (posToValue 32 n)).
+
+Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
+  Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)).
+
+Definition statetrans_transl (stvar : reg) (st : statetrans) : stmnt :=
+  match st with
+  | StateGoto p => state_goto stvar p
+  | StateCond c t f => state_cond stvar c t f
+  end.
+
 Definition valid_freshstate (stm: PositiveMap.t stmnt) (fs: node) :=
   forall (n: node),
     Plt n fs \/ stm!n = None.
@@ -371,6 +383,10 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
     | _, _, _ => Error (Errors.msg "Veriloggen.add_instr")
     end.
 
+(** Add a register to the state without changing the [st_freshreg], as this
+should already be the right value.  This can be assumed because the max register
+is taken from the RTL code. *)
+
 Definition add_reg (r: reg) (s: state) : state :=
   mkstate (st_freshreg s)
           (st_freshstate s)
@@ -410,6 +426,9 @@ Lemma decl_io_state_incr:
          (st_wf s)).
 Proof. constructor; simpl; auto using Ple_succ with verilog_state. Qed.
 
+(** Declare a new register by incrementing the [st_freshreg] by one and
+returning the old [st_freshreg]. *)
+
 Definition decl_io (d: decl) : mon (reg * decl) :=
   fun s => let r := s.(st_freshreg) in
            OK (r, d) (mkstate
@@ -421,6 +440,9 @@ Definition decl_io (d: decl) : mon (reg * decl) :=
                      (st_wf s))
               (decl_io_state_incr s).
 
+(** Declare a new register which is given, by changing [st_decl] and without
+affecting anything else. *)
+
 Definition declare_reg (r: reg) (d: decl): mon (reg * decl) :=
   fun s => OK (r, d) (mkstate
                       (st_freshreg s)
@@ -431,6 +453,9 @@ Definition declare_reg (r: reg) (d: decl): mon (reg * decl) :=
                       (st_wf s))
               (change_decl_state_incr s (PositiveMap.add r d s.(st_decl))).
 
+(** Declare a new fresh register by first getting a valid register to increment,
+and then adding it to the declaration list. *)
+
 Definition decl_fresh_reg (d: decl) : mon (reg * decl) :=
   do (r, d) <- decl_io d;
   declare_reg r d.
@@ -557,18 +582,17 @@ Definition make_stm (r : reg) (s : PositiveMap.t stmnt) : stmnt :=
 
 Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr * stmnt :=
   match st with
-  | (n, StateGoto n') => (posToExpr 32 n, nonblock r (posToExpr 32 n'))
-  | (n, StateCond c n1 n2) => (posToExpr 32 n, nonblock r (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)))
+  | (n, StateGoto n') => (posToExpr 32 n, state_goto r n')
+  | (n, StateCond c n1 n2) => (posToExpr 32 n, state_cond r c n1 n2)
   end.
 
 Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt :=
   Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)) (Some Vskip).
 
-Fixpoint allocate_regs (e : list (reg * decl)) {struct e} : list module_item :=
+Definition allocate_reg (e : reg * decl) : module_item :=
   match e with
-  | (r, (mkdecl n 0))::es => Vdecl r n :: allocate_regs es
-  | (r, (mkdecl n l))::es => Vdeclarr r n l :: allocate_regs es
-  | nil => nil
+  | (r, (mkdecl n 0)) => Vdecl r n
+  | (r, (mkdecl n l)) => Vdeclarr r n l
   end.
 
 Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list module_item :=
@@ -577,7 +601,7 @@ Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list m
       (nonblock st (posToExpr 32 entry))
       (make_statetrans st s.(st_statetrans))))
   :: (Valways_ff (Vposedge clk) (make_stm st s.(st_stm)))
-  :: (allocate_regs (PositiveMap.elements s.(st_decl))).
+  :: (map allocate_reg (PositiveMap.elements s.(st_decl))).
 
 (** To start out with, the assumption is made that there is only one
     function/module in the original code. *)
@@ -598,20 +622,9 @@ Definition transf_module (f: function) : mon module :=
   do st <- decl_fresh_reg (mkdecl 32 0);
   do current_state <- get;
   let mi := make_module_items f.(fn_entrypoint) (fst clk) (fst st) (fst rst) current_state in
-  ret (mkmodule (get_sz start) (get_sz rst) (get_sz clk) (get_sz fin) (get_sz rtrn)
+  ret (mkmodule (get_sz start) (get_sz rst) (get_sz clk) (get_sz fin) (get_sz rtrn) (get_sz st)
                 (map set_int_size f.(fn_params)) mi).
 
-Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit))
-{struct flist} : option function :=
-  match flist with
-  | (i, AST.Gfun (AST.Internal f)) :: xs =>
-    if Pos.eqb i main
-    then Some f
-    else main_function main xs
-  | _ :: xs => main_function main xs
-  | nil => None
-  end.
-
 Lemma max_state_valid_freshstate:
   forall f,
     valid_freshstate (st_stm init_state) (Pos.succ (max_pc_function f)).
@@ -632,6 +645,24 @@ Definition max_state (f: function) : state :=
           (st_decl init_state)
           (max_state_st_wf f).
 
+Definition transl_module (f : function) : Errors.res module :=
+  run_mon (max_state f) (transf_module f).
+
+(** Retrieve the main function from the RTL, this should probably be replaced by
+retrieving a designated function instead.  This could be passed on the
+commandline and be assumed as a [Parameter] in this code. *)
+
+Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit))
+{struct flist} : option function :=
+  match flist with
+  | (i, AST.Gfun (AST.Internal f)) :: xs =>
+    if Pos.eqb i main
+    then Some f
+    else main_function main xs
+  | _ :: xs => main_function main xs
+  | nil => None
+  end.
+
 Definition transf_program (d : program) : Errors.res module :=
   match main_function d.(AST.prog_main) d.(AST.prog_defs) with
   | Some f => run_mon (max_state f) (transf_module f)
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
new file mode 100644
index 0000000..942a83a
--- /dev/null
+++ b/src/translation/Veriloggenproof.v
@@ -0,0 +1,46 @@
+(*
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+From compcert Require Import Smallstep.
+From compcert Require RTL.
+From coqup Require Verilog.
+
+Section CORRECTNESS.
+
+  Variable prog: RTL.program.
+  Variable tprog: Verilog.module.
+
+  Inductive match_states: RTL.state -> Verilog.state -> Prop :=
+  | match_state:
+      forall,
+        
+        match_states (RTL.State f s k sp e m)
+                     (Verilog.State m mi mis assoc nbassoc f cycle pc)
+  | match_returnstate:
+      forall v tv k m tm cs
+             (MS: match_stacks k cs)
+             (LD: Val.lessdef v tv)
+             (MEXT: Mem.extends m tm),
+        match_states (CminorSel.Returnstate v k m)
+                     (RTL.Returnstate cs tv tm).
+
+  Theorem transf_program_correct:
+    forward_simulation (RTL.semantics prog) (Verilog.semantics tprog).
+  Admitted.
+
+End CORRECTNESS.
diff --git a/src/translation/Veriloggenspec.v b/src/translation/Veriloggenspec.v
new file mode 100644
index 0000000..09d08ed
--- /dev/null
+++ b/src/translation/Veriloggenspec.v
@@ -0,0 +1,130 @@
+(*
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+From Coq Require Import FSets.FMapPositive.
+From compcert Require RTL Op Maps.
+From coqup Require Import Coquplib Verilog Veriloggen Value.
+
+(** * Relational specification of the translation *)
+
+(** We now define inductive predicates that characterise the fact that the
+statemachine that is created by the translation contains the correct
+translations for each of the elements *)
+
+Inductive tr_op : Op.operation -> list reg -> expr -> Prop :=
+| tr_op_Omove : forall r, tr_op Op.Omove (r::nil) (Vvar r)
+| tr_op_Ointconst : forall n l, tr_op (Op.Ointconst n) l (Vlit (intToValue n))
+| tr_op_Oneg : forall r, tr_op Op.Oneg (r::nil) (Vunop Vneg (Vvar r))
+| tr_op_Osub : forall r1 r2, tr_op Op.Osub (r1::r2::nil) (bop Vsub r1 r2)
+| tr_op_Omul : forall r1 r2, tr_op Op.Omul (r1::r2::nil) (bop Vmul r1 r2)
+| tr_op_Omulimm : forall r n, tr_op (Op.Omulimm n) (r::nil) (boplit Vmul r n)
+| tr_op_Odiv : forall r1 r2, tr_op Op.Odiv (r1::r2::nil) (bop Vdiv r1 r2)
+| tr_op_Odivu : forall r1 r2, tr_op Op.Odivu (r1::r2::nil) (bop Vdivu r1 r2)
+| tr_op_Omod : forall r1 r2, tr_op Op.Omod (r1::r2::nil) (bop Vmod r1 r2)
+| tr_op_Omodu : forall r1 r2, tr_op Op.Omodu (r1::r2::nil) (bop Vmodu r1 r2)
+| tr_op_Oand : forall r1 r2, tr_op Op.Oand (r1::r2::nil) (bop Vand r1 r2)
+| tr_op_Oandimm : forall n r, tr_op (Op.Oandimm n) (r::nil) (boplit Vand r n)
+| tr_op_Oor : forall r1 r2, tr_op Op.Oor (r1::r2::nil) (bop Vor r1 r2)
+| tr_op_Oorimm : forall n r, tr_op (Op.Oorimm n) (r::nil) (boplit Vor r n)
+| tr_op_Oxor : forall r1 r2, tr_op Op.Oxor (r1::r2::nil) (bop Vxor r1 r2)
+| tr_op_Oxorimm : forall n r, tr_op (Op.Oxorimm n) (r::nil) (boplit Vxor r n)
+| tr_op_Onot : forall r, tr_op Op.Onot (r::nil) (Vunop Vnot (Vvar r))
+| tr_op_Oshl : forall r1 r2, tr_op Op.Oshl (r1::r2::nil) (bop Vshl r1 r2)
+| tr_op_Oshlimm : forall n r, tr_op (Op.Oshlimm n) (r::nil) (boplit Vshl r n)
+| tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2)
+| tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n)
+| tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e
+| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e.
+
+Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
+| tr_instr_Inop :
+    forall n,
+      tr_instr fin rtrn st (RTL.Inop n) Vskip (state_goto st n)
+| tr_instr_Iop :
+    forall n op args e dst,
+      tr_op op args e ->
+      tr_instr fin rtrn st (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
+| tr_instr_Icond :
+    forall n1 n2 cond args s s' i c,
+      translate_condition cond args s = OK c s' i ->
+      tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
+| tr_instr_Ireturn_None :
+      tr_instr fin rtrn st (RTL.Ireturn None) (block fin (Vlit (ZToValue 1%nat 1%Z))) Vskip
+| tr_instr_Ireturn_Some :
+    forall r,
+      tr_instr fin rtrn st (RTL.Ireturn (Some r))
+               (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
+
+Inductive tr_code (c : RTL.code) (stmnts trans : PositiveMap.t stmnt)
+          (fin rtrn st : reg) : Prop :=
+| tr_code_intro :
+    forall i s t n,
+      Maps.PTree.get n c = Some i ->
+      stmnts!n = Some s ->
+      trans!n = Some t ->
+      tr_instr fin rtrn st i s t ->
+      tr_code c stmnts trans fin rtrn st.
+
+(** [tr_module_items start clk st rst s mis] holds if the state is correctly
+translated to actual Verilog, meaning it is correctly implemented as a state
+machine in Verilog.  Currently it does not seem that useful because it models
+the [make_module_items] nearly exactly.  Therefore it might have to be changed
+to make up for that. *)
+
+Inductive tr_module_items : node -> reg -> reg -> reg -> state -> list module_item -> Prop :=
+  tr_module_items_intro :
+    forall start clk st rst s mis,
+      Valways_ff (Vposedge clk)
+                 (Vcond (Vbinop Veq (Vinputvar rst) (Vlit (ZToValue 1 1)))
+                        (nonblock st (posToExpr 32 start))
+                        (make_statetrans st s.(st_statetrans)))
+      :: Valways_ff (Vposedge clk) (make_stm st s.(st_stm))
+      :: List.map allocate_reg (PositiveMap.elements s.(st_decl)) = mis ->
+      tr_module_items start clk st rst s mis.
+
+(** [tr_module function module] Holds if the [module] is the correct translation
+of the [function] that it was given. *)
+
+Inductive tr_module : RTL.function -> module -> Prop :=
+  tr_module_intro :
+    forall f mi st rtrn fin clk rst start s0 s1 s2 s3 s4 s5 s6 i1 i2 i3 i4 i5 i6,
+      decl_io 1 s0 = OK fin s1 i1 ->
+      decl_io 32 s1 = OK rtrn s2 i2 ->
+      decl_io 1 s2 = OK start s3 i3 ->
+      decl_io 1 s3 = OK rst s4 i4 ->
+      decl_io 1 s4 = OK clk s5 i5 ->
+      decl_fresh_reg 32 s5 = OK st s6 i6 ->
+      tr_code f.(RTL.fn_code) s6.(st_stm)
+                                   (PositiveMap.map (statetrans_transl (fst st)) s6.(st_statetrans))
+                                   (fst fin) (fst rtrn) (fst st) ->
+      tr_module_items f.(RTL.fn_entrypoint) (fst clk) (fst st) (fst rst) s6 mi ->
+      tr_module f (mkmodule
+                     start
+                     rst
+                     clk
+                     fin
+                     rtrn
+                     st
+                     (List.map set_int_size f.(RTL.fn_params))
+                     mi).
+
+Lemma tr_module_correct:
+  forall f m,
+  transl_module f = Errors.OK m ->
+  tr_module f m.
+Admitted.
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
new file mode 100644
index 0000000..88b13a6
--- /dev/null
+++ b/src/verilog/AssocMap.v
@@ -0,0 +1,210 @@
+(*
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+From coqup Require Import Coquplib Value.
+From compcert Require Import Maps.
+
+Definition reg := positive.
+
+Module AssocMap := Maps.PTree.
+
+Module AssocMapExt.
+  Import AssocMap.
+
+  Hint Resolve elements_correct elements_complete
+       elements_keys_norepet : assocmap.
+  Hint Resolve gso gss : assocmap.
+
+  Section Operations.
+
+    Variable A : Type.
+
+    Definition get_default (a : A) (k : reg) (m : t A) : A :=
+      match get k m with
+      | None => a
+      | Some v => v
+      end.
+
+    Fixpoint merge (m1 m2 : t A) : t A :=
+      match m1, m2 with
+      | Node l1 (Some a) r1, Node l2 _ r2 => Node (merge l1 l2) (Some a) (merge r1 r2)
+      | Node l1 None r1, Node l2 o r2 => Node (merge l1 l2) o (merge r1 r2)
+      | Leaf, _ => m2
+      | _, _ => m1
+      end.
+
+    Lemma merge_base_1 :
+      forall am,
+      merge (empty A) am = am.
+    Proof. auto. Qed.
+    Hint Resolve merge_base_1 : assocmap.
+
+    Lemma merge_base_2 :
+      forall am,
+      merge am (empty A) = am.
+    Proof.
+      unfold merge.
+      destruct am; trivial.
+      destruct o; trivial.
+    Qed.
+    Hint Resolve merge_base_2 : assocmap.
+
+    Lemma merge_add_assoc :
+      forall r am am' v,
+      merge (set r v am) am' = set r v (merge am am').
+    Proof.
+      induction r; intros; destruct am; destruct am'; try (destruct o); simpl;
+        try rewrite IHr; try reflexivity.
+    Qed.
+    Hint Resolve merge_add_assoc : assocmap.
+
+    Lemma merge_correct_1 :
+      forall am bm k v,
+      get k am = Some v ->
+      get k (merge am bm) = Some v.
+    Proof.
+      induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
+        try rewrite gempty in H; try discriminate; try assumption; auto.
+    Qed.
+    Hint Resolve merge_correct_1 : assocmap.
+
+    Lemma merge_correct_2 :
+      forall am bm k v,
+      get k am = None ->
+      get k bm = Some v ->
+      get k (merge am bm) = Some v.
+    Proof.
+      induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
+        try rewrite gempty in H; try discriminate; try assumption; auto.
+    Qed.
+    Hint Resolve merge_correct_2 : assocmap.
+
+    Definition merge_fold (am bm : t A) : t A :=
+      fold_right (fun p a => set (fst p) (snd p) a) bm (elements am).
+
+    Lemma add_assoc :
+      forall (k : elt) (v : A) l bm,
+      List.In (k, v) l ->
+      list_norepet (List.map fst l) ->
+      @get A k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v.
+    Proof.
+      induction l; intros.
+      - contradiction.
+      - destruct a as [k' v'].
+        destruct (peq k k').
+        + inversion H. inversion H1. inversion H0. subst.
+          simpl. auto with assocmap.
+
+          inversion H0; subst. apply in_map with (f:=fst) in H1. contradiction.
+
+        + inversion H. inversion H1. inversion H0. subst. simpl. rewrite gso; try assumption.
+          apply IHl. contradiction. contradiction.
+          simpl. rewrite gso; try assumption. apply IHl. assumption. inversion H0. subst. assumption.
+    Qed.
+    Hint Resolve add_assoc : assocmap.
+
+    Lemma not_in_assoc :
+      forall k v l bm,
+      ~ List.In k (List.map (@fst elt A) l) ->
+      @get A k bm = Some v ->
+      get k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v.
+    Proof.
+      induction l; intros.
+      - assumption.
+      - destruct a as [k' v'].
+        destruct (peq k k'); subst;
+          simpl in *; apply Decidable.not_or in H; destruct H. contradiction.
+        rewrite AssocMap.gso; auto.
+    Qed.
+    Hint Resolve not_in_assoc : assocmap.
+
+    Lemma elements_iff :
+      forall am k,
+      (exists v, get k am = Some v) <->
+      List.In k (List.map (@fst _ A) (elements am)).
+    Proof.
+      split; intros.
+      destruct H. apply elements_correct in H. apply in_map with (f := fst) in H. apply H.
+      apply list_in_map_inv in H. destruct H. destruct H. subst.
+      exists (snd x). apply elements_complete. assert (x = (fst x, snd x)) by apply surjective_pairing.
+      rewrite H in H0; assumption.
+    Qed.
+    Hint Resolve elements_iff : assocmap.
+
+    Lemma elements_correct' :
+      forall am k,
+      ~ (exists v, get k am = Some v) <->
+      ~ List.In k (List.map (@fst _ A) (elements am)).
+    Proof. auto using not_iff_compat with assocmap. Qed.
+    Hint Resolve elements_correct' : assocmap.
+
+    Lemma elements_correct_none :
+      forall am k,
+      get k am = None ->
+      ~ List.In k (List.map (@fst _ A) (elements am)).
+    Proof.
+      intros. apply elements_correct'. unfold not. intros.
+      destruct H0. rewrite H in H0. discriminate.
+    Qed.
+    Hint Resolve elements_correct_none : assocmap.
+
+    Lemma merge_fold_add :
+      forall k v am bm,
+      am ! k = Some v ->
+      (merge_fold am bm) ! k = Some v.
+    Proof. unfold merge_fold; auto with assocmap. Qed.
+    Hint Resolve merge_fold_add : assocmap.
+
+    Lemma merge_fold_not_in :
+      forall k v am bm,
+      get k am = None ->
+      get k bm = Some v ->
+      get k (merge_fold am bm) = Some v.
+    Proof. intros. apply not_in_assoc; auto with assocmap. Qed.
+    Hint Resolve merge_fold_not_in : assocmap.
+
+    Lemma merge_fold_base :
+      forall am,
+      merge_fold (empty A) am = am.
+    Proof. auto. Qed.
+    Hint Resolve merge_fold_base : assocmap.
+
+  End Operations.
+
+End AssocMapExt.
+Import AssocMapExt.
+
+Definition assocmap := AssocMap.t value.
+
+Definition find_assocmap (n : nat) : reg -> assocmap -> value :=
+  get_default value (ZToValue n 0).
+
+Definition empty_assocmap : assocmap := AssocMap.empty value.
+
+Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value.
+
+Ltac unfold_merge :=
+  unfold merge_assocmap; try (repeat (rewrite merge_add_assoc));
+  rewrite AssocMapExt.merge_base_1.
+
+Module AssocMapNotation.
+  Notation "a ! b" := (AssocMap.get b a) (at level 1).
+  Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1).
+  Notation "a # b" := (find_assocmap 32 b a) (at level 1).
+  Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1).
+End AssocMapNotation.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 1d156ad..a21064c 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -16,89 +16,83 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(** The purpose of the hardware transfer language (HTL) is to create a more
-  * hardware-like layout that is still similar to the register transfer language
-  * (RTL) that it came from. The main change is that function calls become
-  * module instantiations and that we now describe a state machine instead of a
-  * control-flow graph.
-  *)
-
-From coqup.common Require Import Coquplib.
-
+From Coq Require Import FSets.FMapPositive.
+From coqup Require Import Coquplib Value AssocMap.
+From coqup Require Verilog.
+From compcert Require Events Globalenvs Smallstep Integers.
 From compcert Require Import Maps.
-From compcert Require Op AST Memory Registers.
-
-Definition node := positive.
 
-Definition reg := Registers.reg.
-
-Definition ident := AST.ident.
-
-Inductive instruction : Type :=
-| Hnop : node -> instruction
-| Hnonblock : Op.operation -> list reg -> reg -> node -> instruction
-  (** [Hnonblock op args res next] Defines a nonblocking assignment to a
-      register, using the operation defined in Op.v. *)
-| Hload : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction
-| Hstore : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction
-| Hinst : AST.signature -> ident -> reg -> node -> instruction
-  (** [Hinst sig fun args rst strt end res next] Defines the start of a
-      module instantiation, meaning the function will run until the result is
-      returned. *)
-| Htailcall : AST.signature -> ident -> list reg -> instruction
-| Hcond : Op.condition -> list reg -> node -> node -> instruction
-| Hjumptable : reg -> list node -> instruction
-| Hfinish : option reg -> instruction.
-
-Record inst : Type :=
-  mkinst {
-    inst_moddecl : ident;
-    inst_args : list reg
-  }.
+Import HexNotationValue.
 
-Definition code : Type := PTree.t instruction.
+(** The purpose of the hardware transfer language (HTL) is to create a more
+hardware-like layout that is still similar to the register transfer language
+(RTL) that it came from. The main change is that function calls become module
+instantiations and that we now describe a state machine instead of a
+control-flow graph. *)
 
-Definition instances : Type := PTree.t inst.
+Definition reg := positive.
+Definition node := positive.
 
-Definition empty_instances : instances := PTree.empty inst.
+Definition datapath := PTree.t Verilog.stmnt.
+Definition controllogic := PTree.t Verilog.stmnt.
 
-(** Function declaration for VTL also contain a construction which describes the
-    functions that are called in the current function. This information is used
-    to print out *)
-Record module : Type :=
+Record module: Type :=
   mkmodule {
-    mod_sig : AST.signature;
     mod_params : list reg;
-    mod_stacksize : Z;
-    mod_code : code;
-    mod_insts : instances;
-    mod_entrypoint : node
+    mod_datapath : datapath;
+    mod_controllogic : controllogic;
+    mod_entrypoint : node;
+    mod_st : reg;
+    mod_finish : reg;
+    mod_return : reg
   }.
 
-Definition moddecl := AST.fundef module.
-
-Definition design := AST.program moddecl unit.
-
-Definition modsig (md : moddecl) :=
-  match md with
-  | AST.Internal m => mod_sig m
-  | AST.External ef => AST.ef_sig ef
-  end.
-
-(** Describes various transformations that can be applied to HTL. This applies
-    the transformation to each instruction in the function and returns the new
-    function with the modified instructions. *)
-Section TRANSF.
-
-  Variable transf_instr : node -> instruction -> instruction.
-
-  Definition transf_module (m : module) : module :=
-    mkmodule
-      m.(mod_sig)
-      m.(mod_params)
-      m.(mod_stacksize)
-      (PTree.map transf_instr m.(mod_code))
-      m.(mod_insts)
-      m.(mod_entrypoint).
-
-End TRANSF.
+(** * Operational Semantics *)
+
+Definition genv := Globalenvs.Genv.t unit unit.
+Definition genv_empty := Globalenvs.Genv.empty_genv unit unit nil.
+
+Inductive state : Type :=
+| State :
+    forall (m : module)
+           (st : node)
+           (assoc : assocmap),
+  state
+| Returnstate : forall v : value, state.
+
+Inductive step : genv -> state -> Events.trace -> state -> Prop :=
+| step_module :
+    forall g t m st ctrl data assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f stval pstval,
+      m.(mod_controllogic)!st = Some ctrl ->
+      m.(mod_datapath)!st = Some data ->
+      Verilog.stmnt_runp f
+        (Verilog.mkassociations assoc0 empty_assocmap)
+        ctrl
+        (Verilog.mkassociations assoc1 nbassoc0) ->
+      Verilog.stmnt_runp f
+        (Verilog.mkassociations assoc1 nbassoc0)
+        data
+        (Verilog.mkassociations assoc2 nbassoc1) ->
+      assoc3 = merge_assocmap nbassoc1 assoc2 ->
+      assoc3!(m.(mod_st)) = Some stval ->
+      valueToPos stval = pstval ->
+      step g (State m st assoc0) t (State m pstval assoc3)
+| step_finish :
+    forall g t m st assoc retval,
+    assoc!(m.(mod_finish)) = Some (1'h"1") ->
+    assoc!(m.(mod_return)) = Some retval ->
+    step g (State m st assoc) t (Returnstate retval).
+Hint Constructors step : htl.
+
+Inductive initial_state (m : module) : state -> Prop :=
+| initial_state_intro : forall st,
+    st = m.(mod_entrypoint) ->
+    initial_state m (State m st empty_assocmap).
+
+Inductive final_state : state -> Integers.int -> Prop :=
+| final_state_intro : forall retval retvali,
+    value_int_eqb retval retvali = true ->
+    final_state (Returnstate retval) retvali.
+
+Definition semantics (m : module) :=
+  Smallstep.Semantics step (initial_state m) final_state genv_empty.
diff --git a/src/verilog/Test.v b/src/verilog/Test.v
new file mode 100644
index 0000000..90c5312
--- /dev/null
+++ b/src/verilog/Test.v
@@ -0,0 +1,99 @@
+(*
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+From coqup Require Import Verilog Veriloggen Coquplib Value.
+From compcert Require Import AST Errors Maps Op Integers.
+From compcert Require RTL.
+From Coq Require Import FSets.FMapPositive.
+From bbv Require Import Word.
+Import ListNotations.
+Import HexNotationValue.
+Import WordScope.
+
+Local Open Scope word_scope.
+
+Definition test_module : module :=
+  let mods := [
+      Valways (Vposedge 3%positive) (Vseq (Vnonblock (Vvar 6%positive) (Vlit (ZToValue 32 5)))
+                                          (Vnonblock (Vvar 7%positive)
+                                                     (Vvar 6%positive)))
+      ] in
+  mkmodule (1%positive, 1%nat)
+           (2%positive, 1%nat)
+           (3%positive, 1%nat)
+           (4%positive, 1%nat)
+           (5%positive, 32%nat)
+           (6%positive, 32%nat)
+           nil
+           mods.
+
+Definition test_input : RTL.function :=
+  let sig := mksignature nil Tvoid cc_default in
+  let params := nil in
+  let stacksize := 0 in
+  let entrypoint := 3%positive in
+  let code := PTree.set 1%positive (RTL.Ireturn (Some 1%positive))
+               (PTree.set 3%positive (RTL.Iop (Ointconst (Int.repr 5)) nil 1%positive 1%positive)
+                          (PTree.empty RTL.instruction)) in
+  RTL.mkfunction sig params stacksize code entrypoint.
+
+Definition test_input_program : RTL.program :=
+  mkprogram [(1%positive, Gfun (Internal test_input))] nil 1%positive.
+
+Compute transf_program test_input_program.
+
+Definition test_output_module : module :=
+  {| mod_start := (4%positive, 1%nat);
+     mod_reset := (5%positive, 1%nat);
+     mod_clk := (6%positive, 1%nat);
+     mod_finish := (2%positive, 1%nat);
+     mod_return := (3%positive, 32%nat);
+     mod_state := (7%positive, 32%nat);
+     mod_args := [];
+     mod_body :=
+       [Valways_ff (Vposedge 6%positive)
+                   (Vcond (Vbinop Veq (Vinputvar 5%positive) (1'h"1"))
+                          (Vnonblock (Vvar 7%positive) (32'h"3"))
+                          (Vcase (Vvar 7%positive)
+                                 [(Vlit (32'h"1"), Vnonblock (Vvar 7%positive) (32'h"1"));
+                                 (Vlit (32'h"3"), Vnonblock (Vvar 7%positive) (32'h"1"))]
+                                 (Some Vskip)));
+       Valways_ff (Vposedge 6%positive)
+                  (Vcase (Vvar 7%positive)
+                         [(Vlit (32'h"1"), Vseq (Vblock (Vvar 2%positive) (Vlit (1'h"1")))
+                                                (Vblock (Vvar 3%positive) (Vvar 1%positive)));
+                         (Vlit (32'h"3"), Vblock (Vvar 1%positive) (Vlit (32'h"5")))]
+                         (Some Vskip));
+       Vdecl 1%positive 32; Vdecl 7%positive 32] |}.
+
+Lemma valid_test_output :
+  transf_program test_input_program = OK test_output_module.
+Proof. trivial. Qed.
+
+Definition test_fextclk := initial_fextclk test_output_module.
+
+Lemma manual_simulation :
+  step (State test_output_module empty_assocmap empty_assocmap
+              test_fextclk 1 (32'h"1"))
+       (State test_output_module (add_assocmap 7%positive (32'h"3") empty_assocmap)
+              empty_assocmap test_fextclk 2 (32'h"3")).
+Proof.
+  repeat (econstructor; eauto);
+  try (unfold ZToValue; instantiate (1 := eq_refl (vsize (1'h"1"))); auto);
+  apply nevalue; apply weqb_false; trivial. Unshelve. exact 0%nat.
+Qed.
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index fe53dbc..34cb0d2 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq -*-
+(*
  * CoqUp: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
@@ -18,8 +18,9 @@
 
 (* begin hide *)
 From bbv Require Import Word.
-From Coq Require Import ZArith.ZArith.
-From compcert Require Import lib.Integers.
+From bbv Require HexNotation WordScope.
+From Coq Require Import ZArith.ZArith FSets.FMapPositive.
+From compcert Require Import lib.Integers common.Values.
 (* end hide *)
 
 (** * Value
@@ -47,7 +48,7 @@ Definition wordToValue : forall sz : nat, word sz -> value := mkvalue.
 
 Definition valueToWord : forall v : value, word (vsize v) := vword.
 
-Definition valueToNat (v : value) : nat :=
+Definition valueToNat (v :value) : nat :=
   wordToNat (vword v).
 
 Definition natToValue sz (n : nat) : value :=
@@ -59,13 +60,6 @@ Definition valueToN (v : value) : N :=
 Definition NToValue sz (n : N) : value :=
   mkvalue sz (NToWord sz n).
 
-Definition posToValue sz (p : positive) : value :=
-  mkvalue sz (posToWord sz p).
-
-Definition posToValueAuto (p : positive) : value :=
-  let size := Z.to_nat (Z.succ (log_inf p)) in
-  mkvalue size (Word.posToWord size p).
-
 Definition ZToValue (s : nat) (z : Z) : value :=
   mkvalue s (ZToWord s z).
 
@@ -75,9 +69,29 @@ Definition valueToZ (v : value) : Z :=
 Definition uvalueToZ (v : value) : Z :=
   uwordToZ (vword v).
 
+Definition posToValue sz (p : positive) : value :=
+  ZToValue sz (Zpos p).
+
+Definition posToValueAuto (p : positive) : value :=
+  let size := Pos.to_nat (Pos.size p) in
+  ZToValue size (Zpos p).
+
+Definition valueToPos (v : value) : positive :=
+  Z.to_pos (uvalueToZ v).
+
 Definition intToValue (i : Integers.int) : value :=
   ZToValue Int.wordsize (Int.unsigned i).
 
+Definition valueToInt (i : value) : Integers.int :=
+  Int.repr (valueToZ i).
+
+Definition valToValue (v : Values.val) : option value :=
+  match v with
+  | Values.Vint i => Some (intToValue i)
+  | Values.Vundef => Some (ZToValue 32 0%Z)
+  | _ => None
+  end.
+
 (** Convert a [value] to a [bool], so that choices can be made based on the
 result. This is also because comparison operators will give back [value] instead
 of [bool], so if they are in a condition, they will have to be converted before
@@ -91,8 +105,8 @@ Definition boolToValue (sz : nat) (b : bool) : value :=
 
 (** ** Arithmetic operations *)
 
-Lemma unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
-Proof. intros; subst; assumption. Qed.
+Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
+intros; subst; assumption. Defined.
 
 Definition value_eq_size:
   forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }.
@@ -137,6 +151,64 @@ Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value)
   | _ => None
   end.
 
+Lemma eqvalue {sz : nat} (x y : word sz) : x = y <-> mkvalue sz x = mkvalue sz y.
+Proof.
+  split; intros.
+  subst. reflexivity. inversion H. apply existT_wordToZ in H1.
+  apply wordToZ_inj. assumption.
+Qed.
+
+Lemma eqvaluef {sz : nat} (x y : word sz) : x = y -> mkvalue sz x = mkvalue sz y.
+Proof. apply eqvalue. Qed.
+
+Lemma nevalue {sz : nat} (x y : word sz) : x <> y <-> mkvalue sz x <> mkvalue sz y.
+Proof. split; intros; intuition. apply H. apply eqvalue. assumption.
+       apply H. rewrite H0. trivial.
+Qed.
+
+Lemma nevaluef {sz : nat} (x y : word sz) : x <> y -> mkvalue sz x <> mkvalue sz y.
+Proof. apply nevalue. Qed.
+
+(*Definition rewrite_word_size (initsz finalsz : nat) (w : word initsz)
+  : option (word finalsz) :=
+  match Nat.eqb initsz finalsz return option (word finalsz) with
+  | true => Some _
+  | false => None
+  end.*)
+
+Definition valueeq (sz : nat) (x y : word sz) :
+  {mkvalue sz x = mkvalue sz y} + {mkvalue sz x <> mkvalue sz y} :=
+  match weq x y with
+  | left eq => left (eqvaluef x y eq)
+  | right ne => right (nevaluef x y ne)
+  end.
+
+Definition valueeqb (x y : value) : bool :=
+  match value_eq_size x y with
+  | left EQ =>
+    weqb (vword x) (unify_word (vsize x) (vsize y) (vword y) EQ)
+  | right _ => false
+  end.
+
+Definition value_projZ_eqb (v1 v2 : value) : bool := Z.eqb (valueToZ v1) (valueToZ v2).
+
+Theorem value_projZ_eqb_true :
+  forall v1 v2,
+  v1 = v2 -> value_projZ_eqb v1 v2 = true.
+Proof. intros. subst. unfold value_projZ_eqb. apply Z.eqb_eq. trivial. Qed.
+
+Theorem valueeqb_true_iff :
+  forall v1 v2,
+  valueeqb v1 v2 = true <-> v1 = v2.
+Proof.
+  split; intros.
+  unfold valueeqb in H. destruct (value_eq_size v1 v2) eqn:?.
+  - destruct v1, v2. simpl in H.
+Abort.
+
+Definition value_int_eqb (v : value) (i : int) : bool :=
+  Z.eqb (valueToZ v) (Int.unsigned i).
+
 (** Arithmetic operations over [value], interpreting them as signed or unsigned
 depending on the operation.
 
@@ -208,3 +280,48 @@ Definition shift_map (sz : nat) (f : word sz -> nat -> word sz) (w1 w2 : word sz
 
 Definition vshl v1 v2 := map_word2 (fun sz => shift_map sz (@wlshift sz)) v1 v2.
 Definition vshr v1 v2 := map_word2 (fun sz => shift_map sz (@wrshift sz)) v1 v2.
+
+Module HexNotationValue.
+  Export HexNotation.
+  Import WordScope.
+
+  Notation "sz ''h' a" := (NToValue sz (hex a)) (at level 50).
+
+End HexNotationValue.
+
+Inductive val_value_lessdef: val -> value -> Prop :=
+| val_value_lessdef_int:
+    forall i v',
+    Integers.Int.unsigned i = valueToZ v' ->
+    val_value_lessdef (Vint i) v'
+| lessdef_undef: forall v, val_value_lessdef Vundef v.
+
+Lemma valueToZ_ZToValue :
+  forall n z,
+  (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z ->
+  valueToZ (ZToValue (S n) z) = z.
+Proof.
+  unfold valueToZ, ZToValue. simpl.
+  auto using wordToZ_ZToWord.
+Qed.
+
+Lemma uvalueToZ_ZToValue :
+  forall n z,
+  (0 <= z < 2 ^ Z.of_nat n)%Z ->
+  uvalueToZ (ZToValue n z) = z.
+Proof.
+  unfold uvalueToZ, ZToValue. simpl.
+  auto using uwordToZ_ZToWord.
+Qed.
+
+Lemma valueToPos_posToValueAuto :
+  forall p, valueToPos (posToValueAuto p) = p.
+Proof.
+  intros. unfold valueToPos, posToValueAuto.
+  rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z.
+  split. apply Zle_0_pos.
+
+  assert (p < 2 ^ (Pos.size p))%positive. apply Pos.size_gt.
+  inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1.
+  simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.
+Qed.
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index dfb6255..e2b85b2 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq -*-
+(*
  * CoqUp: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
  *
@@ -27,18 +27,22 @@ From Coq Require Import
 
 Import ListNotations.
 
-From coqup Require Import common.Coquplib common.Show verilog.Value.
+From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap.
+From compcert Require Integers Events.
+From compcert Require Import Errors Smallstep Globalenvs.
 
-From compcert Require Integers.
-From compcert Require Import Errors.
-
-Notation "a ! b" := (PositiveMap.find b a) (at level 1).
+Import HexNotationValue.
+Import AssocMapNotation.
 
 Definition reg : Type := positive.
 Definition node : Type := positive.
 Definition szreg : Type := reg * nat.
 
-Definition assoclist : Type := PositiveMap.t value.
+Record associations : Type :=
+  mkassociations {
+    assoc_blocking : assocmap;
+    assoc_nonblocking : assocmap
+  }.
 
 (** * Verilog AST
 
@@ -51,8 +55,6 @@ The Verilog [value] is a bitvector containg a size and the actual bitvector. In
 this case, the [Word.word] type is used as many theorems about that bitvector
 have already been proven. *)
 
-Definition estate : Type := assoclist * assoclist.
-
 (** ** Binary Operators
 
 These are the binary operations that can be represented in Verilog. Ideally,
@@ -159,10 +161,10 @@ Record module : Type := mkmodule {
   mod_clk : szreg;
   mod_finish : szreg;
   mod_return : szreg;
+  mod_state : szreg; (**r Variable that defines the current state, it should be internal. *)
   mod_args : list szreg;
   mod_body : list module_item;
-}.
-
+                        }.
 (** Convert a [positive] to an expression directly, setting it to the right
     size. *)
 Definition posToLit (p : positive) : expr :=
@@ -171,15 +173,41 @@ Definition posToLit (p : positive) : expr :=
 Coercion Vlit : value >-> expr.
 Coercion Vvar : reg >-> expr.
 
-Definition fext := PositiveMap.t value.
+Definition fext := AssocMap.t value.
 Definition fextclk := nat -> fext.
 
-Inductive state: Type :=
-  State:
-    forall (assoc : assoclist)
-           (nbassoc : assoclist)
+(** ** State
+
+The [state] contains the following items:
+n
+- Current [module] that is being worked on, so that the state variable can be
+retrieved and set appropriately.
+- Current [module_item] which is being worked on.
+- A contiunation ([cont]) which defines what to do next.  The option is to
+  either evaluate another module item or go to the next clock cycle.  Finally
+  it could also end if the finish flag of the module goes high.
+- Association list containing the blocking assignments made, or assignments made
+  in previous clock cycles.
+- Nonblocking association list containing all the nonblocking assignments made
+  in the current module.
+- The environment containing values for the input.
+- The program counter which determines the value for the state in this version of
+  Verilog, as the Verilog was generated by the RTL, which means that we have to
+  make an assumption about how it looks.  In this case, that it contains state
+  which determines which part of the Verilog is executed.  This is then the part
+  of the Verilog that should match with the RTL. *)
+
+Inductive state : Type :=
+| State:
+    forall (m : module)
+           (assoc : assocmap)
+           (nbassoc : assocmap)
            (f : fextclk)
-           (cycle : positive),
+           (cycle : nat)
+           (stvar : value),
+    state
+| Finishstate:
+    forall v : value,
     state.
 
 Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value :=
@@ -214,40 +242,48 @@ Definition unop_run (op : unop) : value -> value :=
   | Vnot => vbitneg
   end.
 
-Inductive expr_runp : state -> expr -> value -> Prop :=
+Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop :=
   | erun_Vlit :
-      forall s v,
-      expr_runp s (Vlit v) v
+      forall fext assoc v,
+      expr_runp fext assoc (Vlit v) v
   | erun_Vvar :
-      forall assoc na f c v r,
+      forall fext assoc v r,
       assoc!r = Some v ->
-      expr_runp (State assoc na f c) (Vvar r) v
+      expr_runp fext assoc (Vvar r) v
+  | erun_Vvar_empty :
+      forall fext assoc r sz,
+      assoc!r = None ->
+      expr_runp fext assoc (Vvar r) (ZToValue sz 0)
   | erun_Vinputvar :
-      forall s r v,
-      expr_runp s (Vinputvar r) v
+      forall fext assoc r v,
+      fext!r = Some v ->
+      expr_runp fext assoc (Vinputvar r) v
   | erun_Vbinop :
-      forall s op l r lv rv oper EQ,
-      expr_runp s l lv ->
-      expr_runp s r rv ->
+      forall fext assoc op l r lv rv oper EQ resv,
+      expr_runp fext assoc l lv ->
+      expr_runp fext assoc r rv ->
       oper = binop_run op ->
-      expr_runp s (Vbinop op l r) (oper lv rv EQ)
+      resv = oper lv rv EQ ->
+      expr_runp fext assoc (Vbinop op l r) resv
   | erun_Vunop :
-      forall s u vu op oper,
-      expr_runp s u vu ->
+      forall fext assoc u vu op oper resv,
+      expr_runp fext assoc u vu ->
       oper = unop_run op ->
-      expr_runp s (Vunop op u) (oper vu)
+      resv = oper vu ->
+      expr_runp fext assoc (Vunop op u) resv
   | erun_Vternary_true :
-      forall s c ts fs vc vt,
-      expr_runp s c vc ->
-      expr_runp s ts vt ->
+      forall fext assoc c ts fs vc vt,
+      expr_runp fext assoc c vc ->
+      expr_runp fext assoc ts vt ->
       valueToBool vc = true ->
-      expr_runp s (Vternary c ts fs) vt
+      expr_runp fext assoc (Vternary c ts fs) vt
   | erun_Vternary_false :
-      forall s c ts fs vc vf,
-      expr_runp s c vc ->
-      expr_runp s fs vf ->
+      forall fext assoc c ts fs vc vf,
+      expr_runp fext assoc c vc ->
+      expr_runp fext assoc fs vf ->
       valueToBool vc = false ->
-      expr_runp s (Vternary c ts fs) vf.
+      expr_runp fext assoc (Vternary c ts fs) vf.
+Hint Constructors expr_runp : verilog.
 
 Definition handle_opt {A : Type} (err : errmsg) (val : option A)
   : res A :=
@@ -265,22 +301,20 @@ Definition handle_def {A : Type} (a : A) (val : option A)
 
 Local Open Scope error_monad_scope.
 
-Definition access_fext (s : state) (r : reg) : res value :=
-  match s with
-  | State _ _ f c =>
-    match PositiveMap.find r (f (Pos.to_nat c)) with
-    | Some v => OK v
-    | _ => OK (ZToValue 1 0)
-    end
+Definition access_fext (f : fext) (r : reg) : res value :=
+  match AssocMap.get r f with
+  | Some v => OK v
+  | _ => OK (ZToValue 1 0)
   end.
 
 (* TODO FIX Vvar case without default *)
-Fixpoint expr_run (s : state) (e : expr)
+(*Fixpoint expr_run (assoc : assocmap) (e : expr)
          {struct e} : res value :=
   match e with
   | Vlit v => OK v
   | Vvar r => match s with
-              | State assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r
+              | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r
+              | _ => Error (msg "Verilog: Wrong state")
               end
   | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled")
   | Vinputvar r => access_fext s r
@@ -299,7 +333,7 @@ Fixpoint expr_run (s : state) (e : expr)
   | Vternary c te fe =>
     do cv <- expr_run s c;
     if valueToBool cv then expr_run s te else expr_run s fe
-  end.
+  end.*)
 
 (** Return the name of the lhs of an assignment. For now, this function is quite
 simple because only assignment to normal variables is supported and needed. *)
@@ -310,6 +344,15 @@ Definition assign_name (e : expr) : res reg :=
   | _ => Error (msg "Verilog: expression not supported on lhs of assignment")
   end.
 
+(*Fixpoint stmnt_height (st : stmnt) {struct st} : nat :=
+  match st with
+  | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2)
+  | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2))
+  | Vcase _ ls (Some st) =>
+    S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls)
+  | _ => 1
+  end.
+
 Fixpoint find_case_stmnt (s : state) (v : value) (cl : list (expr * stmnt))
          {struct cl} : option (res stmnt) :=
   match cl with
@@ -348,35 +391,85 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
       end
     | Vblock lhs rhs =>
       match s with
-      | State assoc nbassoc f c =>
+      | State m assoc nbassoc f c =>
         do name <- assign_name lhs;
         do rhse <- expr_run s rhs;
-        OK (State (PositiveMap.add name rhse assoc) nbassoc f c)
+        OK (State m (PositiveMap.add name rhse assoc) nbassoc f c)
+      | _ => Error (msg "Verilog: Wrong state")
       end
     | Vnonblock lhs rhs =>
       match s with
-      | State assoc nbassoc f c =>
+      | State m assoc nbassoc f c =>
         do name <- assign_name lhs;
         do rhse <- expr_run s rhs;
-        OK (State assoc (PositiveMap.add name rhse nbassoc) f c)
+        OK (State m assoc (PositiveMap.add name rhse nbassoc) f c)
+      | _ => Error (msg "Verilog: Wrong state")
       end
     end
   | _ => OK s
   end.
 
-Fixpoint stmnt_height (st : stmnt) {struct st} : nat :=
-  match st with
-  | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2)
-  | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2))
-  | Vcase _ ls (Some st) =>
-    S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls)
-  | _ => 1
-  end.
-
 Definition stmnt_run (s : state) (st : stmnt) : res state :=
-  stmnt_run' (stmnt_height st) s st.
-
-Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
+  stmnt_run' (stmnt_height st) s st. *)
+
+Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop :=
+| stmnt_runp_Vskip:
+    forall f a, stmnt_runp f a Vskip a
+| stmnt_runp_Vseq:
+    forall f st1 st2 as0 as1 as2,
+    stmnt_runp f as0 st1 as1 ->
+    stmnt_runp f as1 st2 as2 ->
+    stmnt_runp f as0 (Vseq st1 st2) as2
+| stmnt_runp_Vcond_true:
+    forall as0 as1 f c vc stt stf,
+    expr_runp f as0.(assoc_blocking) c vc ->
+    valueToBool vc = true ->
+    stmnt_runp f as0 stt as1 ->
+    stmnt_runp f as0 (Vcond c stt stf) as1
+| stmnt_runp_Vcond_false:
+    forall as0 as1 f c vc stt stf,
+    expr_runp f as0.(assoc_blocking) c vc ->
+    valueToBool vc = false ->
+    stmnt_runp f as0 stf as1 ->
+    stmnt_runp f as0 (Vcond c stt stf) as1
+| stmnt_runp_Vcase_nomatch:
+    forall e ve as0 f as1 me mve sc cs def,
+    expr_runp f as0.(assoc_blocking) e ve ->
+    expr_runp f as0.(assoc_blocking) me mve ->
+    mve <> ve ->
+    stmnt_runp f as0 (Vcase e cs def) as1 ->
+    stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1
+| stmnt_runp_Vcase_match:
+    forall e ve as0 f as1 me mve sc cs def,
+    expr_runp f as0.(assoc_blocking) e ve ->
+    expr_runp f as0.(assoc_blocking) me mve ->
+    mve = ve ->
+    stmnt_runp f as0 sc as1 ->
+    stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1
+| stmnt_runp_Vcase_default:
+    forall as0 as1 f st e ve,
+    expr_runp f as0.(assoc_blocking) e ve ->
+    stmnt_runp f as0 st as1 ->
+    stmnt_runp f as0 (Vcase e nil (Some st)) as1
+| stmnt_runp_Vblock:
+    forall lhs name rhs rhsval assoc assoc' nbassoc f,
+    assign_name lhs = OK name ->
+    expr_runp f assoc rhs rhsval ->
+    assoc' = (AssocMap.set name rhsval assoc) ->
+    stmnt_runp f (mkassociations assoc nbassoc)
+                 (Vblock lhs rhs)
+                 (mkassociations assoc' nbassoc)
+| stmnt_runp_Vnonblock:
+    forall lhs name rhs rhsval assoc nbassoc nbassoc' f,
+    assign_name lhs = OK name ->
+    expr_runp f assoc rhs rhsval ->
+    nbassoc' = (AssocMap.set name rhsval nbassoc) ->
+    stmnt_runp f (mkassociations assoc nbassoc)
+                 (Vnonblock lhs rhs)
+                 (mkassociations assoc nbassoc').
+Hint Constructors stmnt_runp : verilog.
+
+(*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
   let run := fun st ls =>
               do s' <- stmnt_run s st;
               mi_step s' ls
@@ -388,41 +481,69 @@ Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
   | (Vdecl _ _)::ls => mi_step s ls
   | (Vdeclarr _ _ _)::ls => mi_step s ls
   | nil => OK s
-  end.
-
-Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist :=
-  PositiveMap.add r v assoc.
-
-Definition merge_assoclist (nbassoc assoc : assoclist) : assoclist :=
-  PositiveMap.fold add_assoclist nbassoc assoc.
-
-Definition empty_assoclist : assoclist := PositiveMap.empty value.
-
-Definition mi_step_commit (s : state) (m : list module_item) : res state :=
+  end.*)
+
+Inductive mi_stepp : fext -> associations -> module_item -> associations -> Prop :=
+| mi_stepp_Valways :
+    forall f s0 st s1 c,
+    stmnt_runp f s0 st s1 ->
+    mi_stepp f s0 (Valways c st) s1
+| mi_stepp_Valways_ff :
+    forall f s0 st s1 c,
+    stmnt_runp f s0 st s1 ->
+    mi_stepp f s0 (Valways_ff c st) s1
+| mi_stepp_Valways_comb :
+    forall f s0 st s1 c,
+    stmnt_runp f s0 st s1 ->
+    mi_stepp f s0 (Valways_comb c st) s1
+| mi_stepp_Vdecl :
+    forall f s lhs rhs,
+    mi_stepp f s (Vdecl lhs rhs) s.
+Hint Constructors mi_stepp : verilog.
+
+Inductive mis_stepp : fext -> associations -> list module_item -> associations -> Prop :=
+| mis_stepp_Cons :
+    forall f mi mis s0 s1 s2,
+    mi_stepp f s0 mi s1 ->
+    mis_stepp f s1 mis s2 ->
+    mis_stepp f s0 (mi :: mis) s2
+| mis_stepp_Nil :
+    forall f s,
+    mis_stepp f s nil s.
+Hint Constructors mis_stepp : verilog.
+
+(*Definition mi_step_commit (s : state) (m : list module_item) : res state :=
   match mi_step s m with
-  | OK (State assoc nbassoc f c) =>
-    OK (State (merge_assoclist nbassoc assoc) empty_assoclist f c)
+  | OK (State m assoc nbassoc f c) =>
+    OK (State m (merge_assocmap nbassoc assoc) empty_assocmap f c)
   | Error msg => Error msg
+  | _ => Error (msg "Verilog: Wrong state")
   end.
 
-Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : nat)
-         {struct n} : res assoclist :=
+Fixpoint mi_run (f : fextclk) (assoc : assocmap) (m : list module_item) (n : nat)
+         {struct n} : res assocmap :=
   match n with
   | S n' =>
     do assoc' <- mi_run f assoc m n';
-    match mi_step_commit (State assoc' empty_assoclist f (Pos.of_nat n')) m with
+    match mi_step_commit (State assoc' empty_assocmap f (Pos.of_nat n')) m with
     | OK (State assoc _ _ _) => OK assoc
     | Error m => Error m
     end
   | O => OK assoc
-  end.
+  end.*)
 
-Definition module_run (n : nat) (m : module) : res assoclist :=
-  let f := fun x => match x with
-                    | S O => (add_assoclist (fst (mod_reset m)) (ZToValue 1 1) empty_assoclist)
-                    | _ => (add_assoclist (fst (mod_reset m)) (ZToValue 1 0) empty_assoclist)
-                    end in
-  mi_run f empty_assoclist (mod_body m) n.
+(** Resets the module into a known state, so that it can be executed.  This is
+assumed to be the starting state of the module, and may have to be changed if
+other arguments to the module are also to be supported. *)
+
+Definition initial_fextclk (m : module) : fextclk :=
+  fun x => match x with
+           | S O => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap)
+           | _ => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap)
+           end.
+
+(*Definition module_run (n : nat) (m : module) : res assocmap :=
+  mi_run (initial_fextclk m) empty_assocmap (mod_body m) n.*)
 
 Local Close Scope error_monad_scope.
 
@@ -463,4 +584,42 @@ Proof.
       assumption.
 Qed.
 
+ *)
+
+Definition genv := Genv.t unit unit.
+
+Inductive step : state -> state -> Prop :=
+| step_module :
+    forall m stvar stvar' cycle f assoc0 assoc1 assoc2 nbassoc,
+    mis_stepp (f cycle) (mkassociations assoc0 empty_assocmap)
+              m.(mod_body)
+              (mkassociations assoc1 nbassoc) ->
+    assoc2 = merge_assocmap nbassoc assoc1 ->
+    Some stvar' = assoc2!(fst m.(mod_state)) ->
+    step (State m assoc0 empty_assocmap f cycle stvar)
+         (State m assoc2 empty_assocmap f (S cycle) stvar')
+| step_finish :
+    forall m assoc f cycle stvar result,
+    assoc!(fst m.(mod_finish)) = Some (1'h"1") ->
+    assoc!(fst m.(mod_return)) = Some result ->
+    step (State m assoc empty_assocmap f cycle stvar)
+         (Finishstate result).
+Hint Constructors step : verilog.
+
+(*Inductive initial_state (m: module): state -> Prop :=
+| initial_state_intro:
+    forall hmi tmi,
+    hmi::tmi = mod_body m ->
+    initial_state m (State m hmi tmi empty_assocmap empty_assocmap (initial_fextclk m) O xH).
+
+(** A final state is a [Returnstate] with an empty call stack. *)
+
+Inductive final_state: state -> Integers.int -> Prop :=
+  | final_state_intro: forall v,
+      final_state (Finishstate v) (valueToInt v).
+
+(** The small-step semantics for a module. *)
+
+Definition semantics (p: module) :=
+  Semantics step (initial_state p) final_state (Genv.empty_genv unit unit nil).
 *)