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

Merge pull request #366 from YosysHQ/regression_5892

add regression test for memory name escaping in smt2 comments
This commit is contained in:
Miodrag Milanović 2026-06-16 10:54:11 +02:00 committed by GitHub
commit d3e72d26e8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

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