In reply to Prabhu Kamalanathan:
[quote]In reply to Tudor Timi:
On the $fell(rst_n) (rst_n is active lo) I can see your point.
However, There are issues with this $fell(rst_n) assertion.
Assume for the moment that you give to a not very experienced designer the following assertion that expressed your requirements on reset:
ap_reset_fell: assert property(disable iff(1’b0) $fell(rst_n) |=> count_out=='1); The designer would then correctly, per this requirement code the following:
ap_reset_fell: assert property(disable iff(1'b0) $fell(rst_n) |=> count_out=='1);
logic rst_reg=1'b1;
always_ff @ (posedge clk) // or negedge rst_n)
begin
rst_reg <= rst_n; // needed for the $fell
if (!rst_n && rst_reg) count_out <= '1; // $fell(rst_n)
else if (ld_enb) count_out <= data_in;
else if (count_enb)
if (count_out != 0) count_out <= count_out - 1'b1;
end
// **** HOWEVER, what I really want is
ap_reset: assert property(disable iff(1'b0) !rst_n |=> count_out=='1);
// BECAUSE, what if after rst_n==1'b0 for 5 cycles, and during that time, I have a ld_enb?
// Above code would load, when I really want the count_out to be reset to zeros.
// So the assertions would work, but the intent is failing.
****** Thus, you do not want a $rose or $fell on the reset signal. ******
Assume for the moment that I have another requirement that states that if
(count_out==0) then with 20 cycles, count_out==0; that puts a limit on the ld_enb and count.
I could code it in one of the following ways:
ap_0to0_in20_bug: assert property(count_out==0 |-> ##[1:20] count_out==0);
// With no default disable, that assertion would fail if I have a reset during the
// This is because count_out is not zero because the reset that forces it back to '1.
// To correct this, you could add the disable iff
ap_0to0_in20: assert property(disable iff(!rst_n)
count_out==0 |-> ##[1:20] count_out==0);
// However, I prefer to use the
default disable iff !rst_n;
// and to cancel that effect in special assertions, I set in the assertion
// disable iff(1'b0)
ap_reset: assert property(disable iff(1'b0) !rst_n |=> count_out=='1);
Correct! That is why assertions should be reviewed!
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- 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