aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorJames Pollard <james@pollard.dev>2020-06-18 00:01:11 +0100
committerJames Pollard <james@pollard.dev>2020-06-18 00:01:11 +0100
commit9e49a65aa01e79b85a35d1dd15f45ee89e3e9906 (patch)
tree842af2f1875c80e661377572a9fc4e8c42028673
parent9a65ca2731adf234f5ce946503314267ced62a44 (diff)
downloadvericert-kvx-9e49a65aa01e79b85a35d1dd15f45ee89e3e9906.tar.gz
vericert-kvx-9e49a65aa01e79b85a35d1dd15f45ee89e3e9906.zip
Fix array semantics behaviour for undefined values.
-rw-r--r--src/verilog/Verilog.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index d20ffcd..4144632 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -80,7 +80,7 @@ Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr :
Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
match a ! r with
| None => None
- | Some arr => Option.join (array_get_error i arr)
+ | Some arr => Some (Option.default (NToValue 32 0) (Option.join (array_get_error i arr)))
end.
Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=