sby error: Async reset \rst yields non-constant value 4'mmmm #321
Description
As this is my first issue creation, kindly pardon me for any mistakes in issue format or details etc.
Following error is seen when I try to compile following file:
SBY 21:40:10 [fifo_basic] base: ERROR: Async reset \rst yields non-constant value 4'mmmm for signal $past$fifo.v:62$1$0
fifo.v file:
Specifically due to this line:
a_counts: assert (asrt_fifo_usedw == 0 || asrt_fifo_usedw == $past(asrt_fifo_usedw)
SBY file:
[tasks]
basic bmc
nofullskip prove
cover
basic cover : default
[options]
cover:
mode cover
--
prove:
mode prove
--
bmc:
mode bmc
--
[engines]
smtbmc boolector
[script]
nofullskip: read -define NO_FULL_SKIP=1
read -formal fifo.v
prep -top fifo
[files]
ram.v
fifo.v
`timescale 1ns / 1ps
`include "ram.v"
module fifo #(
parameter WIDTH = 8,
parameter DEPTH = 16
)(
input wire clk,
input wire rst,
input wire wr_en,
input wire [WIDTH-1:0]wr_data,
input wire rd_en,
output wire [WIDTH-1:0]rd_data,
output wire fifo_full,
output wire fifo_empty,
output reg [$clog2(DEPTH)-1:0]fifo_usedw
);
reg [$clog2(DEPTH)-1:0] wr_addr,
rd_addr;
reg [WIDTH-1:0] wr_data_pipe;
reg wr_en_actual,
rd_en_actual;
wire [WIDTH-1:0] rd_data_int;
wire [$clog2(DEPTH)-1:0] asrt_fifo_usedw;
assign asrt_fifo_usedw = fifo_usedw;
always @ (posedge clk, negedge rst) begin
if (!rst) begin
fifo_usedw <= 0;
end else begin
// the problem is that here priority is given to
// WR_EN over RD_EN, what happens when both are high at the same time?
// We wont increment the fifo_usedw
// instead of checking for WR_EN and RD_EN high at same time,
// checking for their exclusivity
a_oflow: assert (asrt_fifo_usedw <= DEPTH);
a_counts: assert (asrt_fifo_usedw == 0
|| asrt_fifo_usedw == $past(asrt_fifo_usedw)
|| asrt_fifo_usedw == $past(asrt_fifo_usedw) + 1
|| asrt_fifo_usedw == $past(asrt_fifo_usedw) - 1);
if (wr_en && !rd_en) begin
fifo_usedw <= fifo_usedw + 1;
end else if (rd_en && !wr_en) begin
fifo_usedw <= fifo_usedw - 1;
end else begin
fifo_usedw <= fifo_usedw;
end
end
end
assign fifo_full = (fifo_usedw == DEPTH);
assign fifo_empty = (fifo_usedw == 0);
assign rd_data = (rd_en_actual) ? rd_data_int : 'b0;
// because the wr_en_actual is delayed by 1 cycle,
// I need to pipe the wr_data for 1 cycle
always @ (posedge clk) begin
if (rst) begin
wr_en_actual <= 0;
wr_data_pipe <= 0;
end else begin
wr_data_pipe <= wr_data;
if (wr_en && !fifo_full) begin
wr_en_actual <= 1;
end else begin
wr_en_actual <= 0;
end
end
end
always @ (posedge clk) begin
if (rst) begin
rd_en_actual <= 0;
end else begin
if (rd_en && !fifo_empty) begin
rd_en_actual <= 1;
end else begin
rd_en_actual <= 0;
end
end
end
always @ (posedge clk) begin
if (rst) begin
wr_addr <= 0;
end else begin
if (wr_en_actual) begin
wr_addr <= wr_addr + 1;
end else begin
wr_addr <= wr_addr;
end
end
end
always @ (posedge clk) begin
if (rst) begin
rd_addr <= 0;
end else begin
if (rd_en_actual) begin
rd_addr <= rd_addr + 1;
end else begin
rd_addr <= rd_addr;
end
end
end
ram #(.WIDTH(8), .DEPTH(16))
ram_0 (
.clk ( clk ),
.wr_en ( wr_en_actual ),
.wr_addr ( wr_addr ),
.wr_data ( wr_data_pipe ),
.rd_addr ( rd_addr ),
.rd_data ( rd_data_int )
);
endmodule