aboutsummaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Compiler.v100
-rw-r--r--src/VericertClflags.ml2
-rw-r--r--src/common/IntegerExtra.v287
-rw-r--r--src/extraction/Extraction.v17
-rw-r--r--src/hls/Array.v (renamed from src/verilog/Array.v)0
-rw-r--r--src/hls/AssocMap.v (renamed from src/verilog/AssocMap.v)0
-rw-r--r--src/hls/HTL.v (renamed from src/verilog/HTL.v)0
-rw-r--r--src/hls/HTLBlockgen.v655
-rw-r--r--src/hls/HTLSchedulegen.v42
-rw-r--r--src/hls/HTLgen.v (renamed from src/translation/HTLgen.v)8
-rw-r--r--src/hls/HTLgenproof.v (renamed from src/translation/HTLgenproof.v)114
-rw-r--r--src/hls/HTLgenspec.v (renamed from src/translation/HTLgenspec.v)0
-rw-r--r--src/hls/Partition.ml125
-rw-r--r--src/hls/PrintHTL.ml (renamed from src/verilog/PrintHTL.ml)0
-rw-r--r--src/hls/PrintRTLBlock.ml119
-rw-r--r--src/hls/PrintVerilog.ml (renamed from src/verilog/PrintVerilog.ml)0
-rw-r--r--src/hls/PrintVerilog.mli (renamed from src/verilog/PrintVerilog.mli)0
-rw-r--r--src/hls/RTLBlock.v170
-rw-r--r--src/hls/RTLBlockgen.v32
-rw-r--r--src/hls/RTLPar.v99
-rw-r--r--src/hls/Schedule.ml610
-rw-r--r--src/hls/Value.v (renamed from src/verilog/Value.v)0
-rw-r--r--src/hls/ValueInt.v (renamed from src/verilog/ValueInt.v)0
-rw-r--r--src/hls/ValueVal.v209
-rw-r--r--src/hls/Verilog.v (renamed from src/verilog/Verilog.v)4
-rw-r--r--src/hls/Veriloggen.v (renamed from src/translation/Veriloggen.v)0
-rw-r--r--src/hls/Veriloggenproof.v (renamed from src/translation/Veriloggenproof.v)0
27 files changed, 2574 insertions, 19 deletions
diff --git a/src/Compiler.v b/src/Compiler.v
index 6efd7a2..8eeea6b 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -51,12 +51,16 @@ From vericert Require
Verilog
Veriloggen
Veriloggenproof
- HTLgen.
+ HTLgen
+ RTLBlock
+ RTLBlockgen
+ HTLSchedulegen.
From compcert Require Import Smallstep.
Parameter print_RTL: Z -> RTL.program -> unit.
Parameter print_HTL: HTL.program -> unit.
+Parameter print_RTLBlock: RTLBlock.program -> unit.
Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
let unused := printer prog in prog.
@@ -80,13 +84,45 @@ Proof.
intros. destruct x; simpl. rewrite print_identity. auto. auto.
Qed.
+Definition total_if {A: Type}
+ (flag: unit -> bool) (f: A -> A) (prog: A) : A :=
+ if flag tt then f prog else prog.
+
+Definition partial_if {A: Type}
+ (flag: unit -> bool) (f: A -> res A) (prog: A) : res A :=
+ if flag tt then f prog else OK prog.
+
+Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.
+
+Definition transf_backend_opt (r : RTL.program) : res Verilog.program :=
+ OK r
+ @@@ Inlining.transf_program
+ @@ print (print_RTL 1)
+ @@ Renumber.transf_program
+ @@ print (print_RTL 2)
+ @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
+ @@ print (print_RTL 3)
+ @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
+ @@ print (print_RTL 4)
+ @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
+ @@ print (print_RTL 5)
+ @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+ @@ print (print_RTL 6)
+ @@@ time "Unused globals" Unusedglob.transform_program
+ @@ print (print_RTL 7)
+ @@@ HTLgen.transl_program
+ @@ print print_HTL
+ @@ Veriloggen.transl_program.
+
Definition transf_backend (r : RTL.program) : res Verilog.program :=
OK r
@@@ Inlining.transf_program
- @@ print (print_RTL 1)
+ @@ print (print_RTL 1)
+ @@ Renumber.transf_program
+ @@ print (print_RTL 2)
@@@ HTLgen.transl_program
- @@ print print_HTL
- @@ Veriloggen.transl_program.
+ @@ print print_HTL
+ @@ Veriloggen.transl_program.
Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
OK p
@@ -96,9 +132,48 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
@@@ Cminorgen.transl_program
@@@ Selection.sel_program
@@@ RTLgen.transl_program
- @@ print (print_RTL 0)
+ @@ print (print_RTL 0)
@@@ transf_backend.
+Definition transf_hls_opt (p : Csyntax.program) : res Verilog.program :=
+ OK p
+ @@@ SimplExpr.transl_program
+ @@@ SimplLocals.transf_program
+ @@@ Cshmgen.transl_program
+ @@@ Cminorgen.transl_program
+ @@@ Selection.sel_program
+ @@@ RTLgen.transl_program
+ @@ print (print_RTL 0)
+ @@@ transf_backend_opt.
+
+Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
+ OK p
+ @@@ SimplExpr.transl_program
+ @@@ SimplLocals.transf_program
+ @@@ Cshmgen.transl_program
+ @@@ Cminorgen.transl_program
+ @@@ Selection.sel_program
+ @@@ RTLgen.transl_program
+ @@@ Inlining.transf_program
+ @@ print (print_RTL 1)
+ @@ Renumber.transf_program
+ @@ print (print_RTL 2)
+ @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
+ @@ print (print_RTL 3)
+ @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
+ @@ print (print_RTL 4)
+ @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
+ @@ print (print_RTL 5)
+ @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+ @@ print (print_RTL 6)
+ @@@ time "Unused globals" Unusedglob.transform_program
+ @@ print (print_RTL 7)
+ @@@ RTLBlockgen.transl_program
+ @@ print print_RTLBlock
+ @@@ HTLSchedulegen.transl_program
+ @@ print print_HTL
+ @@ Veriloggen.transl_program.
+
Local Open Scope linking_scope.
Definition CompCert's_passes :=
@@ -109,6 +184,7 @@ Definition CompCert's_passes :=
::: mkpass Selectionproof.match_prog
::: mkpass RTLgenproof.match_prog
::: mkpass Inliningproof.match_prog
+ ::: mkpass Renumberproof.match_prog
::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program))
::: mkpass Veriloggenproof.match_prog
::: pass_nil _.
@@ -132,8 +208,9 @@ Proof.
destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate.
unfold transf_backend in T. simpl in T. rewrite ! compose_print_identity in T.
destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate.
- destruct (HTLgen.transl_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate.
- set (p9 := Veriloggen.transl_program p8) in *.
+ set (p8 := Renumber.transf_program p7) in *.
+ destruct (HTLgen.transl_program p8) as [p9|e] eqn:P9; simpl in T; try discriminate.
+ set (p10 := Veriloggen.transl_program p9) in *.
unfold match_prog; simpl.
exists p1; split. apply SimplExprproof.transf_program_match; auto.
exists p2; split. apply SimplLocalsproof.match_transf_program; auto.
@@ -142,8 +219,9 @@ Proof.
exists p5; split. apply Selectionproof.transf_program_match; auto.
exists p6; split. apply RTLgenproof.transf_program_match; auto.
exists p7; split. apply Inliningproof.transf_program_match; auto.
- exists p8; split. apply HTLgenproof.transf_program_match; auto.
- exists p9; split. apply Veriloggenproof.transf_program_match; auto.
+ exists p8; split. apply Renumberproof.transf_program_match; auto.
+ exists p9; split. apply HTLgenproof.transf_program_match; auto.
+ exists p10; split. apply Veriloggenproof.transf_program_match; auto.
inv T. reflexivity.
Qed.
@@ -171,7 +249,7 @@ Ltac DestructM :=
destruct H as (p & M & MM); clear H
end.
repeat DestructM. subst tp.
- assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p9)).
+ assert (F: forward_simulation (Cstrategy.semantics p) (Verilog.semantics p10)).
{
eapply compose_forward_simulations.
eapply SimplExprproof.transl_program_correct; eassumption.
@@ -188,6 +266,8 @@ Ltac DestructM :=
eapply compose_forward_simulations.
eapply Inliningproof.transf_program_correct; eassumption.
eapply compose_forward_simulations.
+ eapply Renumberproof.transf_program_correct; eassumption.
+ eapply compose_forward_simulations.
eapply HTLgenproof.transf_program_correct. eassumption.
eapply Veriloggenproof.transf_program_correct; eassumption.
}
diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml
index ca591de..26b4053 100644
--- a/src/VericertClflags.ml
+++ b/src/VericertClflags.ml
@@ -4,3 +4,5 @@ let option_hls = ref true
let option_debug_hls = ref false
let option_initial = ref false
let option_dhtl = ref false
+let option_drtlblock = ref false
+let option_hls_schedule = ref false
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index c9b5dbd..f44cac2 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -362,4 +362,291 @@ Module IntExtra.
rewrite testbit_repr; auto.
Abort.
+ Lemma div_divs_equiv :
+ forall x y,
+ signed x >= 0 ->
+ signed y >= 0 ->
+ divs x y = divu x y.
+ Proof.
+ unfold divs, divu.
+ intros.
+ rewrite !signed_eq_unsigned;
+ try rewrite Zquot.Zquot_Zdiv_pos; try reflexivity;
+ lazymatch goal with
+ | |- unsigned _ <= max_signed =>
+ solve [rewrite <- signed_positive; assumption]
+ | |- 0 <= unsigned _ => solve [apply unsigned_range_2]
+ end.
+ Qed.
+
+ Lemma neg_signed' :
+ forall x : int,
+ unsigned x <> 2147483648 ->
+ signed (neg x) = - signed x.
+ Proof.
+ intros x Hhalf.
+ Transparent repr.
+ unfold signed.
+ simpl.
+ rewrite Z_mod_modulus_eq.
+ replace modulus with 4294967296; auto.
+ replace half_modulus with 2147483648; auto.
+ repeat match goal with | |- context[if ?x then _ else _] => destruct x end.
+ - destruct (Z.eq_dec (unsigned x) 0).
+ + rewrite e. auto.
+ + pose proof (Z.mod_opp_l_nz (unsigned x) 4294967296).
+ assert (4294967296 <> 0) by lia.
+ apply H in H0.
+ rewrite H0 in l.
+ pose proof (Z.mod_small (unsigned x) 4294967296).
+ assert (0 <= unsigned x < 4294967296).
+ pose proof (unsigned_range_2 x). lia.
+ apply H1 in H2. rewrite H2 in l. lia.
+ rewrite Z.mod_small. assumption.
+ pose proof (unsigned_range_2 x). lia.
+ - destruct (Z.eq_dec (unsigned x) 0).
+ + lia.
+ + rewrite Z.mod_opp_l_nz; try lia.
+ rewrite Z.opp_sub_distr.
+ rewrite Z.mod_small. lia.
+ pose proof (unsigned_range_2 x).
+ simplify; lia.
+ rewrite Z.mod_small. assumption.
+ pose proof (unsigned_range_2 x).
+ simplify; lia.
+ - destruct (Z.eq_dec (unsigned x) 0).
+ + rewrite e in *. rewrite Z.opp_0 in *. rewrite Zmod_0_l in g. lia.
+ + rewrite Z.mod_opp_l_nz; try lia.
+ rewrite Z.mod_small. lia.
+ pose proof (unsigned_range_2 x). lia.
+ rewrite Z.mod_small. assumption.
+ pose proof (unsigned_range_2 x). lia.
+ - destruct (Z.eq_dec (unsigned x) 0).
+ + lia.
+ + rewrite Z.mod_opp_l_nz in g; try lia.
+ rewrite Z.mod_small in g.
+ assert (unsigned x < 2147483648) by lia. lia.
+ pose proof (unsigned_range_2 x).
+ replace max_unsigned with 4294967295 in * by auto. lia.
+ rewrite Z.mod_small. assumption.
+ pose proof (unsigned_range_2 x).
+ replace max_unsigned with 4294967295 in * by auto. lia.
+ Qed.
+
+ Lemma neg_divs_distr_l :
+ forall x y,
+ unsigned x <> 2147483648 ->
+ neg (divs x y) = divs (neg x) y.
+ Proof.
+ intros x y Hhalf. unfold divs, neg.
+ set (x' := signed x). set (y' := signed y).
+ apply eqm_samerepr.
+ apply eqm_trans with (- (Z.quot x' y')).
+ auto with ints.
+ replace (- (Z.quot x' y')) with (Z.quot (- x') y')
+ by (rewrite Zquot.Zquot_opp_l; auto).
+ unfold x'.
+ rewrite <- neg_signed'.
+ auto with ints.
+ assumption.
+ Qed.
+
+ Lemma neg_signed :
+ forall x : int,
+ unsigned x <> 2147483648 ->
+ signed x < 0 ->
+ signed (neg x) >= 0.
+ Proof.
+ intros.
+ rewrite neg_signed'. lia.
+ assumption.
+ Qed.
+
+ Lemma shl_signed_positive :
+ forall y,
+ unsigned y <= 30 ->
+ signed (shl one y) >= 0.
+ Proof.
+ intros.
+ unfold signed, shl.
+ destruct (zlt (unsigned (repr (Z.shiftl (unsigned one) (unsigned y)))) half_modulus).
+ - rewrite unsigned_repr.
+ + rewrite Z.shiftl_1_l.
+ apply Z.le_ge. apply Z.pow_nonneg. lia.
+ + rewrite Z.shiftl_1_l. split.
+ apply Z.pow_nonneg. lia.
+ simplify.
+ replace (4294967295) with (2 ^ 32 - 1); try lia.
+ transitivity (2 ^ 31); try lia.
+ apply Z.pow_le_mono_r; lia.
+ - simplify. rewrite Z.shiftl_1_l in g.
+ unfold half_modulus, modulus, wordsize,
+ Wordsize_32.wordsize in *. unfold two_power_nat in *. simplify.
+ unfold Z_mod_modulus in *.
+ destruct (2 ^ unsigned y) eqn:?.
+ apply Z.ge_le in g. exfalso.
+ replace (4294967296 / 2) with (2147483648) in g; auto.
+ rewrite Z.shiftl_1_l. rewrite Heqz.
+ unfold wordsize in *. unfold Wordsize_32.wordsize in *.
+ rewrite Zbits.P_mod_two_p_eq in *.
+ replace (4294967296 / 2) with (2147483648) in g; auto.
+ rewrite <- Heqz in g.
+ rewrite Z.mod_small in g.
+ replace (2147483648) with (2 ^ 31) in g.
+ pose proof (Z.pow_le_mono_r 2 (unsigned y) 30).
+ apply Z.ge_le in g.
+ assert (0 < 2) by lia. apply H0 in H1. lia. assumption. lia.
+ split. lia. rewrite two_power_nat_equiv.
+ apply Z.pow_lt_mono_r; lia.
+
+ pose proof (Zlt_neg_0 p).
+ pose proof (pow2_nonneg (unsigned y)). rewrite <- Heqz in H0.
+ lia.
+ Qed.
+
+ Lemma is_power2_shl :
+ forall y,
+ unsigned y <= 30 ->
+ is_power2 (shl one y) = Some y.
+ Proof.
+ intros.
+ unfold is_power2, shl.
+ destruct (Zbits.Z_is_power2 (unsigned (repr (Z.shiftl (unsigned one) (unsigned y))))) eqn:?.
+ - simplify.
+ rewrite Z_mod_modulus_eq in Heqo.
+ rewrite Z.mod_small in Heqo. rewrite Z.shiftl_1_l in Heqo.
+ rewrite <- two_p_correct in Heqo.
+ rewrite Zbits.Z_is_power2_complete in Heqo. inv Heqo.
+ rewrite repr_unsigned. auto.
+ pose proof (unsigned_range_2 y). lia.
+ rewrite Z.shiftl_1_l. unfold modulus, wordsize, Wordsize_32.wordsize.
+ rewrite two_power_nat_equiv.
+ split. apply pow2_nonneg.
+ apply Z.pow_lt_mono_r; lia.
+ - simplify.
+ rewrite Z_mod_modulus_eq in Heqo.
+ rewrite Z.mod_small in Heqo. rewrite Z.shiftl_1_l in Heqo.
+ rewrite <- two_p_correct in Heqo.
+ rewrite Zbits.Z_is_power2_complete in Heqo. discriminate.
+ pose proof (unsigned_range_2 y). lia.
+ rewrite Z.shiftl_1_l. unfold modulus, wordsize, Wordsize_32.wordsize.
+ rewrite two_power_nat_equiv.
+ split. apply pow2_nonneg.
+ apply Z.pow_lt_mono_r; lia.
+ Qed.
+
+ Definition shrx_alt (x y : int) : int :=
+ if zlt (signed x) 0
+ then neg (shru (neg x) y)
+ else shru x y.
+
+ Lemma shrx_shrx_alt_equiv_ne :
+ forall x y,
+ unsigned x <> 2147483648 ->
+ unsigned y <= 30 ->
+ shrx x y = shrx_alt x y.
+ Proof.
+ intros x y Hhalf H.
+ unfold shrx, shrx_alt, lt.
+ destruct (Z_ge_lt_dec (signed x) 0);
+ [rewrite zlt_false | rewrite zlt_true];
+
+ repeat lazymatch goal with
+ | |- is_power2 _ = Some _ => apply is_power2_shl
+ | |- signed (shl one _) >= 0 => apply shl_signed_positive
+ | |- signed (neg _) >= 0 => apply neg_signed
+ | |- divs _ _ = divu _ _ => apply div_divs_equiv
+ | |- divs ?x (shl one ?y) = neg (shru (neg ?x) ?y) =>
+ rewrite <- neg_involutive at 1; rewrite neg_divs_distr_l;
+ try assumption; f_equal
+ | |- divs ?x (shl one ?y) = shru ?x ?y =>
+ let H := fresh "H" in
+ pose proof (divu_pow2 x (shl one y) y) as H;
+ rewrite <- H
+ end; try assumption.
+ Qed.
+
+ Lemma shrx_shrx_alt_equiv_eq :
+ forall x y,
+ unsigned x = 2147483648 ->
+ unsigned y <= 30 ->
+ shrx x y = shrx_alt x y.
+ Proof.
+ intros.
+ repeat unfold shrx, shrx_alt, signed, divs, neg.
+ replace half_modulus with 2147483648 by auto.
+ replace modulus with 4294967296 by auto.
+ simplify.
+ rewrite !Z_mod_modulus_eq.
+ rewrite !H.
+ simplify.
+ assert (Hshl: Z.shiftl 1 (unsigned y) mod 4294967296 = Z.shiftl 1 (unsigned y)).
+ { apply Z.mod_small.
+ rewrite Z.shiftl_1_l.
+ split.
+ apply pow2_nonneg.
+ replace 4294967296 with (2^32) by auto.
+ apply Z.le_lt_trans with (m := 2 ^ 31); try lia.
+ apply Z.pow_le_mono_r; lia.
+ }
+ rewrite !Hshl.
+ f_equal.
+ assert ((Z.shiftl 1 (unsigned y)) < 2147483648).
+ rewrite Z.shiftl_1_l.
+ replace 2147483648 with (2^31) by auto.
+ apply Z.le_lt_trans with (m := 2 ^ 30); try lia.
+ apply Z.pow_le_mono_r; lia.
+ destruct (zlt (Z.shiftl 1 (unsigned y)) 2147483648); try lia.
+ replace (-2147483648 mod 4294967296) with 2147483648 by auto.
+ assert (Hmodeq : Z.shiftr 2147483648 (unsigned y) mod 4294967296
+ = Z.shiftr 2147483648 (unsigned y)).
+ { apply Z.mod_small. split.
+ apply Z.shiftr_nonneg. lia.
+ rewrite Z.shiftr_div_pow2.
+ replace 4294967296 with (Z.succ 4294967295); auto.
+ apply Zle_lt_succ.
+ replace 4294967295 with (4294967295 * (2 ^ unsigned y) / (2 ^ unsigned y)).
+ 2: {
+ apply Z.div_mul.
+ pose proof (Z.pow_pos_nonneg 2 (unsigned y)).
+ apply not_eq_sym.
+ apply Z.le_neq. apply H2; try lia.
+ apply unsigned_range_2.
+ }
+
+ apply Z.div_le_mono.
+ apply Z.pow_pos_nonneg. lia.
+ apply unsigned_range_2.
+ transitivity 4294967295; try lia.
+ apply Z.le_mul_diag_r; try lia.
+ replace 1 with (Z.succ 0) by auto.
+ apply Z.le_succ_l.
+ apply Z.pow_pos_nonneg; try lia.
+ apply unsigned_range_2. apply unsigned_range_2.
+ }
+ rewrite !Hmodeq.
+ replace (-2147483648) with (Z.opp 2147483648) by auto.
+ rewrite Zquot.Zquot_opp_l.
+ f_equal.
+ rewrite Zquot.Zquot_Zdiv_pos.
+ rewrite Z.shiftr_div_pow2.
+ rewrite Z.shiftl_1_l. auto.
+ apply unsigned_range_2.
+ lia.
+ rewrite Z.shiftl_1_l.
+ apply Z.lt_le_incl.
+ apply Z.pow_pos_nonneg; try lia.
+ apply unsigned_range_2.
+ Qed.
+
+ Theorem shrx_shrx_alt_equiv :
+ forall x y,
+ unsigned y <= 30 ->
+ shrx x y = shrx_alt x y.
+ Proof.
+ intros.
+ destruct (Z.eq_dec (unsigned x) 2147483648);
+ [ apply shrx_shrx_alt_equiv_eq | apply shrx_shrx_alt_equiv_ne]; auto.
+ Qed.
+
End IntExtra.
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index b1a885e..c2b3951 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -16,7 +16,14 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-From vericert Require Verilog Value Compiler.
+From vericert Require
+ Verilog
+ Value
+ Compiler
+ RTLBlockgen
+ RTLBlock
+ HTLSchedulegen
+ HTLgen.
From Coq Require DecidableClass.
@@ -128,6 +135,7 @@ Extract Constant Compiler.print_Clight => "PrintClight.print_if".
Extract Constant Compiler.print_Cminor => "PrintCminor.print_if".
Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if".
Extract Constant Compiler.print_RTL => "PrintRTL.print_if".
+Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if".
Extract Constant Compiler.print_HTL => "PrintHTL.print_if".
Extract Constant Compiler.print_LTL => "PrintLTL.print_if".
Extract Constant Compiler.print_Mach => "PrintMach.print_if".
@@ -162,12 +170,19 @@ Extract Inlined Constant Binary.B2R => "fun _ -> assert false".
Extract Inlined Constant Binary.round_mode => "fun _ -> assert false".
Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false".
+Extract Constant RTLBlockgen.partition => "Partition.partition".
+Extract Constant HTLSchedulegen.transl_module => "Schedule.transl_module".
+
(* Needed in Coq 8.4 to avoid problems with Function definitions. *)
Set Extraction AccessOpaque.
Cd "src/extraction".
Separate Extraction
Verilog.module Value.uvalueToZ vericert.Compiler.transf_hls
+ vericert.Compiler.transf_hls_temp
+ vericert.Compiler.transf_hls_opt
+ RTLBlockgen.transl_program RTLBlock.successors_instr
+ HTLgen.tbl_to_case_expr
Compiler.transf_c_program Compiler.transf_cminor_program
Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
diff --git a/src/verilog/Array.v b/src/hls/Array.v
index fe0f6b2..fe0f6b2 100644
--- a/src/verilog/Array.v
+++ b/src/hls/Array.v
diff --git a/src/verilog/AssocMap.v b/src/hls/AssocMap.v
index 8d8788a..8d8788a 100644
--- a/src/verilog/AssocMap.v
+++ b/src/hls/AssocMap.v
diff --git a/src/verilog/HTL.v b/src/hls/HTL.v
index 620ef14..620ef14 100644
--- a/src/verilog/HTL.v
+++ b/src/hls/HTL.v
diff --git a/src/hls/HTLBlockgen.v b/src/hls/HTLBlockgen.v
new file mode 100644
index 0000000..5f40962
--- /dev/null
+++ b/src/hls/HTLBlockgen.v
@@ -0,0 +1,655 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+(*From compcert Require Import Maps.
+From compcert Require Errors Globalenvs Integers.
+From compcert Require Import AST.
+From vericert Require Import RTLBlock Verilog HTL Vericertlib AssocMap ValueInt Statemonad.
+
+Hint Resolve AssocMap.gempty : htlh.
+Hint Resolve AssocMap.gso : htlh.
+Hint Resolve AssocMap.gss : htlh.
+Hint Resolve Ple_refl : htlh.
+Hint Resolve Ple_succ : htlh.
+
+Record state: Type := mkstate {
+ st_st : reg;
+ st_freshreg: reg;
+ st_freshstate: node;
+ st_scldecls: AssocMap.t (option io * scl_decl);
+ st_arrdecls: AssocMap.t (option io * arr_decl);
+ st_datapath: datapath;
+ st_controllogic: controllogic;
+}.
+
+Definition init_state (st : reg) : state :=
+ mkstate st
+ 1%positive
+ 1%positive
+ (AssocMap.empty (option io * scl_decl))
+ (AssocMap.empty (option io * arr_decl))
+ (AssocMap.empty stmnt)
+ (AssocMap.empty stmnt).
+
+Module HTLState <: State.
+
+ Definition st := state.
+
+ Inductive st_incr: state -> state -> Prop :=
+ state_incr_intro:
+ forall (s1 s2: state),
+ st_st s1 = st_st s2 ->
+ Ple s1.(st_freshreg) s2.(st_freshreg) ->
+ Ple s1.(st_freshstate) s2.(st_freshstate) ->
+ (forall n,
+ s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) ->
+ (forall n,
+ s1.(st_controllogic)!n = None
+ \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) ->
+ st_incr s1 s2.
+ Hint Constructors st_incr : htlh.
+
+ Definition st_prop := st_incr.
+ Hint Unfold st_prop : htlh.
+
+ Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed.
+
+ Lemma st_trans :
+ forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
+ Proof.
+ intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence.
+ - destruct H4 with n; destruct H8 with n; intuition congruence.
+ - destruct H5 with n; destruct H9 with n; intuition congruence.
+ Qed.
+
+End HTLState.
+Export HTLState.
+
+Module HTLMonad := Statemonad(HTLState).
+Export HTLMonad.
+
+Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
+Import HTLMonadExtra.
+Export MonadNotation.
+
+Definition state_goto (st : reg) (n : node) : stmnt :=
+ Vnonblock (Vvar st) (Vlit (posToValue n)).
+
+Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
+ Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).
+
+Definition check_empty_node_datapath:
+ forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }.
+Proof.
+ intros. case (s.(st_datapath)!n); tauto.
+Defined.
+
+Definition check_empty_node_controllogic:
+ forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }.
+Proof.
+ intros. case (s.(st_controllogic)!n); tauto.
+Defined.
+
+Lemma add_instr_state_incr :
+ forall s n n' st,
+ (st_datapath s)!n = None ->
+ (st_controllogic s)!n = None ->
+ st_incr s
+ (mkstate
+ s.(st_st)
+ s.(st_freshreg)
+ (st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
+ (AssocMap.set n st s.(st_datapath))
+ (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).
+Proof.
+ constructor; intros;
+ try (simpl; destruct (peq n n0); subst);
+ auto with htlh.
+Qed.
+
+Lemma declare_reg_state_incr :
+ forall i s r sz,
+ st_incr s
+ (mkstate
+ s.(st_st)
+ s.(st_freshreg)
+ s.(st_freshstate)
+ (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
+ s.(st_arrdecls)
+ s.(st_datapath)
+ s.(st_controllogic)).
+Proof. auto with htlh. Qed.
+
+Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
+ fun s => OK tt (mkstate
+ s.(st_st)
+ s.(st_freshreg)
+ s.(st_freshstate)
+ (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
+ s.(st_arrdecls)
+ s.(st_datapath)
+ s.(st_controllogic))
+ (declare_reg_state_incr i s r sz).
+
+Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
+ fun s =>
+ match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+ | left STM, left TRANS =>
+ OK tt (mkstate
+ s.(st_st)
+ s.(st_freshreg)
+ (st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
+ (AssocMap.set n st s.(st_datapath))
+ (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic)))
+ (add_instr_state_incr s n n' st STM TRANS)
+ | _, _ => Error (Errors.msg "HTL.add_instr")
+ end.
+
+Lemma add_instr_skip_state_incr :
+ forall s n st,
+ (st_datapath s)!n = None ->
+ (st_controllogic s)!n = None ->
+ st_incr s
+ (mkstate
+ s.(st_st)
+ s.(st_freshreg)
+ (st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
+ (AssocMap.set n st s.(st_datapath))
+ (AssocMap.set n Vskip s.(st_controllogic))).
+Proof.
+ constructor; intros;
+ try (simpl; destruct (peq n n0); subst);
+ auto with htlh.
+Qed.
+
+Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
+ fun s =>
+ match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+ | left STM, left TRANS =>
+ OK tt (mkstate
+ s.(st_st)
+ s.(st_freshreg)
+ (st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
+ (AssocMap.set n st s.(st_datapath))
+ (AssocMap.set n Vskip s.(st_controllogic)))
+ (add_instr_skip_state_incr s n st STM TRANS)
+ | _, _ => Error (Errors.msg "HTL.add_instr")
+ end.
+
+Lemma add_node_skip_state_incr :
+ forall s n st,
+ (st_datapath s)!n = None ->
+ (st_controllogic s)!n = None ->
+ st_incr s
+ (mkstate
+ s.(st_st)
+ s.(st_freshreg)
+ (st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
+ (AssocMap.set n Vskip s.(st_datapath))
+ (AssocMap.set n st s.(st_controllogic))).
+Proof.
+ constructor; intros;
+ try (simpl; destruct (peq n n0); subst);
+ auto with htlh.
+Qed.
+
+Definition add_node_skip (n : node) (st : stmnt) : mon unit :=
+ fun s =>
+ match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+ | left STM, left TRANS =>
+ OK tt (mkstate
+ s.(st_st)
+ s.(st_freshreg)
+ (st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
+ (AssocMap.set n Vskip s.(st_datapath))
+ (AssocMap.set n st s.(st_controllogic)))
+ (add_node_skip_state_incr s n st STM TRANS)
+ | _, _ => Error (Errors.msg "HTL.add_instr")
+ end.
+
+Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
+Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
+
+Definition bop (op : binop) (r1 r2 : reg) : expr :=
+ Vbinop op (Vvar r1) (Vvar r2).
+
+Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=
+ Vbinop op (Vvar r) (Vlit (intToValue l)).
+
+Definition boplitz (op: binop) (r: reg) (l: Z) : expr :=
+ Vbinop op (Vvar r) (Vlit (ZToValue l)).
+
+Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr :=
+ match c, args with
+ | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2)
+ | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2)
+ | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2)
+ | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2)
+ | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2)
+ | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2)
+ | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other")
+ end.
+
+Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int)
+ : mon expr :=
+ match c, args with
+ | Integers.Ceq, r1::nil => ret (boplit Veq r1 i)
+ | Integers.Cne, r1::nil => ret (boplit Vne r1 i)
+ | Integers.Clt, r1::nil => ret (boplit Vlt r1 i)
+ | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i)
+ | Integers.Cle, r1::nil => ret (boplit Vle r1 i)
+ | Integers.Cge, r1::nil => ret (boplit Vge r1 i)
+ | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")
+ end.
+
+Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : mon expr :=
+ match c, args with
+ | Integers.Clt, r1::r2::nil => ret (bop Vltu r1 r2)
+ | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2)
+ | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2)
+ | Integers.Cge, r1::r2::nil => ret (bop Vgeu r1 r2)
+ | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other")
+ end.
+
+Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int)
+ : mon expr :=
+ match c, args with
+ | Integers.Clt, r1::nil => ret (boplit Vltu r1 i)
+ | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i)
+ | Integers.Cle, r1::nil => ret (boplit Vleu r1 i)
+ | Integers.Cge, r1::nil => ret (boplit Vgeu r1 i)
+ | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")
+ end.
+
+Definition translate_condition (c : Op.condition) (args : list reg) : mon expr :=
+ match c, args with
+ | Op.Ccomp c, _ => translate_comparison c args
+ | Op.Ccompu c, _ => translate_comparisonu c args
+ | Op.Ccompimm c i, _ => translate_comparison_imm c args i
+ | Op.Ccompuimm c i, _ => translate_comparison_immu c args i
+ | Op.Cmaskzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero")
+ | Op.Cmasknotzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero")
+ | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other")
+ end.
+
+Definition check_address_parameter_signed (p : Z) : bool :=
+ Z.leb Integers.Ptrofs.min_signed p
+ && Z.leb p Integers.Ptrofs.max_signed.
+
+Definition check_address_parameter_unsigned (p : Z) : bool :=
+ Z.leb p Integers.Ptrofs.max_unsigned.
+
+Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=
+ match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)
+ | Op.Aindexed off, r1::nil =>
+ if (check_address_parameter_signed off)
+ then ret (boplitz Vadd r1 off)
+ else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address out of bounds")
+ | Op.Ascaled scale offset, r1::nil =>
+ if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
+ then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))
+ else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address out of bounds")
+ | Op.Aindexed2 offset, r1::r2::nil =>
+ if (check_address_parameter_signed offset)
+ then ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset)))
+ else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address out of bounds")
+ | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+ if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
+ then ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset))))
+ else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address out of bounds")
+ | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
+ let a := Integers.Ptrofs.unsigned a in
+ if (check_address_parameter_unsigned a)
+ then ret (Vlit (ZToValue a))
+ else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address out of bounds")
+ | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
+ end.
+
+(** Translate an instruction to a statement. FIX mulhs mulhu *)
+Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
+ match op, args with
+ | Op.Omove, r::nil => ret (Vvar r)
+ | Op.Ointconst n, _ => ret (Vlit (intToValue n))
+ | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r))
+ | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2)
+ | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2)
+ | Op.Omulimm n, r::nil => ret (boplit Vmul r n)
+ | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs")
+ | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu")
+ | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2)
+ | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2)
+ | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2)
+ | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2)
+ | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2)
+ | Op.Oandimm n, r::nil => ret (boplit Vand r n)
+ | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2)
+ | Op.Oorimm n, r::nil => ret (boplit Vor r n)
+ | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2)
+ | Op.Oxorimm n, r::nil => ret (boplit Vxor r n)
+ | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r))
+ | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2)
+ | Op.Oshlimm n, r::nil => ret (boplit Vshl r n)
+ | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2)
+ | Op.Oshrimm n, r::nil => ret (boplit Vshr r n)
+ | Op.Oshrximm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshrximm")
+ (*ret (Vbinop Vdiv (Vvar r)
+ (Vbinop Vshl (Vlit (ZToValue 1))
+ (Vlit (intToValue n))))*)
+ | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2)
+ | Op.Oshruimm n, r::nil => ret (boplit Vshru r n)
+ | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm")
+ (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32)))
+ (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*)
+ | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n)))
+ | Op.Ocmp c, _ => translate_condition c args
+ | Op.Osel c AST.Tint, r1::r2::rl =>
+ do tc <- translate_condition c rl;
+ ret (Vternary tc (Vvar r1) (Vvar r2))
+ | Op.Olea a, _ => translate_eff_addressing a args
+ | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other")
+ end.
+
+Lemma add_branch_instr_state_incr:
+ forall s e n n1 n2,
+ (st_datapath s) ! n = None ->
+ (st_controllogic s) ! n = None ->
+ st_incr s (mkstate
+ s.(st_st)
+ (st_freshreg s)
+ (st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
+ (AssocMap.set n Vskip (st_datapath s))
+ (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
+Proof.
+ intros. apply state_incr_intro; simpl;
+ try (intros; destruct (peq n0 n); subst);
+ auto with htlh.
+Qed.
+
+Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
+ fun s =>
+ match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+ | left NSTM, left NTRANS =>
+ OK tt (mkstate
+ s.(st_st)
+ (st_freshreg s)
+ (st_freshstate s)
+ s.(st_scldecls)
+ s.(st_arrdecls)
+ (AssocMap.set n Vskip (st_datapath s))
+ (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
+ (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS)
+ | _, _ => Error (Errors.msg "Htlgen: add_branch_instr")
+ end.
+
+Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
+ (args : list reg) (stack : reg) : mon expr :=
+ match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
+ | Mint32, Op.Aindexed off, r1::nil =>
+ if (check_address_parameter_signed off)
+ then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4))))
+ else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")
+ | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+ if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
+ then ret (Vvari stack
+ (Vbinop Vdivu
+ (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
+ (Vlit (ZToValue 4))))
+ else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")
+ | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
+ let a := Integers.Ptrofs.unsigned a in
+ if (check_address_parameter_unsigned a)
+ then ret (Vvari stack (Vlit (ZToValue (a / 4))))
+ else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset")
+ | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing")
+ end.
+
+Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=
+ match ns with
+ | n :: ns' => (i, n) :: enumerate (i+1) ns'
+ | nil => nil
+ end.
+
+Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
+ List.map (fun a => match a with
+ (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n)))
+ end)
+ (enumerate 0 ns).
+
+Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
+ match ni with
+ (n, i) =>
+ match i with
+ | Inop n' =>
+ if Z.leb (Z.pos n') Integers.Int.max_unsigned then
+ add_instr n n' Vskip
+ else error (Errors.msg "State is larger than 2^32.")
+ | Iop op args dst n' =>
+ if Z.leb (Z.pos n') Integers.Int.max_unsigned then
+ do instr <- translate_instr op args;
+ do _ <- declare_reg None dst 32;
+ add_instr n n' (nonblock dst instr)
+ else error (Errors.msg "State is larger than 2^32.")
+ | Iload mem addr args dst n' =>
+ if Z.leb (Z.pos n') Integers.Int.max_unsigned then
+ do src <- translate_arr_access mem addr args stack;
+ do _ <- declare_reg None dst 32;
+ add_instr n n' (nonblock dst src)
+ else error (Errors.msg "State is larger than 2^32.")
+ | Istore mem addr args src n' =>
+ if Z.leb (Z.pos n') Integers.Int.max_unsigned then
+ do dst <- translate_arr_access mem addr args stack;
+ add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
+ else error (Errors.msg "State is larger than 2^32.")
+ | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
+ | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
+ | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
+ | Icond cond args n1 n2 =>
+ if Z.leb (Z.pos n1) Integers.Int.max_unsigned && Z.leb (Z.pos n2) Integers.Int.max_unsigned then
+ do e <- translate_condition cond args;
+ add_branch_instr e n n1 n2
+ else error (Errors.msg "State is larger than 2^32.")
+ | Ijumptable r tbl =>
+ (*do s <- get;
+ add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))*)
+ error (Errors.msg "Ijumptable: Case statement not supported.")
+ | Ireturn r =>
+ match r with
+ | Some r' =>
+ add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))
+ | None =>
+ add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))
+ end
+ end
+ end.
+
+Lemma create_reg_state_incr:
+ forall s sz i,
+ st_incr s (mkstate
+ s.(st_st)
+ (Pos.succ (st_freshreg s))
+ (st_freshstate s)
+ (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
+ s.(st_arrdecls)
+ (st_datapath s)
+ (st_controllogic s)).
+Proof. constructor; simpl; auto with htlh. Qed.
+
+Definition create_reg (i : option io) (sz : nat) : mon reg :=
+ fun s => let r := s.(st_freshreg) in
+ OK r (mkstate
+ s.(st_st)
+ (Pos.succ r)
+ (st_freshstate s)
+ (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
+ (st_arrdecls s)
+ (st_datapath s)
+ (st_controllogic s))
+ (create_reg_state_incr s sz i).
+
+Lemma create_arr_state_incr:
+ forall s sz ln i,
+ st_incr s (mkstate
+ s.(st_st)
+ (Pos.succ (st_freshreg s))
+ (st_freshstate s)
+ s.(st_scldecls)
+ (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.
+
+Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
+ fun s => let r := s.(st_freshreg) in
+ OK (r, ln) (mkstate
+ s.(st_st)
+ (Pos.succ r)
+ (st_freshstate s)
+ s.(st_scldecls)
+ (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).
+
+Definition stack_correct (sz : Z) : bool :=
+ (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
+
+Definition max_pc_map (m : Maps.PTree.t stmnt) :=
+ PTree.fold (fun m pc i => Pos.max m pc) m 1%positive.
+
+Lemma max_pc_map_sound:
+ forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m).
+Proof.
+ intros until i. unfold max_pc_function.
+ apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m).
+ (* extensionality *)
+ intros. apply H0. rewrite H; auto.
+ (* base case *)
+ rewrite PTree.gempty. congruence.
+ (* inductive case *)
+ intros. rewrite PTree.gsspec in H2. destruct (peq pc k).
+ inv H2. xomega.
+ apply Ple_trans with a. auto. xomega.
+Qed.
+
+Lemma max_pc_wf :
+ forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
+ map_well_formed m.
+Proof.
+ unfold map_well_formed. intros.
+ exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x.
+ apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B.
+ unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst.
+ simplify. transitivity (Z.pos (max_pc_map m)); eauto.
+Qed.
+
+Definition transf_module (f: function) : mon module :=
+ if stack_correct f.(fn_stacksize) then
+ do fin <- create_reg (Some Voutput) 1;
+ do rtrn <- create_reg (Some Voutput) 32;
+ do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
+ do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
+ do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params);
+ do start <- create_reg (Some Vinput) 1;
+ do rst <- create_reg (Some Vinput) 1;
+ do clk <- create_reg (Some Vinput) 1;
+ do current_state <- get;
+ match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned,
+ zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with
+ | left LEDATA, left LECTRL =>
+ ret (mkmodule
+ f.(RTL.fn_params)
+ current_state.(st_datapath)
+ current_state.(st_controllogic)
+ f.(fn_entrypoint)
+ current_state.(st_st)
+ stack
+ stack_len
+ fin
+ rtrn
+ start
+ rst
+ clk
+ current_state.(st_scldecls)
+ current_state.(st_arrdecls)
+ (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)))
+ | _, _ => error (Errors.msg "More than 2^32 states.")
+ end
+ else error (Errors.msg "Stack size misalignment.").
+
+Definition max_state (f: function) : state :=
+ let st := Pos.succ (max_reg_function f) in
+ mkstate st
+ (Pos.succ st)
+ (Pos.succ (max_pc_function f))
+ (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)).
+
+Definition transl_module (f : function) : Errors.res module :=
+ run_mon (max_state f) (transf_module f).
+
+Definition transl_fundef := transf_partial_fundef transl_module.
+
+(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *)
+
+(*Definition transl_main_fundef f : Errors.res HTL.fundef :=
+ match f with
+ | Internal f => transl_fundef (Internal f)
+ | External f => Errors.Error (Errors.msg "Could not find internal main function")
+ end.
+
+(** Translation of a whole program. *)
+
+Definition transl_program (p: RTL.program) : Errors.res HTL.program :=
+ transform_partial_program2 (fun i f => if Pos.eqb p.(AST.prog_main) i
+ then transl_fundef f
+ else transl_main_fundef f)
+ (fun i v => Errors.OK v) p.
+*)
+
+Definition main_is_internal (p : RTLBlock.program) : bool :=
+ let ge := Globalenvs.Genv.globalenv p in
+ match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with
+ | Some b =>
+ match Globalenvs.Genv.find_funct_ptr ge b with
+ | Some (AST.Internal _) => true
+ | _ => false
+ end
+ | _ => false
+ end.
+
+Definition transl_program (p : RTLBlock.program) : Errors.res HTL.program :=
+ if main_is_internal p
+ then transform_partial_program transl_fundef p
+ else Errors.Error (Errors.msg "Main function is not Internal.").
+*)
diff --git a/src/hls/HTLSchedulegen.v b/src/hls/HTLSchedulegen.v
new file mode 100644
index 0000000..1ae3bf6
--- /dev/null
+++ b/src/hls/HTLSchedulegen.v
@@ -0,0 +1,42 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+From compcert Require Import Maps.
+From compcert Require Errors Globalenvs Integers.
+From compcert Require Import AST.
+From vericert Require Import RTLBlock Verilog HTL Vericertlib AssocMap ValueInt Statemonad.
+
+Parameter transl_module : function -> Errors.res module.
+
+Definition transl_fundef := transf_partial_fundef transl_module.
+
+Definition main_is_internal (p : RTLBlock.program) : bool :=
+ let ge := Globalenvs.Genv.globalenv p in
+ match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with
+ | Some b =>
+ match Globalenvs.Genv.find_funct_ptr ge b with
+ | Some (AST.Internal _) => true
+ | _ => false
+ end
+ | _ => false
+ end.
+
+Definition transl_program (p : RTLBlock.program) : Errors.res HTL.program :=
+ if main_is_internal p
+ then transform_partial_program transl_fundef p
+ else Errors.Error (Errors.msg "Main function is not Internal.").
diff --git a/src/translation/HTLgen.v b/src/hls/HTLgen.v
index 68e0293..5f0f8bf 100644
--- a/src/translation/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -358,10 +358,10 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
| Op.Oshlimm n, r::nil => ret (boplit Vshl r n)
| Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2)
| Op.Oshrimm n, r::nil => ret (boplit Vshr r n)
- | Op.Oshrximm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshrximm")
- (*ret (Vbinop Vdiv (Vvar r)
- (Vbinop Vshl (Vlit (ZToValue 1))
- (Vlit (intToValue n))))*)
+ | Op.Oshrximm n, r::nil =>
+ ret (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0)))
+ (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar r)) (Vlit n)))
+ (Vbinop Vshru (Vvar r) (Vlit n)))
| Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2)
| Op.Oshruimm n, r::nil => ret (boplit Vshru r n)
| Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm")
diff --git a/src/translation/HTLgenproof.v b/src/hls/HTLgenproof.v
index bf63800..afc827d 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -1,4 +1,4 @@
-(*
+ (*
* Vericert: Verified high-level synthesis.
* Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
*
@@ -470,7 +470,11 @@ Section CORRECTNESS.
| |- context[match ?d with _ => _ end] => destruct d eqn:?; try discriminate
| H : match ?d with _ => _ end = _ |- _ => repeat unfold_match H
| H : match ?d with _ => _ end _ = _ |- _ => repeat unfold_match H
- | |- Verilog.expr_runp _ _ _ _ _ => econstructor
+ | |- Verilog.expr_runp _ _ _ ?f _ =>
+ match f with
+ | Verilog.Vternary _ _ _ => idtac
+ | _ => econstructor
+ end
| |- val_value_lessdef (?f _ _) _ => unfold f
| |- val_value_lessdef (?f _) _ => unfold f
| H : ?f (Registers.Regmap.get _ _) _ = Some _ |- _ =>
@@ -716,6 +720,71 @@ Section CORRECTNESS.
repeat unfold_match TR_INSTR; inv TR_INSTR; repeat econstructor.
Qed.
+ Lemma eval_correct_Oshrximm :
+ forall s sp rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st n,
+ match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
+ (RTL.fn_code f) ! pc = Some (RTL.Iop (Op.Oshrximm n) args res0 pc') ->
+ Op.eval_operation ge sp (Op.Oshrximm n)
+ (List.map (fun r : BinNums.positive =>
+ Registers.Regmap.get r rs) args) m = Some v ->
+ translate_instr (Op.Oshrximm n) args s = OK e s' i ->
+ exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'.
+ Proof.
+ intros s sp rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st n MSTATE INSTR EVAL TR_INSTR.
+ pose proof MSTATE as MSTATE_2. inv MSTATE.
+ inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR;
+ unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); inv EVAL.
+ (*repeat (simplify; eval_correct_tac; unfold valueToInt in * ).
+ destruct (Z_lt_ge_dec (Int.signed i0) 0).
+ econstructor.*)
+ unfold Values.Val.shrx in *.
+ destruct v0; try discriminate.
+ destruct (Int.ltu n (Int.repr 31)) eqn:?; try discriminate.
+ inversion H1. clear H1.
+ assert (Int.unsigned n <= 30).
+ { unfold Int.ltu in *. destruct (zlt (Int.unsigned n) (Int.unsigned (Int.repr 31))); try discriminate.
+ rewrite Int.unsigned_repr in l by (simplify; lia).
+ replace 31 with (Z.succ 30) in l by auto.
+ apply Zlt_succ_le in l.
+ auto.
+ }
+ rewrite IntExtra.shrx_shrx_alt_equiv in H2 by auto.
+ unfold IntExtra.shrx_alt in *.
+ destruct (zlt (Int.signed i0) 0).
+ - repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue;
+ repeat (simplify; eval_correct_tac).
+ inv_lessdef. unfold valueToInt in *. rewrite H3 in H1.
+ inv H1.
+ unfold Int.lt in *. rewrite zlt_true in Heqb0. simplify.
+ rewrite Int.unsigned_repr in Heqb0. discriminate.
+ simplify; lia.
+ unfold ZToValue. rewrite Int.signed_repr by (simplify; lia).
+ auto.
+ rewrite H3 in H1; discriminate.
+ rewrite H3 in H2; discriminate.
+ rewrite IntExtra.shrx_shrx_alt_equiv; auto. unfold IntExtra.shrx_alt. rewrite zlt_true; try lia.
+ simplify. inv_lessdef. unfold valueToInt in *.
+ rewrite H3 in H1. auto. inv H1. auto.
+ rewrite H3 in H1. discriminate.
+ rewrite H3 in H2. discriminate.
+ - econstructor; econstructor; [eapply Verilog.erun_Vternary_false|idtac]; repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue;
+ repeat (simplify; eval_correct_tac).
+ inv_lessdef. unfold valueToInt in *. rewrite H3 in H1.
+ inv H1.
+ unfold Int.lt in *. rewrite zlt_false in Heqb0. simplify.
+ rewrite Int.unsigned_repr in Heqb0. lia.
+ simplify; lia.
+ unfold ZToValue. rewrite Int.signed_repr by (simplify; lia).
+ auto.
+ rewrite H3 in H1; discriminate.
+ rewrite H3 in H2; discriminate.
+ rewrite IntExtra.shrx_shrx_alt_equiv; auto. unfold IntExtra.shrx_alt. rewrite zlt_false; try lia.
+ simplify. inv_lessdef. unfold valueToInt in *.
+ rewrite H3 in H1. auto. inv H1. auto.
+ rewrite H3 in H1. discriminate.
+ rewrite H3 in H2. discriminate.
+ Qed.
+
Lemma eval_correct :
forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st,
match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
@@ -754,6 +823,47 @@ Section CORRECTNESS.
- rewrite Heqb in Heqb0. discriminate.
(*- unfold Int.ror. unfold Int.or. unfold Int.shru, Int.shl, Int.sub. unfold intToValue. unfold Int.modu,
repeat (rewrite Int.unsigned_repr). auto.*)
+ - assert (Int.unsigned n <= 30).
+ { unfold Int.ltu in *. destruct (zlt (Int.unsigned n) (Int.unsigned (Int.repr 31))); try discriminate.
+ rewrite Int.unsigned_repr in l by (simplify; lia).
+ replace 31 with (Z.succ 30) in l by auto.
+ apply Zlt_succ_le in l.
+ auto.
+ }
+ destruct (zlt (Int.signed i0) 0).
+ + repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue;
+ repeat (simplify; eval_correct_tac).
+ rewrite IntExtra.shrx_shrx_alt_equiv; auto. unfold IntExtra.shrx_alt. rewrite zlt_true; try lia.
+ simplify. inv_lessdef. unfold valueToInt in *.
+ rewrite Heqv0 in H0. auto. inv H0. auto.
+ rewrite Heqv0 in H2. discriminate.
+ unfold valueToInt in l. auto.
+ inv_lessdef. unfold valueToInt in *. rewrite Heqv0 in H0.
+ inv H0.
+ unfold Int.lt in *. rewrite zlt_true in Heqb0. simplify.
+ rewrite Int.unsigned_repr in Heqb0. discriminate.
+ simplify; lia.
+ unfold ZToValue. rewrite Int.signed_repr by (simplify; lia).
+ auto.
+ rewrite Heqv0 in H0; discriminate.
+ rewrite Heqv0 in H2; discriminate.
+ + eapply Verilog.erun_Vternary_false; repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue;
+ repeat (simplify; eval_correct_tac).
+ rewrite IntExtra.shrx_shrx_alt_equiv; auto. unfold IntExtra.shrx_alt. rewrite zlt_false; try lia.
+ simplify. inv_lessdef. unfold valueToInt in *.
+ rewrite Heqv0 in H0. auto. inv H0. auto.
+ rewrite Heqv0 in H2. discriminate.
+ unfold valueToInt in *. auto.
+ inv_lessdef. unfold valueToInt in *.
+ rewrite Heqv0 in H0.
+ inv H0.
+ unfold Int.lt in *. rewrite zlt_false in Heqb0. simplify.
+ rewrite Int.unsigned_repr in Heqb0. lia.
+ simplify; lia.
+ unfold ZToValue. rewrite Int.signed_repr by (simplify; lia).
+ auto.
+ rewrite Heqv0 in H0; discriminate.
+ rewrite Heqv0 in H2; discriminate.
- unfold Op.eval_addressing32 in *. repeat (unfold_match H2); inv H2.
+ unfold translate_eff_addressing in *. repeat (unfold_match H1).
destruct v0; inv Heql; rewrite H2; inv H1; repeat eval_correct_tac.
diff --git a/src/translation/HTLgenspec.v b/src/hls/HTLgenspec.v
index 541f9fa..541f9fa 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
new file mode 100644
index 0000000..d9bccad
--- /dev/null
+++ b/src/hls/Partition.ml
@@ -0,0 +1,125 @@
+ (*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+open Printf
+open Clflags
+open Camlcoq
+open Datatypes
+open Coqlib
+open Maps
+open AST
+open Kildall
+open Op
+open RTLBlock
+
+(* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass
+ [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *)
+let find_edge i n =
+ let succ = RTL.successors_instr i in
+ let filt = List.filter (fun s -> P.lt n s || P.lt s (P.pred n)) succ in
+ ((match filt with [] -> [] | _ -> [n]), filt)
+
+let find_edges c =
+ PTree.fold (fun l n i ->
+ let f = find_edge i n in
+ (List.append (fst f) (fst l), List.append (snd f) (snd l))) c ([], [])
+
+let prepend_instr i = function
+ | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e}
+
+let translate_inst = function
+ | RTL.Inop _ -> Some RBnop
+ | RTL.Iop (op, ls, dst, _) -> Some (RBop (op, ls, dst))
+ | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (m, addr, ls, dst))
+ | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (m, addr, ls, src))
+ | _ -> None
+
+let translate_cfi = function
+ | RTL.Icall (s, r, ls, dst, n) -> Some (RBcall (s, r, ls, dst, n))
+ | RTL.Itailcall (s, r, ls) -> Some (RBtailcall (s, r, ls))
+ | RTL.Ibuiltin (e, ls, r, n) -> Some (RBbuiltin (e, ls, r, n))
+ | RTL.Icond (c, ls, dst1, dst2) -> Some (RBcond (c, ls, dst1, dst2))
+ | RTL.Ijumptable (r, ls) -> Some (RBjumptable (r, ls))
+ | RTL.Ireturn r -> Some (RBreturn r)
+ | _ -> None
+
+let rec next_bblock_from_RTL is_start e (c : RTL.code) s i =
+ let succ = List.map (fun i -> (i, PTree.get i c)) (RTL.successors_instr i) in
+ let trans_inst = (translate_inst i, translate_cfi i) in
+ match trans_inst, succ with
+ | (None, Some i'), _ ->
+ if List.exists (fun x -> x = s) (snd e) && not is_start then
+ Errors.OK { bb_body = []; bb_exit = Some (RBgoto s) }
+ else
+ Errors.OK { bb_body = []; bb_exit = Some i' }
+ | (Some i', None), (s', Some i_n)::[] ->
+ if List.exists (fun x -> x = s) (fst e) then
+ Errors.OK { bb_body = [i']; bb_exit = Some (RBgoto s') }
+ else if List.exists (fun x -> x = s) (snd e) && not is_start then
+ Errors.OK { bb_body = []; bb_exit = Some (RBgoto s) }
+ else begin
+ match next_bblock_from_RTL false e c s' i_n with
+ | Errors.OK bb ->
+ Errors.OK (prepend_instr i' bb)
+ | Errors.Error msg -> Errors.Error msg
+ end
+ | _, _ ->
+ Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong."))
+
+let rec traverseacc f l c =
+ match l with
+ | [] -> Errors.OK c
+ | x::xs ->
+ match f x c with
+ | Errors.Error msg -> Errors.Error msg
+ | Errors.OK x' ->
+ match traverseacc f xs x' with
+ | Errors.Error msg -> Errors.Error msg
+ | Errors.OK xs' -> Errors.OK xs'
+
+let rec translate_all edge c s res =
+ let c_bb, translated = res in
+ if List.exists (fun x -> P.eq x s) translated then Errors.OK (c_bb, translated) else
+ (match PTree.get s c with
+ | None -> Errors.Error (Errors.msg (coqstring_of_camlstring "Could not translate all."))
+ | Some i ->
+ match next_bblock_from_RTL true edge c s i with
+ | Errors.Error msg -> Errors.Error msg
+ | Errors.OK {bb_exit = None; _} ->
+ Errors.Error (Errors.msg (coqstring_of_camlstring "Error in translate all"))
+ | Errors.OK {bb_body = bb; bb_exit = Some e} ->
+ let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in
+ (match traverseacc (translate_all edge c) succ (c_bb, s :: translated) with
+ | Errors.Error msg -> Errors.Error msg
+ | Errors.OK (c', t') ->
+ Errors.OK (PTree.set s {bb_body = bb; bb_exit = Some e} c', t')))
+
+(* Partition a function and transform it into RTLBlock. *)
+let function_from_RTL f =
+ let e = find_edges f.RTL.fn_code in
+ match translate_all e f.RTL.fn_code f.RTL.fn_entrypoint (PTree.empty, []) with
+ | Errors.Error msg -> Errors.Error msg
+ | Errors.OK (c, _) ->
+ Errors.OK { fn_sig = f.RTL.fn_sig;
+ fn_stacksize = f.RTL.fn_stacksize;
+ fn_params = f.RTL.fn_params;
+ fn_entrypoint = f.RTL.fn_entrypoint;
+ fn_code = c
+ }
+
+let partition = function_from_RTL
diff --git a/src/verilog/PrintHTL.ml b/src/hls/PrintHTL.ml
index 44f8b01..44f8b01 100644
--- a/src/verilog/PrintHTL.ml
+++ b/src/hls/PrintHTL.ml
diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml
new file mode 100644
index 0000000..45bd253
--- /dev/null
+++ b/src/hls/PrintRTLBlock.ml
@@ -0,0 +1,119 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+(** Pretty-printers for RTL code *)
+
+open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open RTLBlock
+open PrintAST
+
+(* Printing of RTL code *)
+
+let reg pp r =
+ fprintf pp "x%d" (P.to_int r)
+
+let rec regs pp = function
+ | [] -> ()
+ | [r] -> reg pp r
+ | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let ros pp = function
+ | Coq_inl r -> reg pp r
+ | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
+
+let print_bblock_body pp i =
+ fprintf pp "\t\t";
+ match i with
+ | RBnop -> fprintf pp "nop\n"
+ | RBop(op, ls, dst) ->
+ fprintf pp "%a = %a\n"
+ reg dst (PrintOp.print_operation reg) (op, ls)
+ | RBload(chunk, addr, args, dst) ->
+ fprintf pp "%a = %s[%a]\n"
+ reg dst (name_of_chunk chunk)
+ (PrintOp.print_addressing reg) (addr, args)
+ | RBstore(chunk, addr, args, src) ->
+ fprintf pp "%s[%a] = %a\n"
+ (name_of_chunk chunk)
+ (PrintOp.print_addressing reg) (addr, args)
+ reg src
+
+let print_bblock_exit pp i =
+ fprintf pp "\t\t";
+ match i with
+ | Some(RBcall(_, fn, args, res, _)) ->
+ fprintf pp "%a = %a(%a)\n"
+ reg res ros fn regs args;
+ | Some(RBtailcall(_, fn, args)) ->
+ fprintf pp "tailcall %a(%a)\n"
+ ros fn regs args
+ | Some(RBbuiltin(ef, args, res, _)) ->
+ fprintf pp "%a = %s(%a)\n"
+ (print_builtin_res reg) res
+ (name_of_external ef)
+ (print_builtin_args reg) args
+ | Some(RBcond(cond, args, s1, s2)) ->
+ fprintf pp "if (%a) goto %d else goto %d\n"
+ (PrintOp.print_condition reg) (cond, args)
+ (P.to_int s1) (P.to_int s2)
+ | Some(RBjumptable(arg, tbl)) ->
+ let tbl = Array.of_list tbl in
+ fprintf pp "jumptable (%a)\n" reg arg;
+ for i = 0 to Array.length tbl - 1 do
+ fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i))
+ done
+ | Some(RBreturn None) ->
+ fprintf pp "return\n"
+ | Some(RBreturn (Some arg)) ->
+ fprintf pp "return %a\n" reg arg
+ | Some(RBgoto n) ->
+ fprintf pp "goto %d\n" (P.to_int n)
+ | None -> fprintf pp "\n"
+
+let print_bblock pp (pc, i) =
+ fprintf pp "%5d:{\n" pc;
+ List.iter (print_bblock_body pp) i.bb_body;
+ print_bblock_exit pp i.bb_exit;
+ fprintf pp "\t}\n\n"
+
+let print_function pp id f =
+ fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
+ let instrs =
+ List.sort
+ (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+ (List.rev_map
+ (fun (pc, i) -> (P.to_int pc, i))
+ (PTree.elements f.fn_code)) in
+ List.iter (print_bblock pp) instrs;
+ fprintf pp "}\n\n"
+
+let print_globdef pp (id, gd) =
+ match gd with
+ | Gfun(Internal f) -> print_function pp id f
+ | _ -> ()
+
+let print_program pp (prog: program) =
+ List.iter (print_globdef pp) prog.prog_defs
+
+let destination : string option ref = ref None
+
+let print_if prog =
+ match !destination with
+ | None -> ()
+ | Some f ->
+ let oc = open_out f in
+ print_program oc prog;
+ close_out oc
diff --git a/src/verilog/PrintVerilog.ml b/src/hls/PrintVerilog.ml
index 44710b8..44710b8 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/hls/PrintVerilog.ml
diff --git a/src/verilog/PrintVerilog.mli b/src/hls/PrintVerilog.mli
index 6a15ee9..6a15ee9 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/hls/PrintVerilog.mli
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
new file mode 100644
index 0000000..dc505ed
--- /dev/null
+++ b/src/hls/RTLBlock.v
@@ -0,0 +1,170 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Require Import Coqlib Maps.
+Require Import AST Integers Values Events Memory Globalenvs Smallstep.
+Require Import Op Registers.
+
+Definition node := positive.
+
+Inductive instruction : Type :=
+| RBnop : instruction
+| RBop : operation -> list reg -> reg -> instruction
+| RBload : memory_chunk -> addressing -> list reg -> reg -> instruction
+| RBstore : memory_chunk -> addressing -> list reg -> reg -> instruction.
+
+Definition bblock_body : Type := list instruction.
+
+Inductive control_flow_inst : Type :=
+| RBcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst
+| RBtailcall : signature -> reg + ident -> list reg -> control_flow_inst
+| RBbuiltin : external_function -> list (builtin_arg reg) ->
+ builtin_res reg -> node -> control_flow_inst
+| RBcond : condition -> list reg -> node -> node -> control_flow_inst
+| RBjumptable : reg -> list node -> control_flow_inst
+| RBreturn : option reg -> control_flow_inst
+| RBgoto : node -> control_flow_inst.
+
+Record bblock : Type := mk_bblock {
+ bb_body: bblock_body;
+ bb_exit: option control_flow_inst
+ }.
+
+Definition code : Type := PTree.t bblock.
+
+Record function: Type := mkfunction {
+ fn_sig: signature;
+ fn_params: list reg;
+ fn_stacksize: Z;
+ fn_code: code;
+ fn_entrypoint: node
+}.
+
+Definition fundef := AST.fundef function.
+
+Definition program := AST.program fundef unit.
+
+Definition funsig (fd: fundef) :=
+ match fd with
+ | Internal f => fn_sig f
+ | External ef => ef_sig ef
+ end.
+
+Definition successors_instr (i : control_flow_inst) : list node :=
+ match i with
+ | RBcall sig ros args res s => s :: nil
+ | RBtailcall sig ros args => nil
+ | RBbuiltin ef args res s => s :: nil
+ | RBcond cond args ifso ifnot => ifso :: ifnot :: nil
+ | RBjumptable arg tbl => tbl
+ | RBreturn optarg => nil
+ | RBgoto n => n :: nil
+ end.
+
+(* Definition genv := Genv.t fundef unit.
+Definition regset := Regmap.t val.
+
+Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
+ match rl, vl with
+ | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
+ | _, _ => Regmap.init Vundef
+ end.
+
+Inductive stackframe : Type :=
+ | Stackframe:
+ forall (res: reg) (**r where to store the result *)
+ (f: function) (**r calling function *)
+ (sp: val) (**r stack pointer in calling function *)
+ (pc: node) (**r program point in calling function *)
+ (rs: regset), (**r register state in calling function *)
+ stackframe.
+
+Inductive cont : Type :=
+ | C
+ | N.
+
+Inductive state : Type :=
+ | State:
+ forall (stack: list stackframe) (**r call stack *)
+ (f: function) (**r current function *)
+ (sp: val) (**r stack pointer *)
+ (pc: node) (**r current program point in [c] *)
+ (rs: regset) (**r register state *)
+ (m: mem) (**r memory state *)
+ (bblock: bblock) (**r bblock being executed *)
+ (c : cont),
+ state
+ | Callstate:
+ forall (stack: list stackframe) (**r call stack *)
+ (f: fundef) (**r function to call *)
+ (args: list val) (**r arguments to the call *)
+ (m: mem), (**r memory state *)
+ state
+ | Returnstate:
+ forall (stack: list stackframe) (**r call stack *)
+ (v: val) (**r return value for the call *)
+ (m: mem), (**r memory state *)
+ state.
+
+Section RELSEM.
+
+Variable ge: genv.
+
+Definition find_function
+ (ros: reg + ident) (rs: regset) : option fundef :=
+ match ros with
+ | inl r => Genv.find_funct ge rs#r
+ | inr symb =>
+ match Genv.find_symbol ge symb with
+ | None => None
+ | Some b => Genv.find_funct_ptr ge b
+ end
+ end.
+
+Inductive step : state -> trace -> state -> Prop :=
+ | exec_RBnop :
+ forall s f sp pc rs m ls ci,
+ step (State s f sp pc rs m (mk_bblock (RBnop :: ls) ci) C) E0
+ (State s f sp (Pos.succ pc) rs m (mk_bblock ls ci) C)
+ | exec_RBop :
+ forall s f sp pc rs m ls args op res ci v,
+ eval_operation ge sp op rs##args m = Some v ->
+ step (State s f sp pc rs m (mk_bblock (RBop op args res :: ls) ci) C) E0
+ (State s f sp (Pos.succ pc) rs m (mk_bblock ls ci) C)
+ | exec_RBload:
+ forall s f sp pc rs m chunk addr args dst a v ls ci,
+ eval_addressing ge sp addr rs##args = Some a ->
+ Mem.loadv chunk m a = Some v ->
+ step (State s f sp pc rs m (mk_bblock (RBload chunk addr args dst :: ls) ci) C)
+ E0 (State s f sp (Pos.succ pc) (rs#dst <- v) m (mk_bblock ls ci) C)
+ | exec_RBstore:
+ forall s f sp pc rs m chunk addr args src a m' ls ci,
+ eval_addressing ge sp addr rs##args = Some a ->
+ Mem.storev chunk m a rs#src = Some m' ->
+ step (State s f sp pc rs m (mk_bblock (RBstore chunk addr args src :: ls) ci) C)
+ E0 (State s f sp (Pos.succ pc) rs m' (mk_bblock ls ci) C)
+ | exec_RBcond:
+ forall s f sp pc rs m cond args ifso ifnot b pc',
+ eval_condition cond rs##args m = Some b ->
+ pc' = (if b then ifso else ifnot) ->
+ step (State s f sp pc rs m (mk_bblock nil (RBcond cond args ifso ifnot)) C)
+ E0 (State s f sp pc' rs m (mk_bblock nil (RBcond cond args ifso ifnot)) N)
+.
+
+End RELSEM.
+*)
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
new file mode 100644
index 0000000..6b3e9c3
--- /dev/null
+++ b/src/hls/RTLBlockgen.v
@@ -0,0 +1,32 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+From compcert Require
+ RTL.
+From compcert Require Import
+ AST
+ Maps.
+From vericert Require Import
+ RTLBlock.
+
+Parameter partition : RTL.function -> Errors.res function.
+
+Definition transl_fundef := transf_partial_fundef partition.
+
+Definition transl_program : RTL.program -> Errors.res program :=
+ transform_partial_program transl_fundef.
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
new file mode 100644
index 0000000..af3f28b
--- /dev/null
+++ b/src/hls/RTLPar.v
@@ -0,0 +1,99 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+From compcert Require Import Coqlib Maps.
+From compcert Require Import AST Integers Values Events Memory Globalenvs Smallstep.
+From compcert Require Import Op Registers.
+
+Definition node := positive.
+
+Inductive instruction : Type :=
+| RPnop : instruction
+| RPop : operation -> list reg -> reg -> instruction
+| RPload : memory_chunk -> addressing -> list reg -> reg -> instruction
+| RPstore : memory_chunk -> addressing -> list reg -> reg -> instruction.
+
+Definition bblock_body : Type := list (list instruction).
+
+Inductive control_flow_inst : Type :=
+| RPcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst
+| RPtailcall : signature -> reg + ident -> list reg -> control_flow_inst
+| RPbuiltin : external_function -> list (builtin_arg reg) ->
+ builtin_res reg -> node -> control_flow_inst
+| RPcond : condition -> list reg -> node -> node -> control_flow_inst
+| RPjumptable : reg -> list node -> control_flow_inst
+| RPreturn : option reg -> control_flow_inst
+| RPgoto : node -> control_flow_inst.
+
+Record bblock : Type := mk_bblock {
+ bb_body: bblock_body;
+ bb_exit: option control_flow_inst
+ }.
+
+Definition code : Type := PTree.t bblock.
+
+Record function: Type := mkfunction {
+ fn_sig: signature;
+ fn_params: list reg;
+ fn_stacksize: Z;
+ fn_code: code;
+ fn_entrypoint: node
+}.
+
+Definition fundef := AST.fundef function.
+
+Definition program := AST.program fundef unit.
+
+Definition funsig (fd: fundef) :=
+ match fd with
+ | Internal f => fn_sig f
+ | External ef => ef_sig ef
+ end.
+
+Definition successors_instr (i : control_flow_inst) : list node :=
+ match i with
+ | RPcall sig ros args res s => s :: nil
+ | RPtailcall sig ros args => nil
+ | RPbuiltin ef args res s => s :: nil
+ | RPcond cond args ifso ifnot => ifso :: ifnot :: nil
+ | RPjumptable arg tbl => tbl
+ | RPreturn optarg => nil
+ | RPgoto n => n :: nil
+ end.
+
+(*Inductive state : Type :=
+ | State:
+ forall (stack: list stackframe) (**r call stack *)
+ (f: function) (**r current function *)
+ (sp: val) (**r stack pointer *)
+ (pc: node) (**r current program point in [c] *)
+ (rs: regset) (**r register state *)
+ (m: mem), (**r memory state *)
+ state
+ | Callstate:
+ forall (stack: list stackframe) (**r call stack *)
+ (f: fundef) (**r function to call *)
+ (args: list val) (**r arguments to the call *)
+ (m: mem), (**r memory state *)
+ state
+ | Returnstate:
+ forall (stack: list stackframe) (**r call stack *)
+ (v: val) (**r return value for the call *)
+ (m: mem), (**r memory state *)
+ state.
+*)
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
new file mode 100644
index 0000000..982aa0e
--- /dev/null
+++ b/src/hls/Schedule.ml
@@ -0,0 +1,610 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+open Printf
+open Clflags
+open Camlcoq
+open Datatypes
+open Coqlib
+open Maps
+open AST
+open Kildall
+open Op
+open RTLBlock
+open HTL
+open Verilog
+open HTLgen
+open HTLMonad
+open HTLMonadExtra
+
+module IMap = Map.Make (struct
+ type t = int
+
+ let compare = compare
+end)
+
+type dfg = { nodes : instruction list; edges : (int * int) list }
+(** The DFG type defines a list of instructions with their data dependencies as [edges], which are
+ the pairs of integers that represent the index of the instruction in the [nodes]. The edges
+ always point from left to right. *)
+
+let print_list f out_chan a =
+ fprintf out_chan "[ ";
+ List.iter (fprintf out_chan "%a " f) a;
+ fprintf out_chan "]"
+
+let print_tuple out_chan a =
+ let l, r = a in
+ fprintf out_chan "(%d,%d)" l r
+
+let print_dfg out_chan dfg =
+ fprintf out_chan "{ nodes = %a, edges = %a }"
+ (print_list PrintRTLBlock.print_bblock_body)
+ dfg.nodes (print_list print_tuple) dfg.edges
+
+let read_process command =
+ let buffer_size = 2048 in
+ let buffer = Buffer.create buffer_size in
+ let string = Bytes.create buffer_size in
+ let in_channel = Unix.open_process_in command in
+ let chars_read = ref 1 in
+ while !chars_read <> 0 do
+ chars_read := input in_channel string 0 buffer_size;
+ Buffer.add_substring buffer (Bytes.to_string string) 0 !chars_read
+ done;
+ ignore (Unix.close_process_in in_channel);
+ Buffer.contents buffer
+
+(** Add a dependency if it uses a register that was written to previously. *)
+let add_dep i tree deps curr =
+ match PTree.get curr tree with None -> deps | Some ip -> (ip, i) :: deps
+
+(** This function calculates the dependencies of each instruction. The nodes correspond to previous
+ register that were allocated and show which instruction caused it.
+
+ This function only gathers the RAW constraints, and will therefore only be active for operations
+ that modify registers, which is this case only affects loads and operations. *)
+let accumulate_RAW_deps dfg curr =
+ let i, dst_map, { edges; nodes } = dfg in
+ let acc_dep_instruction rs dst =
+ ( i + 1,
+ PTree.set dst i dst_map,
+ {
+ nodes;
+ edges = List.append (List.fold_left (add_dep i dst_map) [] rs) edges;
+ } )
+ in
+ let acc_dep_instruction_nodst rs =
+ ( i + 1,
+ dst_map,
+ {
+ nodes;
+ edges = List.append (List.fold_left (add_dep i dst_map) [] rs) edges;
+ } )
+ in
+ match curr with
+ | RBop (_, rs, dst) -> acc_dep_instruction rs dst
+ | RBload (_mem, _addr, rs, dst) -> acc_dep_instruction rs dst
+ | RBstore (_mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs)
+ | _ -> (i + 1, dst_map, { edges; nodes })
+
+(** Finds the next write to the [dst] register. This is a small optimisation so that only one
+ dependency is generated for a data dependency. *)
+let rec find_next_dst_write i dst i' curr =
+ let check_dst dst' curr' =
+ if dst = dst' then Some (i, i')
+ else find_next_dst_write i dst (i' + 1) curr'
+ in
+ match curr with
+ | [] -> None
+ | RBop (_, _, dst') :: curr' -> check_dst dst' curr'
+ | RBload (_, _, _, dst') :: curr' -> check_dst dst' curr'
+ | _ :: curr' -> find_next_dst_write i dst (i' + 1) curr'
+
+let rec find_all_next_dst_read i dst i' curr =
+ let check_dst rs curr' =
+ if List.exists (fun x -> x = dst) rs
+ then (i, i') :: find_all_next_dst_read i dst (i' + 1) curr'
+ else find_all_next_dst_read i dst (i' + 1) curr'
+ in
+ match curr with
+ | [] -> []
+ | RBop (_, rs, _) :: curr' -> check_dst rs curr'
+ | RBload (_, _, rs, _) :: curr' -> check_dst rs curr'
+ | RBstore (_, _, rs, src) :: curr' -> check_dst (src :: rs) curr'
+ | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr'
+
+let drop i lst =
+ let rec drop' i' lst' =
+ match lst' with
+ | _ :: ls -> if i' = i then ls else drop' (i' + 1) ls
+ | [] -> []
+ in
+ if i = 0 then lst else drop' 1 lst
+
+let take i lst =
+ let rec take' i' lst' =
+ match lst' with
+ | l :: ls -> if i' = i then [ l ] else l :: take' (i' + 1) ls
+ | [] -> []
+ in
+ if i = 0 then [] else take' 1 lst
+
+let rec next_store i = function
+ | [] -> None
+ | RBstore (_, _, _, _) :: _ -> Some i
+ | _ :: rst -> next_store (i + 1) rst
+
+let rec next_load i = function
+ | [] -> None
+ | RBload (_, _, _, _) :: _ -> Some i
+ | _ :: rst -> next_load (i + 1) rst
+
+let accumulate_RAW_mem_deps dfg curr =
+ let i, { nodes; edges } = dfg in
+ match curr with
+ | RBload (_, _, _, _) -> (
+ match next_store 0 (take i nodes |> List.rev) with
+ | None -> (i + 1, { nodes; edges })
+ | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) )
+ | _ -> (i + 1, { nodes; edges })
+
+let accumulate_WAR_mem_deps dfg curr =
+ let i, { nodes; edges } = dfg in
+ match curr with
+ | RBstore (_, _, _, _) -> (
+ match next_load 0 (take i nodes |> List.rev) with
+ | None -> (i + 1, { nodes; edges })
+ | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) )
+ | _ -> (i + 1, { nodes; edges })
+
+let accumulate_WAW_mem_deps dfg curr =
+ let i, { nodes; edges } = dfg in
+ match curr with
+ | RBstore (_, _, _, _) -> (
+ match next_store 0 (take i nodes |> List.rev) with
+ | None -> (i + 1, { nodes; edges })
+ | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) )
+ | _ -> (i + 1, { nodes; edges })
+
+(** This function calculates the WAW dependencies, which happen when two writes are ordered one
+ after another and therefore have to be kept in that order. This accumulation might be redundant
+ if register renaming is done before hand, because then these dependencies can be avoided. *)
+let accumulate_WAW_deps dfg curr =
+ let i, { edges; nodes } = dfg in
+ let dst_dep dst =
+ match find_next_dst_write i dst (i + 1) (drop (i + 1) nodes) with
+ | Some d -> (i + 1, { nodes; edges = d :: edges })
+ | _ -> (i + 1, { nodes; edges })
+ in
+ match curr with
+ | RBop (_, _, dst) -> dst_dep dst
+ | RBload (_, _, _, dst) -> dst_dep dst
+ | RBstore (_, _, _, _) -> (
+ match next_store (i + 1) (drop (i + 1) nodes) with
+ | None -> (i + 1, { nodes; edges })
+ | Some i' -> (i + 1, { nodes; edges = (i, i') :: edges }) )
+ | _ -> (i + 1, { nodes; edges })
+
+let accumulate_WAR_deps dfg curr =
+ let i, { edges; nodes } = dfg in
+ let dst_dep dst =
+ let dep_list = find_all_next_dst_read i dst 0 (take i nodes |> List.rev)
+ |> List.map (function (d, d') -> (i - d' - 1, d))
+ in
+ (i + 1, { nodes; edges = List.append dep_list edges })
+ in
+ match curr with
+ | RBop (_, _, dst) -> dst_dep dst
+ | RBload (_, _, _, dst) -> dst_dep dst
+ | _ -> (i + 1, { nodes; edges })
+
+let assigned_vars vars = function
+ | RBnop -> vars
+ | RBop (_, _, dst) -> dst :: vars
+ | RBload (_, _, _, dst) -> dst :: vars
+ | RBstore (_, _, _, _) -> vars
+
+(** All the nodes in the DFG have to come after the source of the basic block, and should terminate
+ before the sink of the basic block. After that, there should be constraints for data
+ dependencies between nodes. *)
+let gather_bb_constraints debug bb =
+ let _, _, dfg =
+ List.fold_left accumulate_RAW_deps
+ (0, PTree.empty, { nodes = bb.bb_body; edges = [] })
+ bb.bb_body
+ in
+ if debug then printf "DFG : %a\n" print_dfg dfg else ();
+ let _, dfg' = List.fold_left accumulate_WAW_deps (0, dfg) bb.bb_body in
+ if debug then printf "DFG': %a\n" print_dfg dfg' else ();
+ let _, dfg'' = List.fold_left accumulate_WAR_deps (0, dfg') bb.bb_body in
+ if debug then printf "DFG'': %a\n" print_dfg dfg'' else ();
+ let _, dfg''' =
+ List.fold_left accumulate_RAW_mem_deps (0, dfg'') bb.bb_body
+ in
+ if debug then printf "DFG''': %a\n" print_dfg dfg''' else ();
+ let _, dfg'''' =
+ List.fold_left accumulate_WAR_mem_deps (0, dfg''') bb.bb_body
+ in
+ if debug then printf "DFG'''': %a\n" print_dfg dfg'''' else ();
+ let _, dfg''''' =
+ List.fold_left accumulate_WAW_mem_deps (0, dfg'''') bb.bb_body
+ in
+ if debug then printf "DFG''''': %a\n" print_dfg dfg''''' else ();
+ match bb.bb_exit with
+ | None -> assert false
+ | Some e -> (List.length bb.bb_body, dfg''''', successors_instr e)
+
+let gen_bb_name s i = sprintf "bb%d%s" (P.to_int i) s
+
+let gen_bb_name_ssrc = gen_bb_name "ssrc"
+
+let gen_bb_name_ssnk = gen_bb_name "ssnk"
+
+let gen_var_name s c i = sprintf "v%d%s_%d" (P.to_int i) s c
+
+let gen_var_name_b = gen_var_name "b"
+
+let gen_var_name_e = gen_var_name "e"
+
+let print_lt0 = sprintf "%s - %s <= 0;\n"
+
+let print_bb_order i c = if P.to_int c < P.to_int i then
+ print_lt0 (gen_bb_name_ssnk i) (gen_bb_name_ssrc c) else
+ ""
+
+let print_src_order i c =
+ print_lt0 (gen_bb_name_ssrc i) (gen_var_name_b c i)
+ ^ print_lt0 (gen_var_name_e c i) (gen_bb_name_ssnk i)
+ ^ sprintf "%s - %s = 1;\n" (gen_var_name_e c i) (gen_var_name_b c i)
+
+let print_src_type i c =
+ sprintf "int %s;\n" (gen_var_name_e c i)
+ ^ sprintf "int %s;\n" (gen_var_name_b c i)
+
+let print_data_dep_order c (i, j) =
+ print_lt0 (gen_var_name_e i c) (gen_var_name_b j c)
+
+let rec gather_cfg_constraints (completed, (bvars, constraints, types)) c curr =
+ if List.exists (fun x -> P.eq x curr) completed then
+ (completed, (bvars, constraints, types))
+ else
+ match PTree.get curr c with
+ | None -> assert false
+ | Some (num_iters, dfg, next) ->
+ let constraints' =
+ constraints
+ ^ String.concat "" (List.map (print_bb_order curr) next)
+ ^ String.concat ""
+ (List.map (print_src_order curr)
+ (List.init num_iters (fun x -> x)))
+ ^ String.concat "" (List.map (print_data_dep_order curr) dfg.edges)
+ in
+ let types' =
+ types
+ ^ String.concat ""
+ (List.map (print_src_type curr)
+ (List.init num_iters (fun x -> x)))
+ ^ sprintf "int %s;\n" (gen_bb_name_ssrc curr)
+ ^ sprintf "int %s;\n" (gen_bb_name_ssnk curr)
+ in
+ let bvars' =
+ List.append
+ (List.map
+ (fun x -> gen_var_name_b x curr)
+ (List.init num_iters (fun x -> x)))
+ bvars
+ in
+ let next' = List.filter (fun x -> P.lt x curr) next in
+ List.fold_left
+ (fun compl curr' -> gather_cfg_constraints compl c curr')
+ (curr :: completed, (bvars', constraints', types'))
+ next'
+
+let rec intersperse s = function
+ | [] -> []
+ | [ a ] -> [ a ]
+ | x :: xs -> x :: s :: intersperse s xs
+
+let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ]
+
+let parse_soln tree s =
+ let r = Str.regexp "v\([0-9]+\)b_\([0-9]+\)[ ]+\([0-9]+\)" in
+ if Str.string_match r s 0 then
+ IMap.update
+ (Str.matched_group 1 s |> int_of_string)
+ (update_schedule
+ ( Str.matched_group 2 s |> int_of_string,
+ Str.matched_group 3 s |> int_of_string ))
+ tree
+ else tree
+
+let solve_constraints vars constraints types =
+ let oc = open_out "lpsolve.txt" in
+ fprintf oc "min: ";
+ List.iter (fprintf oc "%s") (intersperse " + " vars);
+ fprintf oc ";\n";
+ fprintf oc "%s" constraints;
+ fprintf oc "%s" types;
+ close_out oc;
+ Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt")
+ |> drop 3
+ |> List.fold_left parse_soln IMap.empty
+
+let find_min = function
+ | [] -> assert false
+ | l :: ls ->
+ let rec find_min' current = function
+ | [] -> current
+ | l' :: ls' ->
+ if snd l' < current then find_min' (snd l') ls'
+ else find_min' current ls'
+ in
+ find_min' (snd l) ls
+
+let find_max = function
+ | [] -> assert false
+ | l :: ls ->
+ let rec find_max' current = function
+ | [] -> current
+ | l' :: ls' ->
+ if snd l' > current then find_max' (snd l') ls'
+ else find_max' current ls'
+ in
+ find_max' (snd l) ls
+
+type registers = { reg_finish : reg; reg_return : reg; reg_stk : reg }
+
+let ( >>= ) = bind
+
+let translate_control_flow r curr_st instr =
+ match instr with
+ | RBgoto n ->
+ fun state ->
+ OK
+ ( (),
+ {
+ state with
+ st_controllogic =
+ PTree.set curr_st (state_goto state.st_st n)
+ state.st_controllogic;
+ } )
+ | RBcond (c, rs, n1, n2) ->
+ translate_condition c rs >>= fun ce state ->
+ OK
+ ( (),
+ {
+ state with
+ st_controllogic =
+ PTree.set curr_st
+ (state_cond state.st_st ce n1 n2)
+ state.st_controllogic;
+ } )
+ | RBreturn ret -> (
+ let new_state state = state.st_freshstate in
+ match ret with
+ | None ->
+ let fin =
+ Vseq
+ ( HTLgen.block r.reg_finish
+ (Vlit (ValueInt.coq_ZToValue (Z.of_uint 1))),
+ HTLgen.block r.reg_return
+ (Vlit (ValueInt.coq_ZToValue (Z.of_uint 0))) )
+ in
+ fun state ->
+ OK
+ ( (),
+ {
+ state with
+ st_datapath =
+ PTree.set (new_state state) fin state.st_datapath;
+ st_controllogic =
+ PTree.set curr_st
+ (state_goto state.st_st (new_state state))
+ state.st_controllogic;
+ st_freshstate = P.succ state.st_freshstate;
+ } )
+ | Some ret' ->
+ let fin =
+ Vseq
+ ( HTLgen.block r.reg_finish
+ (Vlit (ValueInt.coq_ZToValue (Z.of_uint 1))),
+ HTLgen.block r.reg_return (Vvar ret') )
+ in
+ fun state ->
+ OK
+ ( (),
+ {
+ state with
+ st_datapath =
+ PTree.set (new_state state) fin state.st_datapath;
+ st_controllogic =
+ PTree.set curr_st
+ (state_goto state.st_st (new_state state))
+ state.st_controllogic;
+ st_freshstate = P.succ state.st_freshstate;
+ } ) )
+ | RBjumptable (r, tbl) ->
+ fun state ->
+ OK ( (),
+ {
+ state with
+ st_controllogic = PTree.set curr_st (Vcase (Vvar r, HTLgen.tbl_to_case_expr state.st_st tbl, Some Vskip)) state.st_controllogic
+ })
+ | _ ->
+ error
+ (Errors.msg
+ (coqstring_of_camlstring
+ "Control flow instructions not implemented."))
+
+let translate_instr r curr_st instr =
+ let prev_instr state =
+ match PTree.get curr_st state.st_datapath with None -> Vskip | Some v -> v
+ in
+ match instr with
+ | RBnop ->
+ fun state ->
+ OK
+ ( (),
+ {
+ state with
+ st_datapath =
+ PTree.set curr_st (prev_instr state) state.st_datapath;
+ } )
+ | RBop (op, rs, dst) ->
+ translate_instr op rs >>= fun instr ->
+ declare_reg None dst (Nat.of_int 32) >>= fun _ state ->
+ let stmnt = Vseq (prev_instr state, nonblock dst instr) in
+ OK
+ ( (),
+ { state with st_datapath = PTree.set curr_st stmnt state.st_datapath }
+ )
+ | RBload (mem, addr, rs, dst) ->
+ translate_arr_access mem addr rs r.reg_stk >>= fun src ->
+ declare_reg None dst (Nat.of_int 32) >>= fun _ state ->
+ let stmnt = Vseq (prev_instr state, nonblock dst src) in
+ OK
+ ( (),
+ { state with st_datapath = PTree.set curr_st stmnt state.st_datapath }
+ )
+ | RBstore (mem, addr, rs, src) ->
+ translate_arr_access mem addr rs r.reg_stk >>= fun dst state ->
+ OK
+ ( (),
+ {
+ state with
+ st_datapath =
+ PTree.set curr_st
+ (Vseq (prev_instr state, Vnonblock (dst, Vvar src)))
+ state.st_datapath;
+ } )
+
+let combine_bb_schedule schedule s =
+ let i, st = s in
+ IMap.update st (update_schedule i) schedule
+
+let add_schedules r bb_body min_sched curr ischedule =
+ let i, schedule = ischedule in
+ let curr_state = curr - i + min_sched in
+ let instrs = List.map (List.nth bb_body) schedule in
+ if curr_state = 20 then printf "HII: curr_state: %d : curr: %d\n" curr_state curr;
+ collectlist (translate_instr r (P.of_int curr_state)) instrs >>= fun _ ->
+ translate_control_flow r (P.of_int curr_state)
+ (RBgoto (curr_state - 1 |> P.of_int))
+
+(** Should generate the [HTL] code based on the input [RTLBlock] description. *)
+let transf_htl r c (schedule : (int * int) list IMap.t) =
+ let f bbs =
+ let i, bb = bbs in
+ match bb with
+ | { bb_body = []; bb_exit = Some c } -> translate_control_flow r i c
+ | { bb_body = bb_body'; bb_exit = Some ctrl_flow } ->
+ let i_sched =
+ try IMap.find (P.to_int i) schedule
+ with Not_found -> (
+ printf "Could not find %d\n" (P.to_int i);
+ IMap.iter
+ (fun d -> printf "%d: %a\n" d (print_list print_tuple))
+ schedule;
+ assert false
+ )
+ in
+ let min_state = find_min i_sched in
+ let max_state = find_max i_sched in
+ let i_sched_tree =
+ List.fold_left combine_bb_schedule IMap.empty i_sched
+ in
+ collectlist
+ (add_schedules r bb_body' min_state (P.to_int i))
+ (IMap.to_seq i_sched_tree |> List.of_seq)
+ >>= fun _ ->
+ printf "--------------- curr: %d, max: %d, min: %d, next: %d\n" (P.to_int i) max_state min_state (P.to_int i - max_state + min_state - 1);
+ printf "HIIIII: %d orig: %d\n" (P.to_int i - max_state + min_state - 1) (P.to_int i);
+ (match ctrl_flow with
+ | RBgoto _ ->
+ translate_control_flow r (P.of_int (P.to_int i - max_state + min_state)) ctrl_flow
+ | _ ->
+ translate_control_flow r (P.of_int (P.to_int i - max_state + min_state - 1)) ctrl_flow)
+ | _ ->
+ coqstring_of_camlstring "Illegal state reached in scheduler"
+ |> Errors.msg |> error
+ in
+ collectlist f c
+
+let second = function (_, a, _) -> a
+
+let schedule entry r (c : code) =
+ let debug = true in
+ let c' = PTree.map1 (gather_bb_constraints false) c in
+ let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in
+ let _, (vars, constraints, types) =
+ gather_cfg_constraints ([], ([], "", "")) c' entry
+ in
+ let schedule' = solve_constraints vars constraints types in
+ IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';
+ (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*)
+ transf_htl r (PTree.elements c) schedule'
+
+let transl_module' (f : RTLBlock.coq_function) : HTL.coq_module mon =
+ create_reg (Some Voutput) (Nat.of_int 1) >>= fun fin ->
+ create_reg (Some Voutput) (Nat.of_int 32) >>= fun rtrn ->
+ create_arr None (Nat.of_int 32) (Nat.of_int (Z.to_int f.fn_stacksize / 4))
+ >>= fun stack_var ->
+ let stack, stack_len = stack_var in
+ schedule f.fn_entrypoint
+ { reg_finish = fin; reg_return = rtrn; reg_stk = stack }
+ f.fn_code
+ >>= fun _ ->
+ collectlist (fun r -> declare_reg (Some Vinput) r (Nat.of_int 32)) f.fn_params
+ >>= fun _ ->
+ create_reg (Some Vinput) (Nat.of_int 1) >>= fun start ->
+ create_reg (Some Vinput) (Nat.of_int 1) >>= fun rst ->
+ create_reg (Some Vinput) (Nat.of_int 1) >>= fun clk current_state ->
+ let m =
+ {
+ HTL.mod_params = f.fn_params;
+ HTL.mod_datapath = current_state.st_datapath;
+ HTL.mod_controllogic = current_state.st_controllogic;
+ HTL.mod_entrypoint = f.fn_entrypoint;
+ HTL.mod_st = current_state.st_st;
+ HTL.mod_stk = stack;
+ HTL.mod_stk_len = stack_len;
+ HTL.mod_finish = fin;
+ HTL.mod_return = rtrn;
+ HTL.mod_start = start;
+ HTL.mod_reset = rst;
+ HTL.mod_clk = clk;
+ HTL.mod_scldecls = current_state.st_scldecls;
+ HTL.mod_arrdecls = current_state.st_arrdecls;
+ }
+ in
+ OK (m, current_state)
+
+let max_state f =
+ let st = P.of_int 10000 in
+ {
+ (init_state st) with
+ st_st = st;
+ st_freshreg = P.succ st;
+ st_freshstate = P.of_int 10000;
+ st_scldecls =
+ AssocMap.AssocMap.set st (None, Nat.of_int 32) (init_state st).st_scldecls;
+ }
+
+let transl_module (f : RTLBlock.coq_function) : HTL.coq_module Errors.res =
+ run_mon (max_state f) (transl_module' f)
diff --git a/src/verilog/Value.v b/src/hls/Value.v
index d6a3d8b..d6a3d8b 100644
--- a/src/verilog/Value.v
+++ b/src/hls/Value.v
diff --git a/src/verilog/ValueInt.v b/src/hls/ValueInt.v
index f1fd056..f1fd056 100644
--- a/src/verilog/ValueInt.v
+++ b/src/hls/ValueInt.v
diff --git a/src/hls/ValueVal.v b/src/hls/ValueVal.v
new file mode 100644
index 0000000..b882dc6
--- /dev/null
+++ b/src/hls/ValueVal.v
@@ -0,0 +1,209 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+(* begin hide *)
+From bbv Require Import Word.
+From bbv Require HexNotation WordScope.
+From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
+From compcert Require Export lib.Integers common.Values.
+From vericert Require Import Vericertlib.
+(* end hide *)
+
+(** * Value
+
+A [value] is a bitvector with a specific size. We are using the implementation
+of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse.
+However, we need to wrap it with an [Inductive] so that we can specify and match
+on the size of the [value]. This is necessary so that we can easily store
+[value]s of different sizes in a list or in a map.
+
+Using the default [word], this would not be possible, as the size is part of the type. *)
+
+(* Definition value : Type := val.
+
+(** ** Value conversions
+
+Various conversions to different number types such as [N], [Z], [positive] and
+[int], where the last one is a theory of integers of powers of 2 in CompCert. *)
+
+Definition valueToNat (v : value) : nat :=
+ match v with
+ | value_bool b => Nat.b2n b
+ | value_int i => Z.to_nat (Int.unsigned i)
+ | value_int64 i => Z.to_nat (Int64.unsigned i)
+ end.
+
+Definition natToValue (n : nat) : value :=
+ value_int (Int.repr (Z.of_nat n)).
+
+Definition natToValue64 (n : nat) : value :=
+ value_int64 (Int64.repr (Z.of_nat n)).
+
+Definition valueToN (v : value) : N :=
+ match v with
+ | value_bool b => N.b2n b
+ | value_int i => Z.to_N (Int.unsigned i)
+ | value_int64 i => Z.to_N (Int64.unsigned i)
+ end.
+
+Definition NToValue (n : N) : value :=
+ value_int (Int.repr (Z.of_N n)).
+
+Definition NToValue64 (n : N) : value :=
+ value_int64 (Int64.repr (Z.of_N n)).
+
+Definition ZToValue (z : Z) : value :=
+ value_int (Int.repr z).
+
+Definition ZToValue64 (z : Z) : value :=
+ value_int64 (Int64.repr z).
+
+Definition valueToZ (v : value) : Z :=
+ match v with
+ | value_bool b => Z.b2z b
+ | value_int i => Int.signed i
+ | value_int64 i => Int64.signed i
+ end.
+
+Definition uvalueToZ (v : value) : Z :=
+ match v with
+ | value_bool b => Z.b2z b
+ | value_int i => Int.unsigned i
+ | value_int64 i => Int64.unsigned i
+ end.
+
+Definition posToValue (p : positive) : value :=
+ value_int (Int.repr (Z.pos p)).
+
+Definition posToValue64 (p : positive) : value :=
+ value_int64 (Int64.repr (Z.pos p)).
+
+Definition valueToPos (v : value) : positive :=
+ match v with
+ | value_bool b => 1%positive
+ | value_int i => Z.to_pos (Int.unsigned i)
+ | value_int64 i => Z.to_pos (Int64.unsigned i)
+ end.
+
+Definition intToValue (i : Integers.int) : value := value_int i.
+
+Definition int64ToValue (i : Integers.int64) : value := value_int64 i.
+
+Definition valueToInt (v : value) : Integers.int :=
+ match v with
+ | value_bool b => Int.repr (if b then 1 else 0)
+ | value_int i => i
+ | value_int64 i => Int.repr (Int64.unsigned i)
+ end.
+
+(*Definition ptrToValue (i : ptrofs) : value :=
+ value_int (Ptrofs.to_int i).
+
+Definition valueToPtr (i : value) : Integers.ptrofs :=
+ Ptrofs.of_int i.
+
+Definition valToValue (v : Values.val) : option value :=
+ match v with
+ | Values.Vint i => Some (intToValue i)
+ | Values.Vint64 i => Some (intToValue i)
+ | Values.Vptr b off => Some (ptrToValue off)
+ | Values.Vundef => Some (ZToValue 0%Z)
+ | _ => None
+ end.
+
+(** Convert a [value] to a [bool], so that choices can be made based on the
+result. This is also because comparison operators will give back [value] instead
+of [bool], so if they are in a condition, they will have to be converted before
+they can be used. *)
+
+Definition valueToBool (v : value) : bool :=
+ if Z.eqb (uvalueToZ v) 0 then false else true.
+
+Definition boolToValue (b : bool) : value :=
+ natToValue (if b then 1 else 0).
+
+(** ** Arithmetic operations *)
+
+Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
+intros; subst; assumption. Defined.
+
+Lemma unify_word_unfold :
+ forall sz w,
+ unify_word sz sz w eq_refl = w.
+Proof. auto. Qed.
+
+Inductive val_value_lessdef: val -> value -> Prop :=
+| val_value_lessdef_int:
+ forall i v',
+ i = valueToInt v' ->
+ val_value_lessdef (Vint i) v'
+| val_value_lessdef_ptr:
+ forall b off v',
+ off = valueToPtr v' ->
+ val_value_lessdef (Vptr b off) v'
+| lessdef_undef: forall v, val_value_lessdef Vundef v.
+
+Inductive opt_val_value_lessdef: option val -> value -> Prop :=
+| opt_lessdef_some:
+ forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v'
+| opt_lessdef_none: forall v, opt_val_value_lessdef None v.
+
+Lemma valueToZ_ZToValue :
+ forall z,
+ (Int.min_signed <= z <= Int.max_signed)%Z ->
+ valueToZ (ZToValue z) = z.
+Proof. auto using Int.signed_repr. Qed.
+
+Lemma uvalueToZ_ZToValue :
+ forall z,
+ (0 <= z <= Int.max_unsigned)%Z ->
+ uvalueToZ (ZToValue z) = z.
+Proof. auto using Int.unsigned_repr. Qed.
+
+Lemma valueToPos_posToValue :
+ forall v,
+ 0 <= Z.pos v <= Int.max_unsigned ->
+ valueToPos (posToValue v) = v.
+Proof.
+ unfold valueToPos, posToValue.
+ intros. rewrite Int.unsigned_repr.
+ apply Pos2Z.id. assumption.
+Qed.
+
+Lemma valueToInt_intToValue :
+ forall v,
+ valueToInt (intToValue v) = v.
+Proof. auto. Qed.
+
+Lemma valToValue_lessdef :
+ forall v v',
+ valToValue v = Some v' ->
+ val_value_lessdef v v'.
+Proof.
+ intros.
+ destruct v; try discriminate; constructor.
+ unfold valToValue in H. inversion H.
+ unfold valueToInt. unfold intToValue in H1. auto.
+ inv H. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial.
+Qed.
+
+Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue,
+ ptrToValue in *)
+
+(*Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption.*)
+*)
diff --git a/src/verilog/Verilog.v b/src/hls/Verilog.v
index 3b0dd0a..e5f86d5 100644
--- a/src/verilog/Verilog.v
+++ b/src/hls/Verilog.v
@@ -29,7 +29,7 @@ Require Import Lia.
Import ListNotations.
-From vericert Require Import common.Vericertlib common.Show verilog.ValueInt AssocMap Array.
+From vericert Require Import Vericertlib Show ValueInt AssocMap Array.
From compcert Require Events.
From compcert Require Import Integers Errors Smallstep Globalenvs.
@@ -149,7 +149,7 @@ Inductive binop : Type :=
(** ** Unary Operators *)
Inductive unop : Type :=
-| Vneg (** negation ([~]) *)
+| Vneg (** negation ([-]) *)
| Vnot. (** not operation [!] *)
(** ** Expressions *)
diff --git a/src/translation/Veriloggen.v b/src/hls/Veriloggen.v
index a0be0fa..a0be0fa 100644
--- a/src/translation/Veriloggen.v
+++ b/src/hls/Veriloggen.v
diff --git a/src/translation/Veriloggenproof.v b/src/hls/Veriloggenproof.v
index 9abbd4b..9abbd4b 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/hls/Veriloggenproof.v
generated by cgit (git 2.34.1) at 2024-07-06 12:23:22 +0000