3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-06-19 19:36:32 +00:00

add regression test for memory name escaping in smt2 comments

This commit is contained in:
N. Engelhardt 2026-06-09 17:39:25 +02:00
parent 0cb15210a8
commit 93d387d419

55
yosys_5892_memname.sby Normal file
View file

@ -0,0 +1,55 @@
[options]
mode bmc
depth 3
expect fail
[engines]
smtbmc bitwuzla
[script]
read_verilog -sv top.sv
prep -top top -flatten
[file top.sv]
module top(input logic clk, input logic [1:0] addr, input logic [7:0] data);
logic [7:0] value;
wrapper wrapper (
.clk(clk),
.addr(addr),
.data(data),
.value(value)
);
always_ff @(posedge clk) begin
assert (value != 8'hff);
end
endmodule
module wrapper(
input logic clk,
input logic [1:0] addr,
input logic [7:0] data,
output logic [7:0] value
);
uut uut (
.clk(clk),
.addr(addr),
.data(data),
.value(value)
);
endmodule
module uut(
input logic clk,
input logic [1:0] addr,
input logic [7:0] data,
output logic [7:0] value
);
logic [7:0] \mem\with\backslash [0:3];
always_ff @(posedge clk) begin
\mem\with\backslash [addr] <= data;
value <= \mem\with\backslash [addr];
end
endmodule