From 9403299d1a481ea4422524b6caa0d78e4c20fbaf Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 16 May 2023 23:31:37 +0100 Subject: Work on scheduling proof --- src/hls/GiblePargen.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/hls/GiblePargen.v') 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 -- cgit