diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-01-11 18:36:17 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-11 18:36:17 +0000 |
commit | 05ddda4394a86f5c8ca0847f5506335fe1d1b2ab (patch) | |
tree | 4a57e4a01e0015690b31bccd6475d1f624e08373 /src/hls | |
parent | 9e2aca04a7af7987fb8226fb9e211194a7f195ff (diff) | |
download | vericert-05ddda4394a86f5c8ca0847f5506335fe1d1b2ab.tar.gz vericert-05ddda4394a86f5c8ca0847f5506335fe1d1b2ab.zip |
Add top level semantics for forests
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/Scheduleoracle.v | 20 |
1 files changed, 19 insertions, 1 deletions
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 := |