Johnson
A Johnson counter, also known as twisted-ring counter, is a circular shift register with the inverted output of the last stage connected to the input of the first stage. The advantages of the Johnson counter are that there are no decoding glitches, and the counter operates at high speed because there is minimum logic between the registers (simple feedback means low propagation delays and simple routing).
Challenge: Write assertions that define the core elements / characteristics for a Johnson counter. As you well know, writing assertions that emulate the RTL is useless since an error in the fundamental operations of the design (and the RTL) are not detected by the emulation of that RTL.
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
The following should work in simulations I believe I used it… The select operator
//assertion check for termcount
Prop_ter: assert property ((count=='b0)? (termcount == 1’b1) : (termcount == 1’b0));
IN RESPONSE TO: what is the meaning of ($past(count)*2+1)?
$past(count)*2 + 1 is doing a left shift by 1
This is to make sure present value of count is left shift of previous count value.
In reply to ben@SystemVerilog.us:
The following should work in simulations I believe I used it… The select operator
//assertion check for termcount
Prop_ter: assert property ((count=='b0)? (termcount == 1’b1) : (termcount == 1’b0));
IN RESPONSE TO: what is the meaning of ($past(count)*2+1)?
$past(count)*2 + 1 is doing a left shift by 1
This is to make sure present value of count is left shift of previous count value.
An odd way to do a left shift. In any case, it mimics the RTL in the algorithm; something tht should be avoided. FWIW, if failed in my simulation, and needs to be tuned.
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us