diff options
| -rw-r--r-- | include/hls.h | 39 | ||||
| -rw-r--r-- | src/hls/HTLgen.v | 8 | ||||
| -rw-r--r-- | src/hls/HTLgenproof.v | 25 | ||||
| -rw-r--r-- | src/hls/RTLBlock.v | 4 | ||||
| -rw-r--r-- | src/hls/RTLPar.v | 6 |
5 files changed, 66 insertions, 16 deletions
diff --git a/include/hls.h b/include/hls.h index b243fea..61c336b 100644 --- a/include/hls.h +++ b/include/hls.h @@ -4,8 +4,8 @@ /* * Divider C implementation for faster frequency division. */ -unsigned int divider(unsigned int x, unsigned int y) { - unsigned int r0, q0, y0, y1; +unsigned divider_fast(unsigned x, unsigned y) { + unsigned r0, q0, y0, y1; r0 = x; q0 = 0; @@ -15,16 +15,29 @@ unsigned int divider(unsigned int x, unsigned int y) { y1 = 2 * y1; } while (y1 <= x); do { - y1 = y1 / 2; - q0 = 2 * q0; + y1 /= 2; + q0 *= 2; if (r0 >= y1) { - r0 = r0 - y1; - q0 = q0 + 1; + r0 -= y1; + q0++; } } while ((int)y1 != (int)y0); return q0; } +unsigned divider(unsigned x, unsigned y) { + unsigned q0, acc; + q0 = 0; + acc = y; + + while (acc <= x) { + q0++; + acc += y; + } + + return q0; +} + /* * Signed division operation for faster frequency division. */ @@ -42,4 +55,18 @@ int sdivider(int N, int D) { } } +int sdivider_fast(int N, int D) { + if (D < 0) { + if (N < 0) + return divider_fast(-N, -D); + else + return -divider_fast(N, -D); + } else { + if (N < 0) + return -divider_fast(-N, D); + else + return divider_fast(N, D); + } +} + #endif diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 68e0293..5f0f8bf 100644 --- a/src/hls/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/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 22f8f57..6095290 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -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,23 @@ 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. + 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 +775,8 @@ 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.*) + - admit. + - admit. - 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/hls/RTLBlock.v b/src/hls/RTLBlock.v index 117d21b..7984ac9 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -67,9 +67,9 @@ Definition funsig (fd: fundef) := Definition successors_instr (i : control_flow_inst) : list node := match i with -(* | RBcall sig ros args res s => s :: nil + | RBcall sig ros args res s => s :: nil | RBtailcall sig ros args => nil - | RBbuiltin ef args res s => s :: nil*) + | RBbuiltin ef args res s => s :: nil | RBcond cond args ifso ifnot => ifso :: ifnot :: nil | RBjumptable arg tbl => tbl | RBreturn optarg => nil diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 0e94fd5..0d37985 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -67,9 +67,9 @@ Definition funsig (fd: fundef) := 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*) + | 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 |