diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-04-04 13:13:37 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-04-04 13:13:37 +0100 |
| commit | 2cec98b19da0abd58f017dadfd487a1c9caa96b3 (patch) | |
| tree | a1ce51b515e7ff0bdb792ebe969213fb7f25a9ec /src/hls/HTL.v | |
| parent | e57c1968ec6dddeb95f815515fd501f4a25d6901 (diff) | |
| download | vericert-2cec98b19da0abd58f017dadfd487a1c9caa96b3.tar.gz vericert-2cec98b19da0abd58f017dadfd487a1c9caa96b3.zip | |
Finish store proof without admit
Diffstat (limited to 'src/hls/HTL.v')
| -rw-r--r-- | src/hls/HTL.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 92dc48c..98ea6d0 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -60,6 +60,11 @@ Record ram := mk_ram { 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)%positive }. Record module: Type := @@ -135,7 +140,7 @@ Inductive exec_ram: forall ra ar r d_in addr en wr_en u_en, Int.eq en u_en = false -> Int.eq wr_en (ZToValue 0) = false -> - (Verilog.assoc_blocking ra)!(ram_en r) = Some en -> + (Verilog.assoc_blocking ra)#(ram_en r, 32) = en -> (Verilog.assoc_blocking ra)!(ram_u_en r) = Some u_en -> (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some wr_en -> (Verilog.assoc_blocking ra)!(ram_d_in r) = Some d_in -> @@ -145,7 +150,7 @@ Inductive exec_ram: | exec_ram_Some_read: forall ra ar r addr v_d_out en u_en, Int.eq en u_en = false -> - (Verilog.assoc_blocking ra)!(ram_en r) = Some en -> + (Verilog.assoc_blocking ra)#(ram_en r, 32) = en -> (Verilog.assoc_blocking ra)!(ram_u_en r) = Some u_en -> (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some (ZToValue 0) -> (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> |