mirror of https://github.com/YosysHQ/yosys.git
45 lines
915 B
Plaintext
45 lines
915 B
Plaintext
|
|
read -sv << EOT
|
||
|
|
module top;
|
||
|
|
(* nomem2reg *)
|
||
|
|
logic a1 [2:3][3:1] = '{'{0, 1, 1}, '{1, 0, 1}};
|
||
|
|
|
||
|
|
always_comb begin
|
||
|
|
assert(a1[2][3] == 0);
|
||
|
|
assert(a1[2][2] == 1);
|
||
|
|
assert(a1[2][1] == 1);
|
||
|
|
assert(a1[3][3] == 1);
|
||
|
|
assert(a1[3][2] == 0);
|
||
|
|
assert(a1[3][1] == 1);
|
||
|
|
end
|
||
|
|
|
||
|
|
(* nomem2reg *)
|
||
|
|
logic [1:0] a2 [6:5][2:4] = '{'{0, 1, 2}, '{1, 0, 3}};
|
||
|
|
|
||
|
|
always_comb begin
|
||
|
|
assert(a2[6][2] == 0);
|
||
|
|
assert(a2[6][3] == 1);
|
||
|
|
assert(a2[6][4] == 2);
|
||
|
|
assert(a2[5][2] == 1);
|
||
|
|
assert(a2[5][3] == 0);
|
||
|
|
assert(a2[5][4] == 3);
|
||
|
|
end
|
||
|
|
|
||
|
|
(* nomem2reg *)
|
||
|
|
logic [1:0] a3 [-2:-1][-1:1] = '{'{0, 1, 2}, '{1, 0, 3}};
|
||
|
|
|
||
|
|
always_comb begin
|
||
|
|
assert(a3[-2][-1] == 0);
|
||
|
|
assert(a3[-2][0] == 1);
|
||
|
|
assert(a3[-2][1] == 2);
|
||
|
|
assert(a3[-1][-1] == 1);
|
||
|
|
assert(a3[-1][0] == 0);
|
||
|
|
assert(a3[-1][1] == 3);
|
||
|
|
end
|
||
|
|
endmodule
|
||
|
|
EOT
|
||
|
|
hierarchy
|
||
|
|
proc
|
||
|
|
memory
|
||
|
|
async2sync
|
||
|
|
sat -enable_undef -verify -prove-asserts
|