mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-06 22:34:07 +00:00
Test signals with nonzero start offsets in aim files with smtbmc
This commit is contained in:
parent
079df4d95f
commit
a434252ca1
1
tests/.gitignore
vendored
1
tests/.gitignore
vendored
|
@ -10,3 +10,4 @@
|
|||
/junit_*/
|
||||
/submod_props*/
|
||||
/multi_assert*/
|
||||
/aim_vs_smt2_nonzero_start_offset*/
|
||||
|
|
33
tests/aim_vs_smt2_nonzero_start_offset.sby
Normal file
33
tests/aim_vs_smt2_nonzero_start_offset.sby
Normal file
|
@ -0,0 +1,33 @@
|
|||
[tasks]
|
||||
bmc
|
||||
prove
|
||||
|
||||
[options]
|
||||
bmc: mode bmc
|
||||
prove: mode prove
|
||||
expect fail
|
||||
wait on
|
||||
|
||||
[engines]
|
||||
bmc: abc bmc3
|
||||
bmc: abc sim3
|
||||
prove: aiger avy
|
||||
prove: aiger suprove
|
||||
prove: abc pdr
|
||||
|
||||
[script]
|
||||
read -sv test.sv
|
||||
prep -top test
|
||||
|
||||
[file test.sv]
|
||||
module test (
|
||||
input clk,
|
||||
input [8:1] nonzero_offset
|
||||
);
|
||||
reg [7:0] counter = 0;
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (counter == 3) assert(nonzero_offset[1]);
|
||||
counter <= counter + 1;
|
||||
end
|
||||
endmodule
|
Loading…
Reference in a new issue