From f2f21f405ae0a1f457f7bc32d5053f0a92959e72 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 9 Nov 2020 19:33:52 +0000
Subject: Change and add back HTLgen

---
 src/hls/HTLgen.v      |  8 ++++----
 src/hls/HTLgenproof.v | 25 ++++++++++++++++++++++++-
 src/hls/RTLBlock.v    |  4 ++--
 src/hls/RTLPar.v      |  6 +++---
 4 files changed, 33 insertions(+), 10 deletions(-)

(limited to 'src')

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
-- 
cgit