From 05ddda4394a86f5c8ca0847f5506335fe1d1b2ab Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 11 Jan 2021 18:36:17 +0000 Subject: Add top level semantics for forests --- src/hls/Scheduleoracle.v | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v index bc62d47..785c1ef 100644 --- a/src/hls/Scheduleoracle.v +++ b/src/hls/Scheduleoracle.v @@ -185,7 +185,9 @@ Using IMap we can create a map from resources to any other type, as resources ca identified as positive numbers. |*) -Module Rmap := Maps.IMap(R_indexed). +Module Rmap := Maps.IMap(R_indexed). + +Definition forest : Type := Rmap.t expression. Definition regset := Registers.Regmap.t val. @@ -248,6 +250,22 @@ with sem_val_list : sem_val_list parent st l lv -> sem_val_list parent st (Econs e l) (v :: lv). +Inductive sem_regset : + val -> sem_state -> forest -> regset -> Prop := + | Sregset: + forall parent st f rs', + (forall x, sem_value parent st (f # (Reg x)) (Registers.Regmap.get x rs')) -> + sem_regset parent st f rs'. + +Inductive sem : + val -> sem_state -> forest -> sem_state -> Prop := + | Sem: + forall st rs' fr' m' f parent, + sem_regset parent st f rs' -> + sem_mem parent st (f # Mem) m' -> + sem parent st fr' (mk_sem_state (sem_state_stackp st) rs' m'). + + End SEMANTICS. Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := -- cgit