diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-16 23:31:37 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-16 23:31:37 +0100 |
| commit | 9403299d1a481ea4422524b6caa0d78e4c20fbaf (patch) | |
| tree | ba457e3550ca8add319d22a124e7cbbcc8639c7b /src/hls/GiblePargen.v | |
| parent | b24fc9492bafb61761f847ec4829eaf5b5d88c7b (diff) | |
| download | vericert-9403299d1a481ea4422524b6caa0d78e4c20fbaf.tar.gz vericert-9403299d1a481ea4422524b6caa0d78e4c20fbaf.zip | |
Work on scheduling proof
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 |