aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation/HTLgen.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/translation/HTLgen.v')
-rw-r--r--src/translation/HTLgen.v116
1 files changed, 48 insertions, 68 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 1869a8f..8245a06 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -1,5 +1,5 @@
(*
- * CoqUp: Verified high-level synthesis.
+ * 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
@@ -19,7 +19,7 @@
From compcert Require Import Maps.
From compcert Require Errors Globalenvs Integers.
From compcert Require Import AST RTL.
-From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt Statemonad.
+From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt Statemonad.
Hint Resolve AssocMap.gempty : htlh.
Hint Resolve AssocMap.gso : htlh.
@@ -311,16 +311,26 @@ Definition check_address_parameter_unsigned (p : Z) : bool :=
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 =>
- ret (boplitz Vadd r1 off)
+ if (check_address_parameter_signed off)
+ then ret (boplitz Vadd r1 off)
+ else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned")
| Op.Ascaled scale offset, r1::nil =>
- ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))
+ 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 misaligned")
| Op.Aindexed2 offset, r1::r2::nil =>
- ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset)))
+ 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 misaligned")
| Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
- ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset))))
+ 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 misaligned")
| Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
let a := Integers.Ptrofs.unsigned a in
- ret (Vlit (ZToValue a))
+ if (check_address_parameter_unsigned a)
+ then ret (Vlit (ZToValue a))
+ else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned")
| _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
end.
@@ -402,38 +412,26 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
| _, _ => 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 misaligned") *)
-(* | 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 misaligned") *)
-(* | 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 misaligned stack offset") *)
-(* | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") *)
-(* end. *)
-
-Definition translate_arr_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 =>
- ret (boplitz Vadd r1 off)
- | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
- ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
- | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
+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 misaligned")
+ | 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 misaligned")
+ | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
let a := Integers.Ptrofs.unsigned a in
- ret (Vlit (ZToValue a))
- | _, _ => error (Errors.msg "Veriloggen: translate_arr_addressing unsuported addressing")
+ if (check_address_parameter_unsigned a)
+ then ret (Vvari stack (Vlit (ZToValue (a / 4))))
+ else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset")
+ | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing")
end.
Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=
@@ -448,16 +446,6 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
end)
(enumerate 0 ns).
-Definition create_single_cycle_load (stack : reg) (addr : expr) (dst : reg) : stmnt :=
- Vnonblock (Vvar dst) (Vload stack addr).
-
-Definition create_single_cycle_store (stack : reg) (addr : expr) (src : reg) : stmnt :=
- let l0 := Vnonblock (Vvari stack addr) (Vvarb0 src) in
- let l1 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) (Vvarb1 src) in
- let l2 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb2 src) in
- let l3 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 3)) (Vvarb3 src)
- in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3.
-
Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
match ni with
(n, i) =>
@@ -472,25 +460,17 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
do _ <- declare_reg None dst 32;
add_instr n n' (nonblock dst instr)
else error (Errors.msg "State is larger than 2^32.")
- | Iload chunk addr args dst n' =>
- match chunk with
- | Mint32 =>
- if Z.leb (Z.pos n') Integers.Int.max_unsigned
- then do addr' <- translate_arr_addressing addr args;
- do _ <- declare_reg None dst 32;
- add_instr n n' $ create_single_cycle_load stack addr' dst
- else error (Errors.msg "State is larger than 2^32.")
- | _ => error (Errors.msg "Iload invalid chunk size.")
- end
- | Istore chunk addr args src n' =>
- match chunk with
- | Mint32 =>
- if Z.leb (Z.pos n') Integers.Int.max_unsigned
- then do addr' <- translate_arr_addressing addr args;
- add_instr n n' $ create_single_cycle_store stack addr' src
- else error (Errors.msg "State is larger than 2^32.")
- | _ => error (Errors.msg "Istore invalid chunk size.")
- end
+ | 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.")
@@ -596,7 +576,7 @@ 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 8 (Z.to_nat f.(fn_stacksize));
+ 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;
generated by cgit (git 2.34.1) at 2024-07-06 09:55:33 +0000