SBY · Yosys

Formal

Write properties, explore free inputs and read the counterexample. Choose bounded checking, induction, PDR or qualified liveness.

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module top(input clk, rst, en);
  reg [3:0] count=0;
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end
    else begin assume(!rst); end
    if (rst) count<=0;
    else if (en) count<=count+1'b1;
  end
endmodule

assert property (@(posedge clk) disable iff (rst) count < 4'd10);

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.

Formal

design.sv

props.sv