diff options
Diffstat (limited to 'src/hls/HTLPargen.v')
-rw-r--r-- | src/hls/HTLPargen.v | 57 |
1 files changed, 29 insertions, 28 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 373f704..b66a704 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -27,6 +27,7 @@ Require Import compcert.lib.Maps. Require Import vericert.common.Statemonad. Require Import vericert.common.Vericertlib. Require Import vericert.hls.AssocMap. +Require Import vericert.hls.FunctionalUnits. Require Import vericert.hls.HTL. Require Import vericert.hls.Predicate. Require Import vericert.hls.RTLBlockInstr. @@ -329,6 +330,30 @@ Definition check_address_parameter_signed (p : Z) : bool := Definition check_address_parameter_unsigned (p : Z) : bool := Z.leb p Integers.Ptrofs.max_unsigned. +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). + 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?*) @@ -367,10 +392,10 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | 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.Odiv, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: div") + | Op.Odivu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: divu") + | Op.Omod, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mod") + | Op.Omodu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: modu") | 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) @@ -470,30 +495,6 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). -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 |