diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-03-31 20:45:15 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-03-31 20:45:15 +0100 |
commit | 2837868fcc427b2161b083f33d3de495f0c21bf7 (patch) | |
tree | af64714106456b6c5afb28835735a75e634754a8 /src/hls/HTL.v | |
parent | ff10c279b5ddbac503ed0da1f1e0c25cd0979749 (diff) | |
download | vericert-2837868fcc427b2161b083f33d3de495f0c21bf7.tar.gz vericert-2837868fcc427b2161b083f33d3de495f0c21bf7.zip |
Add memory disable
Diffstat (limited to 'src/hls/HTL.v')
-rw-r--r-- | src/hls/HTL.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 32b91ab..4899671 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -139,7 +139,7 @@ Inductive exec_ram: (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some wr_en -> (Verilog.assoc_blocking ra)!(ram_d_in r) = Some d_in -> (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> - exec_ram ra ar (Some r) ra + exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) ra (ZToValue 0)) (Verilog.nonblock_arr (ram_mem r) (valueToNat addr) ar d_in) | exec_ram_Some_read: forall ra ar r addr v_d_out en, @@ -149,7 +149,8 @@ Inductive exec_ram: (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar) (ram_mem r) (valueToNat addr) = Some v_d_out -> - exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) ar + exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) + (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) (ZToValue 0)) ar | exec_ram_None: forall r a, exec_ram r a None r a. |