Add CompCert semantics for Verilog

1 files changed, 152 insertions, 81 deletions

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