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!
ben2
March 16, 2015, 10:46pm
2
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
SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
Component Design by Example ", 2001 ISBN 0-9705394-0-1
VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
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?
ben2
March 17, 2015, 10:20pm
4
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