ror.sby

[options]
mode prove
depth 10

[engines]
smtbmc

[script]
read_verilog -formal ror.v
prep -top ror

[files]
ror.v

ror.v

`default_nettype none
module ror
  (
   input 		clk,
   output reg [LEN-1:0] q = 'd1);

   parameter LEN = 4;

   always @(posedge clk)
     q <= {q[0], q[LEN-1:1]};

`ifdef FORMAL
   reg [LEN-1:0] 	qvalid = 'd0;

   always @(posedge clk) begin
      qvalid <= {1'b1, qvalid[LEN-1:1]};
      cover(&(qvalid));
      
      if (&(qvalid))
	assert (q == $past(q, LEN));
   end
`endif
endmodule