diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-11-15 21:01:26 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-15 21:01:26 +0000 |
| commit | c54576bce7bccb71a807f8331b9e9d7fbdf1eec3 (patch) | |
| tree | 8432046f1c85c9efaef404298700e20ecadc6265 | |
| parent | 39200b933b230579b90089539216077f016bacc5 (diff) | |
| download | vericert-c54576bce7bccb71a807f8331b9e9d7fbdf1eec3.tar.gz vericert-c54576bce7bccb71a807f8331b9e9d7fbdf1eec3.zip | |
Remove unnecessary RAM
| -rw-r--r-- | src/hls/HTL.v | 17 |
1 files changed, 1 insertions, 16 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 8cebbfd..d5a99fc 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -31,6 +31,7 @@ Require Import vericert.common.Vericertlib. Require Import vericert.hls.ValueInt. Require Import vericert.hls.AssocMap. Require Import vericert.hls.Array. +Require Import vericert.hls.FunctionalUnits. Require vericert.hls.Verilog. Local Open Scope positive. @@ -54,22 +55,6 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := In p0 (map fst (Maps.PTree.elements m)) -> (Z.pos p0 <= Integers.Int.max_unsigned)%Z. -Record ram := mk_ram { - ram_size: nat; - ram_mem: reg; - ram_en: reg; - ram_u_en: reg; - ram_addr: reg; - ram_wr_en: reg; - ram_d_in: reg; - ram_d_out: reg; - ram_ordering: (ram_addr < ram_en - /\ ram_en < ram_d_in - /\ ram_d_in < ram_d_out - /\ ram_d_out < ram_wr_en - /\ ram_wr_en < ram_u_en) -}. - Definition module_ordering a b c d e f g := a < b < c /\ c < d < e /\ e < f < g. Record module: Type := |