diff options
| -rw-r--r-- | src/hls/GiblePargen.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 0462e28..11da966 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -287,6 +287,17 @@ Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pr | RBexit p c => lst end. +(*Compute match update (T, mk_forest (PTree.empty _) (PTree.empty _) (NE.singleton (T, EEbase))) + (RBop None Op.Odiv (1::2::nil) 3) with + | Some x => + match update x (RBop None (Op.Ointconst (Int.repr 10)) nil 3) with + | Some y => + RTree.get (Reg 3) (forest_regs (snd y)) + | None => None + end + | None => None + end.*) + (*| Implementing which are necessary to show the correctness of the translation validation by showing that there aren't any more effects in the resultant RTLPar |