aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/Verilog.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/verilog/Verilog.v')
-rw-r--r--src/verilog/Verilog.v335
1 files changed, 247 insertions, 88 deletions
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).
*)
generated by cgit (git 2.34.1) at 2024-07-08 02:41:14 +0000