In reply to pavan yala:
In reply to ben@SystemVerilog.us:
I can come up with these checks:
default clocking cb @(posedge clk); endclocking
default disable iff(!rst_n);
//Disable the assertion check for the Current count = 10000
Prop_count: assert property disable iff(!rst_n || (count[WIDTH-1] && ($countones(count) == 1)))
(1 ##1 (count == ($past(count)*2+1)));
//assertion check for the Current count = 10000
Prop_count_last: assert property count[WIDTH-1] && ($countones(count)==1) |=> (count==0));
//assertion check for termcount
Prop_ter: assert property ((count=='b0)? 1’b1 : 1’b0);
Good that you took a look at this model. Aside from coding problems, two of your 3 assertions did not work. Below is corrected coding (for syntax) of your code along with some comments.
//Disable the assertion check for the Current count = 10000
Prop_count: assert property ( // (<-- ** FAILS IN simulation
disable iff(!rst_n || (count[WIDTH-1] && ($countones(count) == 1)))
1 ##1 count == ($past(count)*2+1));
[Ben] Why are disabling the assertion when count=100000? That is a valid count!
Also, what is the meaning of ($past(count)*2+1)?
The next count == previous count multiplied by 2, and the result added to 1?
??
//******************************
//assertion check for the Current count = 10000
Prop_count_last: assert property (count[WIDTH-1] && ($countones(count)==1) |=> (count==0));
[Ben] Valid assertion
//******************************
//assertion check for termcount
Prop_ter: assert property ((count=='b0)? 1'b1 : 1'b0); // <-- FAILS IN simulation
[Ben] I never used that form in an assertion. You probably meant something like
(count=='b0)|=> count==1)
//******************************
As a general comment, you use way too many parentheses, that is confusing and hard to read.
When you write an assertion, you need to look at the core of what the design performs, and address this core.
Core characteristics of Johnson counter include:
- Excluding the reset condition, every count value is repeated every 2*WIDTH of the register; thus, a 6-bit Johnson counter would have every count repeat every 12 cycles.
- At every cycle, the count is different than the previous count.
- Upon a synchronous active reset, the count is reset to ZERO, and the terminal count is set to ONE.
- If the count is ZERO, then terminal count is ONE.
- If the count is not ZERO, then terminal count is ZERO.
For a counter of width WIDTH, the following can be expressed:
module johnson #(WIDTH = 6) (
output logic[WIDTH-1:0] count, // counter output
output logic termcount, //terminal count
input logic clk, rst_n);
always_ff @ (posedge clk or negedge rst_n) begin
if (!rst_n) begin
count <= '0;
termcount <= 1'b1;
end
else begin
count <= {count[WIDTH-2:0], !count[WIDTH-1] };
termcount <= (count[WIDTH - 1] == 1 &&
count[WIDTH - 2] == 0);
end
end
// Assertions
// 1. 50% duty output once per cycle on each of the bits
default clocking @(posedge clk); endclocking
default disable iff !rst_n;
ap_duty_cycle: assert property(##(2*WIDTH) count==$past(count, 12));
ap_next: assert property(##1 count !=$past(count, 1) );
ap_reset: assert property(disable iff(0) !rst_n |=> count=='0 && termcount==1'b1);
ap_termcount1: assert property(count=='0 |-> termcount==1'b1);
ap_termcount0: assert property(count!='0 |-> termcount==1'b0);
endmodule // johnson
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