diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-01-11 18:45:18 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-11 18:45:18 +0000 |
commit | 489b93c3e257e37f45c1f0eafeff950b97249c3f (patch) | |
tree | 71189a2f51a87ee249b808063f2042d6a9b181df /src/hls/Scheduleoracle.v | |
parent | 05ddda4394a86f5c8ca0847f5506335fe1d1b2ab (diff) | |
download | vericert-489b93c3e257e37f45c1f0eafeff950b97249c3f.tar.gz vericert-489b93c3e257e37f45c1f0eafeff950b97249c3f.zip |
Improve definition of forest for infinite registers
Diffstat (limited to 'src/hls/Scheduleoracle.v')
-rw-r--r-- | src/hls/Scheduleoracle.v | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v index 785c1ef..2c60e96 100644 --- a/src/hls/Scheduleoracle.v +++ b/src/hls/Scheduleoracle.v @@ -185,14 +185,20 @@ 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 Rtree := Maps.ITree(R_indexed). -Definition forest : Type := Rmap.t expression. +Definition forest : Type := Rtree.t expression. Definition regset := Registers.Regmap.t val. -Notation "a # b" := (Rmap.get b a) (at level 1). -Notation "a # b <- c" := (Rmap.set b c a) (at level 1, b at next level). +Definition get_forest v f := + match Rtree.get v f with + | None => Ebase v + | Some v' => v' + end. + +Notation "a # b" := (get_forest b a) (at level 1). +Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level). Record sem_state := mk_sem_state { sem_state_stackp : val; |