3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-07-10 05:16:17 +00:00

Move test to proper place and remove empty dir

This commit is contained in:
Miodrag Milanovic 2026-07-08 09:41:11 +02:00
parent 6e3dc04d92
commit 985d7bdd3d
3 changed files with 0 additions and 6 deletions

View file

@ -1,4 +0,0 @@
*
!Makefile
!.gitignore
!*.sby

View file

@ -1,2 +0,0 @@
SUBDIR=parser
include ../make/subdir.mk

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