SVA CHALLENGE: Write assertions for a Johnson counter

In reply to ben@SystemVerilog.us:

Ben,

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.