The industry section proved the DMA's register rules with a formal tool and found, in under a second, the trace that broke an old claim: DONE and ERR can be set together. Your UVM bench binds a checker with rules of its own. The design team now wants one rules file that both benches read, so that a rule edited in one place is the same rule everywhere. What has to differ between the two benches, which rules must not travel, and what do you do with a counterexample once you have it?

The idea: one rule text, a thin layer that differs

A property does not know which engine evaluates it. What differs between the benches is everything around the property: who drives the inputs, how failures are reported, and how knobs are set. In simulation, the UVM drivers drive the inputs and an assert on an input checks that the driver behaves. In formal, nothing drives the inputs; the tool may choose any value on any cycle unless an assume forbids it. So the same input-side rule is an assertion in one bench and an assumption in the other. Think of a contract read by two parties: the words are identical, but one party is bound by a clause the other relies on.

That gives the file three kinds of rule. Output-side rules (the DUT's promises) are asserted in both benches. Input-side protocol rules (what any legal master does) are assumed in formal and asserted in simulation. Usage rules (what this bench's tests normally do) stay simulation-only, because assuming them in formal would remove behaviour the DUT must handle.

The picture: one file, two benches

Build it: the switch lives in macros, not in copies

The worst way to share rules is to keep two copies, one per bench; within a month they differ. The usual pattern is one file with macros for the parts that change. FORMAL is defined only in the formal tool's file list:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

// snippet: one rule file, two benches
`ifdef FORMAL
  `define CHK_FAIL(ID, MSG) begin end             // formal tools ignore action blocks anyway
  `define CHK_INPUT(NAME, PROP) NAME: assume property (PROP);
`else
  `define CHK_FAIL(ID, MSG) `uvm_error(ID, MSG)
  `define CHK_INPUT(NAME, PROP) NAME: assert property (PROP) else `uvm_error("CHK_INPUT", "input rule broken");
`endif

module dma_rules_chk #(parameter bit SHORT_PKT_EN = 1) ( /* ports as before */ );
`ifndef FORMAL
  import uvm_pkg::*;
  bit short_pkt_en = SHORT_PKT_EN;               // simulation: overridable from config_db
  initial begin
    @(posedge rst_n);
    void'(uvm_config_db#(bit)::get(null, inst_path(), "short_pkt_en", short_pkt_en));
  end
`else
  localparam bit short_pkt_en = SHORT_PKT_EN;    // formal: a constant per run
`endif

  // Output-side rule: asserted in both benches.
  a_done_not_busy: assert property (@(posedge clk) disable iff (!rst_n) !(done && busy))
    else `CHK_FAIL("DMA_DONE_BUSY", $sformatf("%m: DONE and BUSY both set"))

  // Input-side rule: assume in formal, assert in simulation (checks the bench's driver).
  `CHK_INPUT(m_apb_hold, @(posedge clk) disable iff (!rst_n) psel && penable && !pready |=> psel && penable)

  // Usage rule: asserted in simulation only. NOT an assumption in formal (see below).
  a_full_packet: assert property (@(posedge clk) disable iff (!rst_n || !short_pkt_en)
    take && s_tlast |-> last_word)
    else `CHK_FAIL("DMA_SHORT_PKT", "input TLAST before word LEN")
endmodule

• `CHK_INPUT` is the only place where assume and assert differ, and the property text is written once. The same pattern carries the APB checker in Assertion VIP and bind; its APB_FAIL macro is the same idea as CHK_FAIL.

• The UVM glue is guarded by ifndef FORMAL. Formal front ends do not read uvm_pkg, and a config_db lookup means nothing to a solver. The knob becomes a parameter, so a formal run can also prove the rules with the knob off.

• `a_full_packet` is not an assumption. Assuming "packets are always LEN long" would make every proof about ERR vacuous, because the solver could never reach the error path. That is the over-constraint failure the industry lesson demonstrates with an unreached c_err cover. A rule that tests break on purpose is a usage rule, never an environment rule.

What a proof changes in the UVM plan

When a rule is fully proved, the plan row for it closes by proof, and directed tests whose only purpose was to poke that rule can go. The assertion itself stays bound in simulation. It costs little, and it checks something the proof cannot: that the RTL in the integrated bench, with real drivers and real configuration, is the RTL that was proved. A bounded proof closes nothing on its own; the formal sign-off discussion covers how a depth is justified with covers.

Watch it run: a counterexample comes back as a test (scratch run)

The formal run's counterexample for "never DONE and ERR together" was: write LEN = 2, write GO, send one word with TLAST, write GO again without clearing ERR, send two words. A counterexample is a waveform with no testbench attached; to keep it, turn it into a directed UVM test, so the scenario runs in every regression with the scoreboard and coverage watching. The replay below is that trace, step for step:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

// snippet: the counterexample replayed as a directed UVM test (scratch bench)
task run_phase(uvm_phase phase);
  bit [31:0] status;
  phase.raise_objection(this);
  reg_write(LEN, 2);
  reg_write(CTRL, 32'h1);                  // GO, no interrupt
  send(1);                                 // one word with TLAST: ERR
  #50ns;
  reg_read(STATUS, status);
  `uvm_info("CEX", $sformatf("after the short packet: STATUS=%08h", status), UVM_LOW)
  reg_write(CTRL, 32'h1);                  // GO again, ERR not cleared
  send(2);
  #50ns;
  reg_read(STATUS, status);
  `uvm_info("CEX", $sformatf("after the full packet:  STATUS=%08h", status), UVM_LOW)
  if (status[2:1] != 2'b11) `uvm_error("CEX", "trace did not reproduce DONE and ERR together")
  #100ns;
  phase.drop_objection(this);
endtask

+UVM_TESTNAME=sva_cex_replay_test
UVM_INFO sva_tb.sv(30) @ 35000: reporter [DMA_CHK] top.dut.u_rules: short_pkt_en=0
UVM_INFO sva_tb.sv(192) @ 225000: uvm_test_top [CEX] after the short packet: STATUS=00000004
UVM_INFO sva_tb.sv(197) @ 425000: uvm_test_top [CEX] after the full packet:  STATUS=00000006
UVM_INFO dma_tb.sv(411) @ 525000: uvm_test_top.env.sb [SB] 3 words matched, 0 mismatched
TEST VERDICT: PASS (UVM_ERROR=0, UVM_FATAL=0)

• STATUS = 4, then 6: ERR alone after the short packet, then DONE and ERR together after the second job. The simulation reproduces the formal trace exactly, and the scoreboard checked all 3 words that moved.

• The replay switched off `a_full_packet`. The first attempt failed with DMA_SHORT_PKT, because the formal environment allowed short packets and the simulation's usage rule does not. A counterexample from a free-input environment often breaks a usage rule; switch off that rule for the replay, by name, and say why in the test.

• The trace is now a permanent regression test and a covered plan row (status=both), where before it existed only in one engineer's formal run directory.

What breaks: an assumption that nothing checks

Formal results are only as good as the assumptions. An assumption written only in the formal harness and never asserted anywhere can drift from reality without anyone noticing. A common case is an assumption that a ready signal is never held low for more than four cycles, copied from an old interface; the real interconnect holds it for sixteen. The proofs pass, and the deadlock they would have found is outside the space the solver was allowed to search. The defence is the CHK_INPUT macro: every assumption is the same text as a simulation assertion, so the first UVM test that drives a sixteen-cycle stall fails with CHK_INPUT, and someone has to decide whether the assumption or the interconnect is wrong. An assumption with no simulation twin should fail review.

Next: whichever engine finds a failure, someone has to read it. Reporting Assertion Failures through uvm_report gets assertion failures into the verdict without drowning the log.

Related topics

• Up: UVM with SVA and Formal

• Formal Alongside Simulation

• Over-constraint scenario (Formal course)

• Seeds and replay