diff options
Diffstat (limited to 'src/hls/GiblePargen.v')
| -rw-r--r-- | src/hls/GiblePargen.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 11da966..08806aa 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -40,6 +40,8 @@ Require Import vericert.hls.GiblePargenproofEquiv. Import NE.NonEmptyNotation. +Import ListNotations. + #[local] Open Scope positive. #[local] Open Scope forest. #[local] Open Scope pred_op. @@ -309,6 +311,11 @@ Get a sequence from the basic block. Definition abstract_sequence (b : list instr) : option forest := Option.map snd (mfold_left update b (Some (Ptrue, empty))). +Compute Option.bind (fun x => RTree.get (Reg 3) (forest_regs x)) + (abstract_sequence + [RBop None Op.Odiv [1;2] 3; + RBop None (Op.Ointconst (Int.repr 10)) nil 3]). + (*| Check equivalence of control flow instructions. As none of the basic blocks should have been moved, none of the labels should be different, meaning the |