Hi All,
How should I handle the Clock Crossing domains in my assertions?
Let’s take an example of DPR FIFO where each side works on a different clock domain - signals on SideA are synchronized to clkA,
signals on SideB are synchronized to clkB. How can I check/assert that all the data, which was pushed from SideA, then was pop-ed on the SideB? The clkA and clkB are fully asynchronous.
Thank you!
The code below should do the job, but you’ll need other assertions regarding writing on full, reading an empty.
module fifo_async (
// Outputs
wfull, rdata, rempty,
// Inputs
wrst_n, wclk, wen, wdata, rrst_n, rclk, ren
) ;
parameter WIDTH = 8;
output wfull; // Write full
output [WIDTH - 1: 0] rdata; // read data
output rempty; // fifo empty
input wrst_n; // asynchronous active low write reset
input wclk; // write clock input
input wen; // fifo active hi write enable
input [WIDTH-1:0] wdata; // write data
input rrst_n; // read reset active low
input rclk; // fifo read clock
input ren; // fifo read enable (active hi)
property p_async_fifo;
bit[WIDTH-1:0] v_wdata;
@(posedge wclk) (!wfull && wen, v_wdata=wdata) |->
@(posedge rclk) ##[1:$] !rempty && ren ##0 rdata==v_wdata;
endproperty
ap_async_fifo: assert property(p_async_fifo));
Below is code on a sync fifo, but it should help you consider other assertions for your designs (this is from stuff from my books).
/ Activating reset during interesting corner cases
// is covered via cover directives.
property p_t1_full; @ (posedge clk)
full ##1 reset_n==0;
endproperty : p_t1_full
cp_t1_full_1: cover property (p_t1_full);
property p_t2_afull; @ (posedge clk)
almost_full ##1 reset_n==0;
endproperty : p_t2_afull
cp_t2_afull_1: cover property (p_t2_afull);
property p_t3_empty; @ (posedge clk)
empty ##1 reset_n==0;
endproperty : p_t3_empty
cp_t3_empty_1: cover property (p_t3_empty);
property p_t4_aempty; @ (posedge clk)
almost_empty ##1 reset_n==0;
endproperty : p_t4_aempty
cp_t4_aempty_1 : cover property (p_t4_aempty);
// turned unbounded into bounded
property p_push_pop_sequencing;
@ (posedge clk) push |=> ##[0:99] pop;
endproperty : p_push_pop_sequencing
// coverage of sequences
cp_push_pop_sequencing : cover property (p_push_pop_sequencing);
property p_error_flag;
@ (posedge clk)
(push && full && !pop) || (pop && empty) == error;
endproperty : p_error_flag
ap_error_flag : assert property (p_error_flag);
begin: no_error
// never a push and full and no pop
property p_push_error;
@ (posedge clk)
not (push && full && !pop);
endproperty : p_push_error
// ap_push_error : assert property (p_push_error);
ap_push_error : assume property (p_push_error);
// never a pop on empty
property p_pop_error;
@ (posedge clk)
not (pop && empty);
endproperty : p_pop_error
// ap_pop_error : assert property (p_pop_error);
ap_pop_error : assume property (p_pop_error);
property p_push_data;
word_t data;
logic [BIT_DEPTH-1 : 0] ptr;
(push, data = data_in, ptr = wr_ptr) |=> buffer[ptr] == data;
endproperty : p_push_data
ap_push_data : assert property (@ (posedge clk) disable iff (!reset_n) p_push_data);
property p_pop_data; //===== From book:
pop |-> data_out == buffer[rd_ptr];
endproperty : p_pop_data
ap_pop_data : assert property (@ (posedge clk) disable iff (!reset_n) p_pop_data);
//===== correct pointer manuipulation:
property p_push;
@ (posedge clk) disable iff (!reset_n)
push |=> wr_ptr == ($past(wr_ptr) + 1 ) % DEPTH;
endproperty : p_push
ap_push : assert property (p_push);
property p_pop;
@ (posedge clk) disable iff (!reset_n)
pop |=> rd_ptr == ($past(rd_ptr) + 1 ) % DEPTH;
endproperty : p_pop
ap_pop: assert property (p_pop);
property p_nopush;
@ (posedge clk) disable iff (!reset_n)
!push |=> wr_ptr == $past(wr_ptr);
endproperty : p_nopush
ap_nopush : assert property (p_nopush);
property p_nopop;
@ (posedge clk) disable iff (!reset_n)
!pop |=> rd_ptr == $past(rd_ptr);
endproperty : p_nopop
ap_nopop: assert property (p_nopop);
end // no_error
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
In reply to ben@SystemVerilog.us:
Could you please explain these two properties:
property p_push_data;
word_t data;
logic [BIT_DEPTH-1 : 0] ptr;
(push, data = data_in, ptr = wr_ptr) |=> buffer[ptr] == data;
endproperty : p_push_data
ap_push_data : assert property (@ (posedge clk) disable iff (!reset_n) p_push_data);
property p_pop_data; //===== From book:
pop |-> data_out == buffer[rd_ptr];
endproperty : p_pop_data
ap_pop_data : assert property (@ (posedge clk) disable iff (!reset_n) p_pop_data);
Where is the ‘buffer[ptr]’ defined/declared? Is the array common/visible for these two properties?
In reply to dmitryl:
The goal was to demonstrate the concepts. I copied all the code in http://SystemVerilog.us/ccntrl.tar
// file fifo_props3.sv
parameter BIT_DEPTH = 4; // 2**BIT_DEPTH = depth of fifo
parameter DEPTH = 2**BIT_DEPTH ;
parameter FULL = DEPTH - 1; // int'(2** BIT_DEPTH -1);
parameter ALMOST_FULL = 10; // int'(3*FULL / 4);
parameter ALMOST_EMPTY = 4; //int'(FULL/4);
parameter WIDTH = 32;
typedef logic [WIDTH-1 : 0] word_t;
typedef word_t [0 : (2**BIT_DEPTH-1)] buffer_t;
Ben SystemVerilog.us