jkff.sby

[tasks]
prove
cover

[options]
prove: mode prove
cover: mode cover

[engines]
smtbmc yices

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

[files]
jkff.v

jkff.v

`default_nettype none

module jkff(
  input i_clk,
  input i_reset,
  input i_j,
  input i_k,
  output o_q,
  output o_q_bar
);

reg temp, temp_bar;

initial begin
  temp = 0;
  temp_bar = 1;
end

assign o_q = temp;
assign o_q_bar = temp_bar;

always @(posedge i_clk) begin
  if (i_reset == 1'b1) begin
    temp     <= 0;
    temp_bar <= 1;
  end else begin
    case ({i_j, i_k})
      2'b00: begin
        temp     <= temp;
        temp_bar <= temp_bar;
      end
      2'b01: begin
        temp     <= 1'b0;
        temp_bar <= 1'b1;
      end
      2'b10: begin
        temp     <= 1'b1;
        temp_bar <= 1'b0;
      end
      2'b11: begin
        temp     <= ~temp;
        temp_bar <= ~temp_bar;
      end
    endcase
  end
end

`ifdef FORMAL
  reg last_clk;

  initial assume(i_reset);
  initial last_clk = 1'b0;

  always @($global_clock) begin
    assume(i_clk == !last_clk);
  end

  always @(*) begin
    assert(o_q != o_q_bar);
  end
`endif

endmodule