Closed christian-krieg closed 2 years ago
ZipCPU
commented
3 years ago Looks like an overflow issue. For a temporary solution, assign a combinatorial register to (cnt - $past(cnt)):
reg [9:0] f_tmp;
always @(posedge clk)
begin
f_tmp = 0;
if (!rst) begin
// ...
f_tmp = cnt - $past(cnt); // Note the *blocking* assignment
if ($past(mode))
begin
if (!$past(rst))
begin
if ($past(cnt) == -162)
assert(f_tmp == 10);
else if // ...etc.
Dan
christian-krieg
commented
3 years ago Hi Dan,
Thanks for your workaround!
It turned out to be an issue with the constants, which are by default 32 bits wide. The Verific frontend trims these values to fit in the 10-bit wide cnt register, while the Yosys frontend doesn't. Explicitly specifying the number format as 10-bit wide signed decimal solves the issue.
Here is an updated version of counter.v:
module counter (clk, rst, mode, cnt);
input wire clk;
input wire rst;
input wire mode;
output reg signed [9:0] cnt = -10'sd28;
always @(posedge clk) begin
if (rst)
cnt <= -10'sd28;
else begin
if (mode) begin
if (cnt != -10'sd162) begin
if (cnt <= 10'sd277) begin
cnt <= cnt + 10'sd5;
end
end else if (cnt <= 10'sd272) begin
cnt <= cnt + 10'sd10;
end
// mode = 0
end else begin
if (cnt != -10'sd148) begin
if (cnt >= -10'sd334 ) begin
cnt <= cnt + -10'sd9;
end
end else if (cnt >= -10'sd325) begin
cnt <= cnt + -10'sd18;
end
end
end
end
`ifdef FORMAL
reg init = 1;
always @(posedge clk) begin
if (init) assume(rst);
else assume(!rst);
init <= 0;
end
always @(posedge clk) begin
if (rst) begin
assert (cnt == -10'sd28);
end
if (!rst) begin
//
// Check if counter value is never lower than MIN, larger than MAX, or
// equal to INV
//
assert (cnt <= 10'sd282);
assert (cnt >= -10'sd343);
assert (cnt != -10'sd157);
//
// Check if the counter value is correctly incremented and decremented
//
// Counting up
if ($past(mode)) begin
if (!$past(rst)) begin
if ($past(cnt) == -10'sd162) // INV - INC, counter jumped over INV
assert ((cnt - $past(cnt)) == 10'sd10);
else if ($past(cnt) <= 10'sd282 && $past(cnt) > 10'sd277) // cnt was near MAX
assert ((cnt - $past(cnt)) == 10'sd0);
else
assert ((cnt - $past(cnt)) == 10'sd5);
end
end
// Counting down
if (!$past(mode)) begin
if (!$past(rst)) begin
if ($past(cnt) == -10'sd148) // INV + DEC, counter jumped over INV
assert (($past(cnt) - cnt) == 10'sd18);
else if ($past(cnt) >= -10'sd343 && $past(cnt) < -10'sd334) // cnt was near MIN
assert (($past(cnt) - cnt) == 10'sd0);
else
assert (($past(cnt) - cnt) == 10'sd9);
end
end
end
end
`endif
endmoduleReopening this issue because it would be nice if read_verilog would behave as read. Leaving it like it is potentially makes the Verilog code less readable, and IMO less usable.
I have a simple counter implementation along with some simple properties on the counter value (
counter.v):The following SBY configuration file (
vrf.sby) specifies two tasksyosysandverific, each using either the Yosys or the Verific Verilog frontend.A verification run in
provemode succeeds for the case where I read the design with Verific, but it fails when I read it with Yosys. So,succeeds, whereas
fails with the following report:
The failing asserttion is given here (
counter.v:68.29-69.61):I cannot figure out what's the problem here. What am I missing?