aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--_CoqProject2
-rw-r--r--src/translation/HTLgen.v14
-rw-r--r--src/translation/Veriloggen.v5
-rw-r--r--src/verilog/HTL.v21
-rw-r--r--src/verilog/Verilog.v57
5 files changed, 50 insertions, 49 deletions
diff --git a/_CoqProject b/_CoqProject
index a1026ed..7965da9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -14,4 +14,4 @@
-R lib/CompCert/flocq compcert.flocq
-R lib/CompCert/lib compcert.lib
-R lib/CompCert/x86 compcert.x86
--R lib/CompCert/x86_32 compcert.x86_64
+-R lib/CompCert/x86_32 compcert.x86_32
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index d35a296..1c67fe7 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -131,7 +131,7 @@ Lemma declare_reg_state_incr :
s.(st_st)
s.(st_freshreg)
s.(st_freshstate)
- (AssocMap.set r (i, Scalar sz) s.(st_scldecls))
+ (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
s.(st_arrdecls)
s.(st_datapath)
s.(st_controllogic)).
@@ -142,7 +142,7 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
s.(st_st)
s.(st_freshreg)
s.(st_freshstate)
- (AssocMap.set r (i, Scalar sz) s.(st_scldecls))
+ (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
s.(st_arrdecls)
s.(st_datapath)
s.(st_controllogic))
@@ -393,7 +393,7 @@ Lemma create_reg_state_incr:
s.(st_st)
(Pos.succ (st_freshreg s))
(st_freshstate s)
- (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls))
+ (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
s.(st_arrdecls)
(st_datapath s)
(st_controllogic s)).
@@ -405,7 +405,7 @@ Definition create_reg (i : option io) (sz : nat) : mon reg :=
s.(st_st)
(Pos.succ r)
(st_freshstate s)
- (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls))
+ (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
(st_arrdecls s)
(st_datapath s)
(st_controllogic s))
@@ -418,7 +418,7 @@ Lemma create_arr_state_incr:
(Pos.succ (st_freshreg s))
(st_freshstate s)
s.(st_scldecls)
- (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls))
+ (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
(st_datapath s)
(st_controllogic s)).
Proof. constructor; simpl; auto with htlh. Qed.
@@ -430,7 +430,7 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
(Pos.succ r)
(st_freshstate s)
s.(st_scldecls)
- (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls))
+ (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
(st_datapath s)
(st_controllogic s))
(create_arr_state_incr s sz ln i).
@@ -466,7 +466,7 @@ Definition max_state (f: function) : state :=
mkstate st
(Pos.succ st)
(Pos.succ (max_pc_function f))
- (AssocMap.set st (None, Scalar 32) (st_scldecls (init_state st)))
+ (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st)))
(st_arrdecls (init_state st))
(st_datapath (init_state st))
(st_controllogic (init_state st)).
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index efe3565..2b9974b 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -29,13 +29,13 @@ Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr
Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item :=
match scldecl with
- | (r, (io, Scalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl'
+ | (r, (io, VScalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl'
| nil => nil
end.
Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item :=
match arrdecl with
- | (r, (io, Array sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl'
+ | (r, (io, VArray sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl'
| nil => nil
end.
@@ -56,6 +56,7 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
m.(mod_return)
m.(mod_st)
m.(mod_stk)
+ m.(mod_stk_len)
m.(mod_params)
body
m.(mod_entrypoint).
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index c509248..8149ddf 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -17,7 +17,7 @@
*)
From Coq Require Import FSets.FMapPositive.
-From coqup Require Import Coquplib Value AssocMap.
+From coqup Require Import Coquplib Value AssocMap Array.
From coqup Require Verilog.
From compcert Require Events Globalenvs Smallstep Integers Values.
From compcert Require Import Maps.
@@ -66,13 +66,8 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
| _, _ => empty_assocmap
end.
-Fixpoint zeroes' (acc : list value) (n : nat) : list value :=
- match n with
- | O => acc
- | S n => zeroes' ((NToValue 32 0)::acc) n
- end.
-
-Definition zeroes : nat -> list value := zeroes' nil.
+Definition empty_stack (m : module) : AssocMap.t (Array value) :=
+ (AssocMap.set m.(mod_stk) (Verilog.zeroes m.(mod_stk_len)) (AssocMap.empty (Array value))).
(** * Operational Semantics *)
@@ -84,7 +79,7 @@ Inductive stackframe : Type :=
(m : module)
(pc : node)
(reg_assoc : assocmap)
- (arr_assoc : AssocMap.t (list value)),
+ (arr_assoc : AssocMap.t (Array value)),
stackframe.
Inductive state : Type :=
@@ -93,7 +88,7 @@ Inductive state : Type :=
(m : module)
(st : node)
(reg_assoc : assocmap)
- (arr_assoc : AssocMap.t (list value)), state
+ (arr_assoc : AssocMap.t (Array value)), state
| Returnstate :
forall (res : list stackframe)
(v : value), state
@@ -114,7 +109,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
m.(mod_datapath)!st = Some data ->
Verilog.stmnt_runp f
(Verilog.mkassociations asr empty_assocmap)
- (Verilog.mkassociations asa (AssocMap.empty (list value)))
+ (Verilog.mkassociations asa (empty_stack m))
ctrl
(Verilog.mkassociations basr1 nasr1)
(Verilog.mkassociations basa1 nasa1) ->
@@ -125,7 +120,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
(Verilog.mkassociations basr2 nasr2)
(Verilog.mkassociations basa2 nasa2) ->
asr' = merge_assocmap nasr2 basr2 ->
- asa' = AssocMapExt.merge (list value) nasa2 basa2 ->
+ asa' = AssocMapExt.merge (Array value) nasa2 basa2 ->
asr'!(m.(mod_st)) = Some stval ->
valueToPos stval = pstval ->
step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
@@ -140,7 +135,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
(State res m m.(mod_entrypoint)
(AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint))
(init_regs args m.(mod_params)))
- (AssocMap.set m.(mod_stk) (zeroes m.(mod_stk_len)) (AssocMap.empty (list value))))
+ (empty_stack m))
| step_return :
forall g m asr asa i r sf pc mst,
mst = mod_st m ->
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 8b83d49..3ab3f10 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -27,7 +27,7 @@ From Coq Require Import
Import ListNotations.
-From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap.
+From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap Array.
From compcert Require Integers Events.
From compcert Require Import Errors Smallstep Globalenvs.
@@ -48,38 +48,31 @@ Record associations (A : Type) : Type :=
}.
Definition reg_associations := associations value.
-Definition arr_associations := associations (list value).
+Definition arr_associations := associations (Array value).
-Definition assocmap_arr := AssocMap.t (list value).
+Definition assocmap_arr := AssocMap.t (Array value).
Definition merge_associations {A : Type} (assoc : associations A) :=
mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking))
(AssocMap.empty A).
-Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : value :=
+Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
match a ! r with
- | None => natToValue 32 0
- | Some arr => nth i arr (natToValue 32 0)
+ | None => None
+ | Some arr => array_get_error i arr
end.
-Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A :=
- match i, l with
- | _, nil => nil
- | S n, h :: t => h :: list_set n x t
- | O, h :: t => x :: t
- end.
-
-Definition assocmap_l_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
+Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
match a ! r with
| None => a
- | Some arr => AssocMap.set r (list_set i v arr) a
+ | Some arr => a # r <- (array_set i v arr)
end.
Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
- mkassociations (assocmap_l_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking).
+ mkassociations (arr_assocmap_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking).
Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
- mkassociations asa.(assoc_blocking) (assocmap_l_set r i v asa.(assoc_nonblocking)).
+ mkassociations asa.(assoc_blocking) (arr_assocmap_set r i v asa.(assoc_nonblocking)).
Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking).
@@ -87,8 +80,8 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)).
-Inductive scl_decl : Type := Scalar (sz : nat).
-Inductive arr_decl : Type := Array (sz : nat) (ln : nat).
+Inductive scl_decl : Type := VScalar (sz : nat).
+Inductive arr_decl : Type := VArray (sz : nat) (ln : nat).
(** * Verilog AST
@@ -217,6 +210,7 @@ Record module : Type := mkmodule {
mod_return : reg;
mod_st : reg; (**r Variable that defines the current state, it should be internal. *)
mod_stk : reg;
+ mod_stk_len : nat;
mod_args : list reg;
mod_body : list module_item;
mod_entrypoint : node;
@@ -234,7 +228,7 @@ Definition posToLit (p : positive) : expr :=
Coercion Vlit : value >-> expr.
Coercion Vvar : reg >-> expr.
-Definition fext := AssocMap.t value.
+Definition fext := assocmap.
Definition fextclk := nat -> fext.
(** ** State
@@ -272,7 +266,7 @@ Inductive state : Type :=
(m : module)
(st : node)
(reg_assoc : assocmap)
- (arr_assoc : AssocMap.t (list value)), state
+ (arr_assoc : AssocMap.t (Array value)), state
| Returnstate :
forall (res : list stackframe)
(v : value), state
@@ -324,7 +318,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop
| erun_Vvari :
forall fext reg stack v iexp i r,
expr_runp fext reg stack iexp i ->
- arr_assocmap_lookup stack r (valueToNat i) = v ->
+ arr_assocmap_lookup stack r (valueToNat i) = Some v ->
expr_runp fext reg stack (Vvari r iexp) v
| erun_Vinputvar :
forall fext reg stack r v,
@@ -690,16 +684,27 @@ Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} :=
Definition genv := Globalenvs.Genv.t fundef unit.
+Fixpoint list_zeroes' (acc : list value) (n : nat) : list value :=
+ match n with
+ | O => acc
+ | S n => list_zeroes' ((NToValue 32 0)::acc) n
+ end.
+
+Definition list_zeroes : nat -> list value := list_zeroes' nil.
+Definition zeroes (n : nat) : Array value := make_array (list_zeroes n).
+Definition empty_stack (m : module) : AssocMap.t (Array value) :=
+ (AssocMap.set m.(mod_stk) (zeroes m.(mod_stk_len)) (AssocMap.empty (Array value))).
+
Inductive step : genv -> state -> Events.trace -> state -> Prop :=
| step_module :
forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g,
mis_stepp f (mkassociations asr empty_assocmap)
- (mkassociations asa (AssocMap.empty (list value)))
+ (mkassociations asa (empty_stack m))
m.(mod_body)
(mkassociations basr1 nasr1)
(mkassociations basa1 nasa1)->
asr' = merge_assocmap nasr1 basr1 ->
- asa' = AssocMapExt.merge (list value) nasa1 basa1 ->
+ asa' = AssocMapExt.merge (Array value) nasa1 basa1 ->
asr'!(m.(mod_st)) = Some stval ->
valueToPos stval = pstval ->
step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
@@ -714,13 +719,13 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
(State res m m.(mod_entrypoint)
(AssocMap.set m.(mod_st) (posToValue 32 m.(mod_entrypoint))
(init_params args m.(mod_args)))
- (AssocMap.empty (list value)))
+ (empty_stack m))
| step_return :
forall g m asr i r sf pc mst,
mst = mod_st m ->
step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0
(State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
- (AssocMap.empty (list value))).
+ (empty_stack m)).
Hint Constructors step : verilog.
Inductive initial_state (p: program): state -> Prop :=
generated by cgit (git 2.34.1) at 2024-06-29 07:18:39 +0000