aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls')
-rw-r--r--src/hls/HTL.v2
-rw-r--r--src/hls/HTLgenproof.v28
-rw-r--r--src/hls/Verilog.v32
-rw-r--r--src/hls/Veriloggen.v4
-rw-r--r--src/hls/Veriloggenproof.v32
5 files changed, 80 insertions, 18 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 620ef14..cfc7aa3 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -120,6 +120,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
ctrl
(Verilog.mkassociations basr1 nasr1)
(Verilog.mkassociations basa1 nasa1) ->
+ basr1!(mod_reset m) = Some (ZToValue 0) ->
+ basr1!(mod_finish m) = Some (ZToValue 0) ->
basr1!(m.(mod_st)) = Some (posToValue st) ->
Verilog.stmnt_runp f
(Verilog.mkassociations basr1 nasr1)
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index afc827d..1fbc361 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -1080,12 +1080,13 @@ Section CORRECTNESS.
crush.
econstructor.
econstructor.
- econstructor.
-
- all: invert MARR; big_tac.
- inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia.
+ all: try constructor; invert MARR; big_tac.
+ inv CONST. simplify. assumption.
+ inv CONST. simplify. assumption.
+ inv CONST. constructor. simplify; rewrite AssocMap.gso; auto; lia.
+ simplify; rewrite AssocMap.gso; auto; lia.
Unshelve. exact tt.
Qed.
Hint Resolve transl_inop_correct : htlproof.
@@ -1113,7 +1114,10 @@ Section CORRECTNESS.
econstructor; simpl; trivial.
constructor; trivial.
econstructor; simpl; eauto.
- simpl. econstructor. econstructor.
+ simpl.
+ inv CONST. assumption.
+ inv CONST. assumption.
+ econstructor. econstructor.
apply H5. simplify.
all: big_tac.
@@ -2448,7 +2452,10 @@ Section CORRECTNESS.
eapply eval_cond_correct; eauto. intros.
intros. eapply RTL.max_reg_function_use. apply H22. auto.
econstructor. auto.
- simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl.
+ simpl.
+ inv CONST. assumption.
+ inv CONST. assumption.
+ econstructor. unfold Verilog.merge_regs. unfold_merge. simpl.
apply AssocMap.gss.
inv MARR. inv CONST.
@@ -2465,7 +2472,10 @@ Section CORRECTNESS.
eapply eval_cond_correct; eauto. intros.
intros. eapply RTL.max_reg_function_use. apply H22. auto.
econstructor. auto.
- simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl.
+ simpl.
+ inv CONST. assumption.
+ inv CONST. assumption.
+ econstructor. unfold Verilog.merge_regs. unfold_merge. simpl.
apply AssocMap.gss.
inv MARR. inv CONST.
@@ -2514,6 +2524,8 @@ Section CORRECTNESS.
inv CONST; assumption.
inv CONST; assumption.
constructor.
+ inv CONST. assumption.
+ inv CONST. assumption.
econstructor; simpl; trivial.
econstructor; simpl; trivial.
constructor.
@@ -2545,6 +2557,8 @@ Section CORRECTNESS.
inv CONST; assumption.
inv CONST; assumption.
constructor.
+ inv CONST. assumption.
+ inv CONST. assumption.
econstructor; simpl; trivial.
econstructor; simpl; trivial.
constructor. constructor. constructor.
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index e5f86d5..6b4004f 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -286,6 +286,11 @@ Inductive state : Type :=
(st : node)
(reg_assoc : assocmap_reg)
(arr_assoc : assocmap_arr), state
+| Resetstate :
+ forall (stack : list stackframe)
+ (m : module)
+ (reg_assoc : assocmap_reg)
+ (arr_assoc : assocmap_arr), state
| Returnstate :
forall (res : list stackframe)
(v : value), state
@@ -724,6 +729,20 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
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')
+| step_reset :
+ forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf g,
+ asr!(m.(mod_reset)) = Some (ZToValue 1) ->
+ asr!(m.(mod_finish)) = Some (ZToValue 0) ->
+ mis_stepp f (mkassociations asr empty_assocmap)
+ (mkassociations asa (empty_stack m))
+ m.(mod_body)
+ (mkassociations basr1 nasr1)
+ (mkassociations basa1 nasa1) ->
+ asr' = merge_regs nasr1 basr1 ->
+ asa' = merge_arrs nasa1 basa1 ->
+ asr'!(m.(mod_st)) = Some stval ->
+ valueToPos stval = pstval ->
+ step g (Resetstate sf m asr asa) Events.E0 (State sf m pstval asr' asa')
| step_finish :
forall asr asa sf retval m st g,
asr!(m.(mod_finish)) = Some (ZToValue 1) ->
@@ -732,11 +751,10 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
| step_call :
forall g res m args,
step g (Callstate res m args) Events.E0
- (State res m m.(mod_entrypoint)
- (AssocMap.set (mod_reset m) (ZToValue 0)
+ (Resetstate res m
+ (AssocMap.set (mod_reset m) (ZToValue 1)
(AssocMap.set (mod_finish m) (ZToValue 0)
- (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint))
- (init_params args m.(mod_args)))))
+ (init_params args m.(mod_args))))
(empty_stack m))
| step_return :
forall g m asr i r sf pc mst asa,
@@ -883,9 +901,9 @@ Lemma semantics_determinate :
Proof.
intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify.
- invert H; invert H0; constructor. (* Traces are always empty *)
- - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst.
- pose proof (mis_stepp_determinate H5 H15).
- crush.
+ - invert H; invert H0; crush; assert (f = f0) by (destruct f; destruct f0; auto); subst.
+ pose proof (mis_stepp_determinate H5 H15). crush.
+ pose proof (mis_stepp_determinate H3 H10). crush.
- constructor. invert H; crush.
- invert H; invert H0; unfold ge0, ge1 in *; crush.
- red; simplify; intro; invert H0; invert H; crush.
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v
index a0be0fa..b497115 100644
--- a/src/hls/Veriloggen.v
+++ b/src/hls/Veriloggen.v
@@ -44,7 +44,9 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1)))
(Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint))))
(Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip)))
- :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
+ :: Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 0)))
+ (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
+ Vskip)
:: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
Verilog.mkmodule m.(mod_start)
diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v
index 9abbd4b..1f7126f 100644
--- a/src/hls/Veriloggenproof.v
+++ b/src/hls/Veriloggenproof.v
@@ -300,7 +300,12 @@ Section CORRECTNESS.
}
apply Maps.PTree.elements_correct. eassumption. eassumption.
- econstructor. econstructor.
+ econstructor. econstructor. econstructor.
+ econstructor. econstructor. simplify.
+ unfold find_assocmap, AssocMapExt.get_default.
+ rewrite H5. trivial.
+ constructor. simplify. unfold valueToBool, boolToValue, Int.eq, uvalueToZ, natToValue.
+ rewrite zeq_true. rewrite Int.unsigned_repr. auto. lia.
eapply transl_list_correct.
intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto.
@@ -319,9 +324,30 @@ Section CORRECTNESS.
- econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption.
constructor; assumption.
- - econstructor; split. apply Smallstep.plus_one. constructor.
+ - econstructor; split. eapply Smallstep.plus_two. constructor.
+ econstructor.
+ apply AssocMap.gss.
+ rewrite AssocMap.gso.
+ apply AssocMap.gss. admit.
+ econstructor.
+ constructor. eapply stmnt_runp_Vcond_true. econstructor. econstructor. simplify.
+ unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gss. auto.
+ econstructor. simplify. unfold valueToBool, boolToValue, Int.eq, uvalueToZ, natToValue.
+ rewrite zeq_true. rewrite Int.unsigned_repr. auto. simpl. unfold_constants. lia.
+ econstructor. econstructor. econstructor.
+ econstructor. econstructor.
+ eapply stmnt_runp_Vcond_false. econstructor. econstructor. simplify.
+ unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gss. auto.
+ econstructor. simplify. unfold valueToBool, boolToValue, Int.eq, uvalueToZ, natToValue.
+ rewrite zeq_false. rewrite Int.unsigned_repr. auto. simpl. unfold_constants. lia.
+ unfold ZToValue. rewrite !Int.unsigned_repr; unfold_constants; try lia.
+ econstructor.
+ apply mis_stepp_decl. trivial. trivial. simplify.
+ unfold merge_regs. unfold_merge. apply AssocMap.gss. auto. auto.
+ rewrite valueToPos_posToValue.
+ simplify. unfold merge_regs. unfold_merge.
+
- constructor. constructor.
- inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial.
apply match_state. assumption.
generated by cgit (git 2.34.1) at 2024-07-01 20:16:44 +0000