A Pipeline: Instruction-Level Checking

Check a pipeline through its retirement port: one symbolic register for "read what was written", the ISA function for "computed what the ISA says", and the helpers that make it a proof.

Lesson: F8.7
Time: 25 min
Runs on: SymbiYosys
Check: 4 questions

A three-stage pipeline forwarded results from writeback to issue. A later change added a bypass from execute with the priority the wrong way round. It broke one case: a register written by two instructions in a row and read by the third. The random instruction stream rarely made the pattern, and the wrong value looked like a data error.

Three Stages and a Side PortA free instruction enters every cycle. Operands are read at issue, with bypasses from execute and writeback. Each instruction is reported on the retirement port with the values it used and wrote.

data: where the transaction goes

Read the diagram as text

issue: read rs1, rs2: execute bypass, else writeback bypass, else the register file
execute: ADD, SUB, AND, ADDI
writeback: writes rd in the four-entry register file
retirement port: rvfi_valid, op, rs1/rs2 index and value used, rd index and value written

issue → execute
execute → writeback
execute → issue: execute bypass
writeback → issue: writeback bypass
writeback → retirement port

The same idea as riscv-formal's RVFI, nine signals instead of dozens. Pipelining itself is R4.3. pipe3 has 147 flops.

The Reg Check: One Register Stands for All

Two writes to the tracked register, then a read of the older one

Measured with smtbmc yices: FAIL at reported step 7, 0.6 s. Ops: 0 ADD, 1 SUB, 2 AND, 3 ADDI.

Pick a register index as a free constant, keep a shadow of its value updated at retirement, and assert that every retired read of that register used the shadow. One index, every register (F4.4). The trace marks the three instructions that matter. Two writes retire at steps 4 and 5; the read at step 6 took the older result.

The Insn Check, and Why Both

Check	Correct design	BUG_FWD_PRIO	BUG_ALU (SUB off by one on a borrow)
reg: reads see the last write	BMC PASS to depth 20; `abc pdr` Prove PASS (abc pdr)	FAIL at reported step 7	BMC PASS to depth 20
insn: result is the ISA function of the operands	Prove PASS (k = 3)	BMC PASS to depth 20	FAIL at reported step 6

Every run is bmc depth 20 unless noted, with smtbmc yices.

insn says each result is the ISA function of the operand values the port reports. It cannot see a wrong operand, because it trusts the reported one. reg cannot see a wrong result, because it only checks reads. Each is blind to the other's bug.

The riscv-formal suite runs more checks on the same port: pc_fwd and pc_bwd for the program counter, unique and causal for ordering, and a liveness check. This toy has no program counter, so two are enough.

Making It a Proof

Proof run, correct design	Measured result
reg, prove k = 8	UNKNOWN at k = 8 (base case passed, induction step failed), 0.6 s
reg plus helpers, prove k = 2	Prove PASS (k = 2), 0.6 s
reg, `abc pdr`	Prove PASS (abc pdr), 3.3 s
insn, prove k = 2	UNKNOWN at k = 2 (base case passed, induction step failed), 0.5 s
insn, prove k = 3	Prove PASS (k = 3), 0.5 s

smtbmc yices unless noted.

A register can sit untouched for any number of cycles, so no k makes the reg check inductive alone. The helpers state what the pipeline keeps true: the register file matches the shadow, and every operand in flight matches what issue should have seen (F4.6).

The alternative is sequential equivalence against an unpipelined reference (F6.2). It needs a golden model and a mapping; the instruction checks need only the ISA. Use SEC when a reference exists, these checks when the ISA is the spec.

Asked in Interviews

Question	Answer
How does riscv-formal check a core?	Through a retirement port, with per-instruction checks (insn, reg, pc_fwd, pc_bwd, unique, causal, liveness) that never look inside the pipeline.
SEC or property checking for a pipeline?	SEC when a reference core exists; instruction checks when the ISA is the spec.
Why both reg and insn?	Each is blind to the other's bug class: a wrong operand passes insn, a wrong result passes reg.

Try It

The lab task. The twins run the covers, the proofs and the insn check on both bugs.

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top pipe3
[files]
design.sv

reg (rs1 shown; rs2 is the same), insn for ADD, and a cover, in concurrent SVA. No assumption: the instruction stream is free.

(* anyconst *) reg [1:0] f_rd;
assert property (@(posedge clk) disable iff (rst) rvfi_valid && rvfi_rs1_addr == f_rd |-> rvfi_rs1_rdata == f_shadow);
assert property (@(posedge clk) disable iff (rst) rvfi_valid && rvfi_op == ADD |-> rvfi_rd_wdata == rvfi_rs1_rdata + rvfi_rs2_rdata);
cover property (@(posedge clk) disable iff (rst) rvfi_valid [*3]);

As the engine runs it.

  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  (* anyconst *) reg [1:0] f_rd;   // the tracked register: the solver picks it
  reg [7:0] f_shadow = 0;            // its value as the retired instructions wrote it (registers reset to 0)
  always @(posedge clk)
    if (rst) f_shadow <= 0;
    else if (rvfi_valid && rvfi_rd_addr == f_rd) f_shadow <= rvfi_rd_wdata;
  always @(posedge clk) if (!rst && rvfi_valid) begin
    if (rvfi_rs1_addr == f_rd) assert(rvfi_rs1_rdata == f_shadow);                    // reg: read what was written
    if (rvfi_rs2_addr == f_rd && rvfi_op != 2'd3) assert(rvfi_rs2_rdata == f_shadow);
    assert(rvfi_rd_wdata == (rvfi_op == 2'd0 ? rvfi_rs1_rdata + rvfi_rs2_rdata : rvfi_op == 2'd1 ? rvfi_rs1_rdata - rvfi_rs2_rdata
         : rvfi_op == 2'd2 ? rvfi_rs1_rdata & rvfi_rs2_rdata : rvfi_rs1_rdata + rvfi_imm));   // insn: the ISA result
  end
  // helpers for k-induction: the register file and every operand in flight agree with the shadow
  wire [7:0] f_now = rf[f_rd];                      // includes the write now on the retirement port
  wire [7:0] f_wb_alu = wb_op == 2'd0 ? wb_a + wb_b : wb_op == 2'd1 ? wb_a - wb_b : wb_op == 2'd2 ? wb_a & wb_b : wb_a + wb_imm;
  always @(posedge clk) if (!rst) begin
    assert(f_now == (rvfi_valid && rvfi_rd_addr == f_rd ? rvfi_rd_wdata : f_shadow));
    if (wb_v) assert(wb_res == f_wb_alu);
    if (wb_v && wb_rs1 == f_rd) assert(wb_a == f_now);
    if (wb_v && wb_rs2 == f_rd && wb_op != 2'd3) assert(wb_b == f_now);
    if (ex_v && ex_rs1 == f_rd) assert(ex_a == (wb_v && wb_rd == f_rd ? wb_res : f_now));
    if (ex_v && ex_rs2 == f_rd && ex_op != 2'd3) assert(ex_b == (wb_v && wb_rd == f_rd ? wb_res : f_now));
  end
  reg [1:0] f_since = 3;   // retirements since the last write to f_rd, saturating
  reg [1:0] f_run = 0;     // consecutive retirements, saturating
  always @(posedge clk) begin
    f_since <= rst ? 2'd3 : rvfi_valid && rvfi_rd_addr == f_rd ? 2'd0 : rvfi_valid && f_since != 2'd3 ? f_since + 2'd1 : f_since;
    f_run <= rst || !rvfi_valid ? 2'd0 : f_run != 2'd3 ? f_run + 2'd1 : f_run;
  end
  always @(posedge clk) if (!rst) begin
    c_dep: cover(rvfi_valid && rvfi_rs1_addr == f_rd && f_since == 2'd1);   // reads f_rd right after the write
    c_three: cover(rvfi_valid && f_run == 2'd2);                           // three retirements in a row
  end

Covers
A read of f_rd right after a write to it, and three retirements in a row, both at step 7.
The bug
Run as loaded: FAIL at reported step 7. Find the two writes and the read.
Fix and prove
Swap the bypass priority, then prove reg with the helpers at k = 2 and insn at k = 3.
Blind spots
Run insn on BUG_FWD_PRIO and on BUG_ALU. Which one passes, and why?

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 pipe3(input clk, rst, valid, input [1:0] op, rd, rs1, rs2, input [7:0] imm,
  output reg rvfi_valid = 0, output reg [1:0] rvfi_op = 0, output reg [1:0] rvfi_rd_addr = 0,
  output reg [1:0] rvfi_rs1_addr = 0, output reg [1:0] rvfi_rs2_addr = 0, output reg [7:0] rvfi_rs1_rdata = 0,
  output reg [7:0] rvfi_rs2_rdata = 0, output reg [7:0] rvfi_rd_wdata = 0, output reg [7:0] rvfi_imm = 0);
  reg [7:0] rf [0:3];
  // execute stage: the instruction and the operand values it was issued with
  reg ex_v = 0; reg [1:0] ex_op = 0, ex_rd = 0, ex_rs1 = 0, ex_rs2 = 0; reg [7:0] ex_a = 0, ex_b = 0, ex_imm = 0;
  // writeback stage: the result
  reg wb_v = 0; reg [1:0] wb_op = 0, wb_rd = 0, wb_rs1 = 0, wb_rs2 = 0; reg [7:0] wb_a = 0, wb_b = 0, wb_imm = 0, wb_res = 0;
  wire [7:0] ex_res = ex_op == 2'd0 ? ex_a + ex_b
                    : ex_op == 2'd1 ? ex_a - ex_b
                    : ex_op == 2'd2 ? ex_a & ex_b : ex_a + ex_imm;
  wire [7:0] opa = wb_v && wb_rd == rs1 ? wb_res : ex_v && ex_rd == rs1 ? ex_res : rf[rs1];   // bug: older result first
  wire [7:0] opb = wb_v && wb_rd == rs2 ? wb_res : ex_v && ex_rd == rs2 ? ex_res : rf[rs2];
  always @(posedge clk) begin
    if (rst) begin ex_v <= 0; wb_v <= 0; rvfi_valid <= 0; rf[0] <= 0; rf[1] <= 0; rf[2] <= 0; rf[3] <= 0; end
    else begin
      ex_v <= valid; ex_op <= op; ex_rd <= rd; ex_rs1 <= rs1; ex_rs2 <= rs2; ex_a <= opa; ex_b <= opb; ex_imm <= imm;
      wb_v <= ex_v; wb_op <= ex_op; wb_rd <= ex_rd; wb_rs1 <= ex_rs1; wb_rs2 <= ex_rs2; wb_a <= ex_a; wb_b <= ex_b; wb_imm <= ex_imm; wb_res <= ex_res;
      if (wb_v) rf[wb_rd] <= wb_res;
      rvfi_valid <= wb_v; rvfi_op <= wb_op; rvfi_rd_addr <= wb_rd; rvfi_rs1_addr <= wb_rs1; rvfi_rs2_addr <= wb_rs2;
      rvfi_rs1_rdata <= wb_a; rvfi_rs2_rdata <= wb_b; rvfi_rd_wdata <= wb_res; rvfi_imm <= wb_imm;
    end
  end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  (* anyconst *) reg [1:0] f_rd;   // the tracked register: the solver picks it
  reg [7:0] f_shadow = 0;            // its value as the retired instructions wrote it (registers reset to 0)
  always @(posedge clk)
    if (rst) f_shadow <= 0;
    else if (rvfi_valid && rvfi_rd_addr == f_rd) f_shadow <= rvfi_rd_wdata;
  always @(posedge clk) if (!rst && rvfi_valid) begin
    if (rvfi_rs1_addr == f_rd) assert(rvfi_rs1_rdata == f_shadow);                    // reg: read what was written
    if (rvfi_rs2_addr == f_rd && rvfi_op != 2'd3) assert(rvfi_rs2_rdata == f_shadow);
  end
`endif
endmodule

Check Yourself

Predict the outputpipe3 with BUG_FWD_PRIO, mode bmc, default depth 20, smtbmc yices, reset assumed in step 0, only the insn check. The verdict is:

module pipe3(input clk, rst, valid, input [1:0] op, rd, rs1, rs2, input [7:0] imm,
  output reg rvfi_valid = 0, output reg [1:0] rvfi_op = 0, output reg [1:0] rvfi_rd_addr = 0,
  output reg [1:0] rvfi_rs1_addr = 0, output reg [1:0] rvfi_rs2_addr = 0, output reg [7:0] rvfi_rs1_rdata = 0,
  output reg [7:0] rvfi_rs2_rdata = 0, output reg [7:0] rvfi_rd_wdata = 0, output reg [7:0] rvfi_imm = 0);
  reg [7:0] rf [0:3];
  // execute stage: the instruction and the operand values it was issued with
  reg ex_v = 0; reg [1:0] ex_op = 0, ex_rd = 0, ex_rs1 = 0, ex_rs2 = 0; reg [7:0] ex_a = 0, ex_b = 0, ex_imm = 0;
  // writeback stage: the result
  reg wb_v = 0; reg [1:0] wb_op = 0, wb_rd = 0, wb_rs1 = 0, wb_rs2 = 0; reg [7:0] wb_a = 0, wb_b = 0, wb_imm = 0, wb_res = 0;
  wire [7:0] ex_res = ex_op == 2'd0 ? ex_a + ex_b
                    : ex_op == 2'd1 ? ex_a - ex_b
                    : ex_op == 2'd2 ? ex_a & ex_b : ex_a + ex_imm;
  wire [7:0] opa = wb_v && wb_rd == rs1 ? wb_res : ex_v && ex_rd == rs1 ? ex_res : rf[rs1];   // bug: older result first
  wire [7:0] opb = wb_v && wb_rd == rs2 ? wb_res : ex_v && ex_rd == rs2 ? ex_res : rf[rs2];
  always @(posedge clk) begin
    if (rst) begin ex_v <= 0; wb_v <= 0; rvfi_valid <= 0; rf[0] <= 0; rf[1] <= 0; rf[2] <= 0; rf[3] <= 0; end
    else begin
      ex_v <= valid; ex_op <= op; ex_rd <= rd; ex_rs1 <= rs1; ex_rs2 <= rs2; ex_a <= opa; ex_b <= opb; ex_imm <= imm;
      wb_v <= ex_v; wb_op <= ex_op; wb_rd <= ex_rd; wb_rs1 <= ex_rs1; wb_rs2 <= ex_rs2; wb_a <= ex_a; wb_b <= ex_b; wb_imm <= ex_imm; wb_res <= ex_res;
      if (wb_v) rf[wb_rd] <= wb_res;
      rvfi_valid <= wb_v; rvfi_op <= wb_op; rvfi_rd_addr <= wb_rd; rvfi_rs1_addr <= wb_rs1; rvfi_rs2_addr <= wb_rs2;
      rvfi_rs1_rdata <= wb_a; rvfi_rs2_rdata <= wb_b; rvfi_rd_wdata <= wb_res; rvfi_imm <= wb_imm;
    end
  end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  (* anyconst *) reg [1:0] f_rd;   // the tracked register: the solver picks it
  reg [7:0] f_shadow = 0;            // its value as the retired instructions wrote it (registers reset to 0)
  always @(posedge clk)
    if (rst) f_shadow <= 0;
    else if (rvfi_valid && rvfi_rd_addr == f_rd) f_shadow <= rvfi_rd_wdata;
  always @(posedge clk) if (!rst && rvfi_valid) begin
    assert(rvfi_rd_wdata == (rvfi_op == 2'd0 ? rvfi_rs1_rdata + rvfi_rs2_rdata : rvfi_op == 2'd1 ? rvfi_rs1_rdata - rvfi_rs2_rdata
         : rvfi_op == 2'd2 ? rvfi_rs1_rdata & rvfi_rs2_rdata : rvfi_rs1_rdata + rvfi_imm));   // insn: the ISA result
  end
`endif
endmodule

ConceptWhich retirement-port check is the wrong one to write?

assert(ex_res == ex_a + ex_b); on pipeline internalsinsn: the retired result is the ISA function of the reported operandsreg: a retired read of f_rd used the shadow valuea cover on three retirements in a row

ConceptWhy one symbolic register index instead of a shadow register file?

A shadow register file would be a second design to verify.One free index covers every register with one shadow value.The tool cannot model arrays such as a register file.Four registers are too many to shadow in one bench.

Read the waveformIn the BUG_FWD_PRIO trace, in which steps do the two writes to f_rd retire, and which bypass did the third instruction take?

Two writes to the tracked register, then a read of the older one

Measured with smtbmc yices: FAIL at reported step 7, 0.6 s. Ops: 0 ADD, 1 SUB, 2 AND, 3 ADDI.

Step 5 only; the execute bypassSteps 4 and 5; the execute bypassSteps 4 and 5; the writeback bypassSteps 4 and 5; the register file

Remember

Write pipeline checks against a retirement port, never against internals.
reg: one free register index and a shadow catch every forwarding bug.
insn: the result is the ISA function of the reported operands; reg and insn are blind to each other's bugs.
Helpers that tie the register file and the operands in flight to the shadow make reg inductive at k = 2.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.