SVA CHALLENGE: Write assertions for a Johnson counter

SystemVerilog
,
2

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);