Add Verilog semantics with new Verilog module

1 files changed, 326 insertions, 33 deletions

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index b9200b7..0315cb7 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -21,38 +21,44 @@ From Coq Require Import
   FSets.FMapPositive
   Program.Basics
   PeanoNat
-  ZArith.
+  ZArith
+  Lists.List
+  Program.
 
-From bbv Require Word.
+Import ListNotations.
 
-From coqup.common Require Import Coquplib Show.
+From coqup Require Import common.Coquplib common.Show verilog.Value.
 
 From compcert Require Integers.
+From compcert Require Import Errors.
 
-Import ListNotations.
+Notation "a ! b" := (PositiveMap.find b a) (at level 1).
 
 Definition reg : Type := positive.
+Definition node : Type := positive.
 Definition szreg : Type := reg * nat.
 
-Record value : Type := mkvalue {
-  vsize : nat;
-  vword : Word.word vsize
-}.
+Definition assoclist : Type := PositiveMap.t value.
+
+(** * Verilog AST
+
+The Verilog AST is defined here, which is the target language of the
+compilation.
 
-Definition posToValue (p : positive) : value :=
-  let size := Z.to_nat (Z.succ (log_inf p)) in
-  mkvalue size (Word.posToWord size p).
+** Value
 
-Definition ZToValue (s : nat) (z : Z) : value :=
-  mkvalue s (Word.ZToWord s z).
+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 intToValue (i : Integers.int) : value :=
-  mkvalue 32%nat (Word.ZToWord 32%nat (Integers.Int.unsigned i)).
+Definition estate : Type := assoclist * assoclist.
 
-Definition valueToZ (v : value) : Z :=
-  Word.uwordToZ v.(vword).
+(** ** Binary Operators
 
-Definition state : Type := PositiveMap.t value * PositiveMap.t value.
+These are the binary operations that can be represented in Verilog. Ideally,
+multiplication and division would be done by custom modules which could al so be
+scheduled properly. However, for now every Verilog operator is assumed to take
+one clock cycle. *)
 
 Inductive binop : Type :=
 | Vadd : binop  (** addition (binary [+]) *)
@@ -61,7 +67,7 @@ Inductive binop : Type :=
 | Vdiv : binop  (** division (binary [/]) *)
 | Vdivu : binop  (** division unsigned (binary [/]) *)
 | Vmod : binop  (** remainder ([%]) *)
-| Vmodu : binop  (** remainder unsigned ([/]) *)
+| Vmodu : binop  (** remainder unsigned ([%]) *)
 | Vlt : binop   (** less than ([<]) *)
 | Vltu : binop   (** less than unsigned ([<]) *)
 | Vgt : binop   (** greater than ([>]) *)
@@ -76,12 +82,16 @@ Inductive binop : Type :=
 | Vor : binop   (** or (binary [|]) *)
 | Vxor : binop  (** xor (binary [^|]) *)
 | Vshl : binop  (** shift left ([<<]) *)
-| Vshr : binop. (** shift left ([<<]) *)
+| Vshr : binop. (** shift right ([>>]) *)
+
+(** ** Unary Operators *)
 
 Inductive unop : Type :=
 | Vneg  (** negation ([~]) *)
 | Vnot. (** not operation [!] *)
 
+(** ** Expressions *)
+
 Inductive expr : Type :=
 | Vlit : value -> expr
 | Vvar : reg -> expr
@@ -90,35 +100,54 @@ Inductive expr : Type :=
 | Vternary : expr -> expr -> expr -> expr.
 
 Definition posToExpr (p : positive) : expr :=
-  Vlit (posToValue p).
+  Vlit (posToValueAuto p).
+
+(** ** Statements *)
 
 Inductive stmnt : Type :=
 | Vskip : stmnt
-| Vseq : list stmnt -> stmnt
+| Vseq : stmnt -> stmnt -> stmnt
 | Vcond : expr -> stmnt -> stmnt -> stmnt
-| Vcase : expr -> list (expr * stmnt) -> stmnt
+| Vcase : expr -> list (expr * stmnt) -> option stmnt -> stmnt
 | Vblock : expr -> expr -> stmnt
 | Vnonblock : expr -> expr -> stmnt.
 
-(** [edge] is not part of [stmnt] in this formalisation because is closer to the
-    semantics that are used. *)
+(** ** Edges
+
+These define when an always block should be triggered, for example if the always
+block should be triggered synchronously at the clock edge, or asynchronously for
+combinational logic.
+
+[edge] is not part of [stmnt] in this formalisation because is closer to the
+semantics that are used. *)
+
 Inductive edge : Type :=
 | Vposedge : reg -> edge
 | Vnegedge : reg -> edge
 | Valledge : edge
 | Voredge : edge -> edge -> edge.
 
+(** ** Module Items
+
+Module items can either be declarations ([Vdecl]) or always blocks ([Valways]).
+The declarations are always register declarations as combinational logic can be
+done using combinational always block instead of continuous assignments. *)
+
 Inductive module_item : Type :=
 | Vdecl : reg -> nat -> module_item
 | Valways : edge -> stmnt -> module_item.
 
-(** [mod_start] If set, starts the computations in the module. *)
-(** [mod_reset] If set, reset the state in the module. *)
-(** [mod_clk] The clock that controls the computation in the module. *)
-(** [mod_args] The arguments to the module. *)
-(** [mod_finish] Bit that is set if the result is ready. *)
-(** [mod_return] The return value that was computed. *)
-(** [mod_body] The body of the module, including the state machine. *)
+(** The main module type containing all the important control signals
+
+- [mod_start] If set, starts the computations in the module.
+- [mod_reset] If set, reset the state in the module.
+- [mod_clk] The clock that controls the computation in the module.
+- [mod_args] The arguments to the module.
+- [mod_finish] Bit that is set if the result is ready.
+- [mod_return] The return value that was computed.
+- [mod_body] The body of the module, including the state machine.
+*)
+
 Record module : Type := mkmodule {
   mod_start : szreg;
   mod_reset : szreg;
@@ -132,7 +161,271 @@ Record module : Type := mkmodule {
 (** Convert a [positive] to an expression directly, setting it to the right
     size. *)
 Definition posToLit (p : positive) : expr :=
-  Vlit (posToValue p).
+  Vlit (posToValueAuto p).
 
 Coercion Vlit : value >-> expr.
 Coercion Vvar : reg >-> expr.
+
+Inductive state: Type :=
+| State:
+    forall (assoc: assoclist)
+           (nbassoc: assoclist),
+    state
+| Callstate: state
+| Returnstate: state.
+
+Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value :=
+  match op with
+  | Vadd => vplus
+  | Vsub => vminus
+  | Vmul => vmul
+  | Vdiv => vdivs
+  | Vdivu => vdiv
+  | Vmod => vmods
+  | Vmodu => vmod
+  | Vlt => vlts
+  | Vltu => vlt
+  | Vgt => vgts
+  | Vgtu => vgt
+  | Vle => vles
+  | Vleu => vle
+  | Vge => vges
+  | Vgeu => vge
+  | Veq => veq
+  | Vne => vne
+  | Vand => vand
+  | Vor => vor
+  | Vxor => vxor
+  | Vshl => vshl
+  | Vshr => vshr
+  end.
+
+Definition unop_run (op : unop) : value -> value :=
+  match op with
+  | Vneg => vnot
+  | Vnot => vbitneg
+  end.
+
+Inductive expr_runp : assoclist -> expr -> value -> Prop :=
+  | erun_Vlit :
+      forall a v,
+      expr_runp a (Vlit v) v
+  | erun_Vvar :
+      forall assoc v r,
+      assoc!r = Some v ->
+      expr_runp assoc (Vvar r) v
+  | erun_Vbinop :
+      forall a op l r lv rv oper EQ,
+      expr_runp a l lv ->
+      expr_runp a r rv ->
+      oper = binop_run op ->
+      expr_runp a (Vbinop op l r) (oper lv rv EQ)
+  | erun_Vunop :
+      forall a u vu op oper,
+      expr_runp a u vu ->
+      oper = unop_run op ->
+      expr_runp a (Vunop op u) (oper vu)
+  | erun_Vternary_true :
+      forall a c t f vc vt,
+      expr_runp a c vc ->
+      expr_runp a t vt ->
+      valueToBool vc = true ->
+      expr_runp a (Vternary c t f) vt
+  | erun_Vternary_false :
+      forall a c t f vc vf,
+      expr_runp a c vc ->
+      expr_runp a f vf ->
+      valueToBool vc = false ->
+      expr_runp a (Vternary c t f) vf.
+
+Definition handle_opt {A : Type} (err : errmsg) (val : option A)
+  : res A :=
+  match val with
+  | Some a => OK a
+  | None => Error err
+  end.
+
+Local Open Scope error_monad_scope.
+
+Fixpoint expr_run (assoc : assoclist) (e : expr)
+  {struct e} : res value :=
+  match e with
+  | Vlit v => OK v
+  | Vvar r => handle_opt (msg "Verilog: reg not in assoc map") assoc!r
+  | Vbinop op l r =>
+    let lv := expr_run assoc l in
+    let rv := expr_run assoc r in
+    let oper := binop_run op in
+    do lv' <- lv;
+    do rv' <- rv;
+    handle_opt (msg "Verilog: sizes are not equal")
+               (eq_to_opt lv' rv' (oper lv' rv'))
+  | Vunop op e =>
+    let oper := unop_run op in
+    do ev <- expr_run assoc e;
+    OK (oper ev)
+  | Vternary c t f =>
+    do cv <- expr_run assoc c;
+    if valueToBool cv then expr_run assoc t else expr_run assoc f
+  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. *)
+
+Definition assign_name (e : expr) : res reg :=
+  match e with
+  | Vvar r => OK r
+  | _ => Error (msg "Verilog: expression not supported on lhs of assignment")
+  end.
+
+Fixpoint find_case_stmnt (a : assoclist) (v : value) (cl : list (expr * stmnt))
+         {struct cl} : res stmnt :=
+  match cl with
+  | (e, s)::xs =>
+    do v' <- expr_run a e;
+      match eq_to_opt v v' (veq v v') with
+      | Some eq => if valueToBool eq then OK s else find_case_stmnt a v xs
+      | None => Error (msg "Verilog: equality check sizes not equal")
+      end
+  | _ => Error (msg "Verilog: No more statements in case statement")
+  end.
+
+Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
+  match n with
+  | S n' =>
+    match st with
+    | Vskip => OK s
+    | Vseq s1 s2 =>
+      do s' <- stmnt_run' n' s s1;
+      stmnt_run' n' s' s2
+    | Vcond c st sf =>
+      match s with
+      | State assoc _ =>
+        do cv <- expr_run assoc c;
+        if valueToBool cv
+        then stmnt_run' n' s st
+        else stmnt_run' n' s sf
+      | _ => Error (msg "Verilog: stmnt execution in wrong state")
+      end
+    | Vcase e cl defst =>
+      match s with
+      | State a _ =>
+        do v <- expr_run a e;
+        do st' <- find_case_stmnt a v cl;
+        match find_case_stmnt a v cl with
+        | OK st' => stmnt_run' n' s st'
+        | _ =>
+          match option_map (stmnt_run' n' s) defst with
+          | Some s => s
+          | None => Error (msg "Verilog: no case was matched")
+          end
+        end
+      | _ => Error (msg "Verilog: stmnt execution in wrong state")
+      end
+    | Vblock lhs rhs =>
+      match s with
+      | State assoc nbassoc =>
+        do name <- assign_name lhs;
+        do rhse <- expr_run assoc rhs;
+        OK (State (PositiveMap.add name rhse assoc) nbassoc)
+      | _ => Error (msg "Verilog: stmnt exectution in wrong state")
+      end
+    | Vnonblock lhs rhs =>
+      match s with
+      | State assoc nbassoc =>
+        do name <- assign_name lhs;
+        do rhse <- expr_run assoc rhs;
+        OK (State assoc (PositiveMap.add name rhse nbassoc))
+      | _ => Error (msg "Verilog: stmnt execution in wrong state")
+      end
+    end
+  | _ => Error (msg "Verilog: stmnt_run reached bottom")
+  end.
+
+Fixpoint stmnt_height (st : stmnt) {struct st} : nat :=
+  match st with
+  | Vskip => 1
+  | Vseq s1 s2 => stmnt_height s1 + stmnt_height s2
+  | Vcond _ s1 s2 => Nat.max (stmnt_height s1) (stmnt_height s2)
+  | Vcase _ ls (Some st) =>
+    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 module_step (s : state) (m : list module_item) {struct m} : res state :=
+  match m with
+  | (Valways _ st)::ls =>
+    do s' <- stmnt_run s st;
+    module_step s' ls
+  | (Vdecl _ _)::ls => module_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.
+
+Fixpoint module_step_commit (assoc : assoclist) (m : list module_item) : res assoclist :=
+  match module_step (State assoc empty_assoclist) m with
+  | OK (State assoc' nbassoc) =>
+    OK (merge_assoclist nbassoc assoc')
+  | Error msg => Error msg
+  | _ => Error (msg "Returned in the wrong state")
+  end.
+
+Fixpoint module_run (assoc : assoclist) (m : list module_item) (n : nat)
+         {struct n} : res assoclist :=
+  match n with
+  | S n' =>
+    do assoc' <- module_run assoc m n';
+    module_step_commit assoc' m
+  | O => OK assoc
+  end.
+
+Local Close Scope error_monad_scope.
+
+(* Theorem value_eq_size_if_eq:
+  forall lv rv EQ,
+  vsize lv = vsize rv -> value_eq_size lv rv = left EQ.
+Proof. Admitted.
+
+Theorem expr_run_same:
+  forall assoc e v, expr_run assoc e = OK v <-> expr_runp assoc e v.
+Proof.
+  split; generalize dependent v; generalize dependent assoc.
+  - induction e.
+    + intros. inversion H. constructor.
+    + intros. inversion H. constructor. assumption.
+    + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (expr_run assoc e2) eqn:?.
+      unfold eq_to_opt in H1. destruct (value_eq_size v0 v1) eqn:?. inversion H1.
+      constructor. apply IHe1. assumption. apply IHe2. assumption. reflexivity. discriminate. discriminate.
+      discriminate.
+    + intros. inversion H. destruct (expr_run assoc e) eqn:?. unfold option_map in H1.
+      inversion H1. constructor. apply IHe. assumption. reflexivity. discriminate.
+    + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (valueToBool v0) eqn:?.
+      eapply erun_Vternary_true. apply IHe1. eassumption. apply IHe2. eassumption. assumption.
+      eapply erun_Vternary_false. apply IHe1. eassumption. apply IHe3. eassumption. assumption.
+      discriminate.
+  - induction e.
+    + intros. inversion H. reflexivity.
+    + intros. inversion H. subst. simpl. assumption.
+    + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4.
+      apply IHe2 in H6. rewrite H6. unfold eq_to_opt. assert (vsize lv = vsize rv).
+      apply EQ. apply (value_eq_size_if_eq lv rv EQ) in H0. rewrite H0. reflexivity.
+    + intros. inversion H. subst. simpl. destruct (expr_run assoc e) eqn:?. simpl.
+      apply IHe in H3. rewrite Heqo in H3.
+      inversion H3. subst. reflexivity. apply IHe in H3. rewrite Heqo in H3. discriminate.
+    + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7.
+      apply IHe2 in H6. rewrite H6. reflexivity.
+      subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. apply IHe3.
+      assumption.
+Qed.
+
+*)