Interview Question · Code Writing

Binding a Checker to an RTL Block

L1 JuniorL2 Mid-Levelsvabindcheckers

The interviewer asks

The RTL owner will not let you edit their counter module. Write the code that attaches an overflow assertion to every instance of it. Can your checker see the internal count_q?

systemverilog

module counter(input logic clk, rst, inc);
  logic [1:0] count_q;      // internal, not a port
  always @(posedge clk)
    if (rst) count_q <= 0; else if (inc) count_q <= count_q + 1;
endmodule

Reveal the Model Answer

Write the assertion in its own module, then use bind counter counter_props u_props (.clk, .rst, .inc, .count_q);. The bind puts an instance of the checker inside every counter, without touching the RTL file. The port connections are resolved inside the target, so the checker can read internal signals such as count_q. Each failure message then names the instance where it happened.

One Bind, Two Rule Instances, Three ReportsA bind adds a checker instance inside every instance of the target module. Arrows show what the bind creates, which signals each instance reads, and where its failure messages go.

Read the diagram as text

rd_rules: hold, stall, last
port0 signals: v0, r0, l0, d0
bind rd_port: rd_rules #(.MAX_STALL(2)) rules (.*)
port1 signals: v1, r1, l1, d1
tb.port0.rules: MAX_STALL = 2
tb.port1.rules: MAX_STALL = 2
Fail messages: %m gives the full path

rd_rules → bind rd_port: named in
bind rd_port → tb.port0.rules: creates
bind rd_port → tb.port1.rules: creates
port0 signals → tb.port0.rules: .* by name
port1 signals → tb.port1.rules: .* by name
tb.port0.rules → Fail messages: fails
tb.port1.rules → Fail messages: fails

The rules are written once. The instance path in each message says which port broke which rule.

Self-Check

Tick each key point you covered in your answer.

Key point 1 Write the assertion in its own module, then use bind counter counter_props u_props (.clk, .rst, .inc, .count_q);. Key point 2 The bind puts an instance of the checker inside every counter, without touching the RTL file. Key point 3 The port connections are resolved inside the target, so the checker can read internal signals such as count_q. Key point 4 Each failure message then names the instance where it happened.

What Interviewers Listen For (Junior)

A good junior answer writes the checker module and the bind line. It knows that a bind to a module name reaches every instance.

Cross-Questions

Where the interviewer goes next. Open a node to practise that follow-up.

WhyProve ItBreak ItCompare

Binding a Checker to an RTL Block
WhyWhy Bind ExistsL1 Junior
Why did the language add bind instead of just letting people write assertions in the RTL?

Reveal the Model Answer

Design and verification are often owned by different people. Bind keeps checkers out of the design files, so adding a check never needs an RTL change or an RTL review. It also lets one checker attach to a block the team cannot edit, such as third-party IP.

Self-Check
Tick each key point you covered in your answer.
Key point 1 Design and verification are often owned by different people. Key point 2 Bind keeps checkers out of the design files, so adding a check never needs an RTL change or an RTL review. Key point 3 It also lets one checker attach to a block the team cannot edit, such as third-party IP.

Half-Truth

"Assertions inside RTL are bad practice."

Designers often write useful assertions in their own code. Bind is for checks that belong to the verification side.
- Lesson A7.1Packaging and Binding
CompareBinding to a Module vs to One InstanceL2 Mid-Level
Compare bind counter ... with bind tb.u1 ....

Reveal the Model Answer

Binding to the module name puts the checker in every instance of counter. Binding to a hierarchical instance path puts it only there. Use the module form for rules that every copy must obey. Use the instance form for a rule that depends on how one copy is used.

bind counter ... bind tb.u1 ...

Reaches Every instance of counter Only the instance at that path
Use it for Rules every copy must obey A rule that depends on how one copy is used

Self-Check
Tick each key point you covered in your answer.
Key point 1 Binding to the module name puts the checker in every instance of counter. Key point 2 Binding to a hierarchical instance path puts it only there. Key point 3 Use the module form for rules that every copy must obey. Key point 4 Use the instance form for a rule that depends on how one copy is used.

Misconception

"Binding by module name reaches only the first instance."

It reaches all instances. The twin on the root binds once and gets a checker in both u0 and u1.

Source IEEE 1800-2017 §23.11
- Lesson A7.1Packaging and Binding
Prove ItSolve 6.6.11: A Read-Channel Assertion SuiteSimulator-graded

Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
Open Problem 6.6.11
Break ItA Bind That Connected the Wrong SignalL2 Mid-Level
How can a correct checker, bound to the right module, still check nothing?

Reveal the Model Answer

The bind port list can connect the wrong signal, for example a signal that never goes high. Every attempt then passes vacuously, which means the antecedent never matched and nothing was checked. An antecedent cover per assertion shows it as a cover stuck at zero.

Self-Check
Tick each key point you covered in your answer.
Key point 1 The bind port list can connect the wrong signal, for example a signal that never goes high. Key point 2 Every attempt then passes vacuously, which means the antecedent never matched and nothing was checked. Key point 3 An antecedent cover per assertion shows it as a cover stuck at zero.

Missed Corner

"If the bind compiles, the connections are right."

Any signal of a matching type compiles. Only covers or a review of the port list catch a wrong but legal connection.

Source Lesson A1.3 (implication and vacuous success)
- Lesson A1.3Implication and Vacuous Success
- Lesson A7.1Packaging and Binding
Prove ItA Bug That Escapes Through VacuityL2 Mid-Level
Give a real bug that escapes req |=> ack because the assertion passes vacuously.

Reveal the Model Answer

A typical one is a bind mistake: the assertion's req is tied to a signal that never goes high. Every attempt is then vacuous while the real handshake is broken. Another is a test that never reaches the mode where req is raised. Both show up only as an antecedent cover stuck at zero.
Passes with nothing checked
Every edge starts an attempt, and every attempt passes vacuously because no error response ever occurs.

Self-Check
Tick each key point you covered in your answer.
Key point 1 A typical one is a bind mistake: the assertion's req is tied to a signal that never goes high. Key point 2 Every attempt is then vacuous while the real handshake is broken. Key point 3 Another is a test that never reaches the mode where req is raised. Key point 4 Both show up only as an antecedent cover stuck at zero.

Half-Truth

"Vacuity only happens in badly written properties."

A correct property goes vacuous whenever the stimulus or the wiring never produces the antecedent. It is a test and setup problem as often as a property problem.
- Lesson A1.3Implication and Vacuous Success
- Lesson F3.2Over-Constraint and Vacuity

	`bind counter ...`	`bind tb.u1 ...`
Reaches	Every instance of `counter`	Only the instance at that path
Use it for	Rules every copy must obey	A rule that depends on how one copy is used

What People Get Wrong

Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.

Misconception

"A bound checker can only see the target's ports."

Bind connections are resolved in the target's scope. The twin reads the internal count_q and reports the wrap inside instance u1.

Run It

An overflow checker bound to two counters; only u1 counts past 3.

RUNVerilator · simulator service

Edit the code, then run it

Expected: tb.u1.u_props.a_no_wrap: count_q wrapped from 3 u0 fails=0 u1 fails=1 FAIL: the bound checker read count_q, an internal signal, inside instance u1

module counter(input logic clk, rst, inc);
  logic [1:0] count_q;                       // internal state, not a port
  always @(posedge clk) if (rst) count_q <= 0; else if (inc) count_q <= count_q + 1;
endmodule
// The checker is written separately and bound in: the RTL file is not edited.
module counter_props(input logic clk, rst, inc, input logic [1:0] count_q);
  int fails = 0;
  a_no_wrap: assert property (@(posedge clk) disable iff (rst) !(count_q == 3 && inc))
    else begin fails++; $display("%m: count_q wrapped from 3"); end
endmodule
// The belief: a bound checker can only see the target's ports.
bind counter counter_props u_props (.clk, .rst, .inc, .count_q);
module tb;
  logic clk = 0, rst = 1, inc0 = 0, inc1 = 0;
  always #5 clk = ~clk;
  counter u0 (.clk, .rst, .inc(inc0));
  counter u1 (.clk, .rst, .inc(inc1));
  initial begin
    @(negedge clk) rst = 0;
    repeat (4) @(negedge clk) inc1 = 1;      // only u1 counts past 3
    @(negedge clk) inc1 = 0;
    @(negedge clk);
    $display("u0 fails=%0d u1 fails=%0d", tb.u0.u_props.fails, tb.u1.u_props.fails);
    if (tb.u1.u_props.fails) $display("FAIL: the bound checker read count_q, an internal signal, inside instance u1");
    $finish;
  end
endmodule

Tool as Truth

"Bind is a simulator feature; formal tools need the assertions inside the RTL."

Bind is part of the language, and formal tools read bound checkers the same way.

Source IEEE 1800-2017 §23.11

Wrong Altitude

Proposes asking the RTL owner to add ifdef assertions instead.

That is possible, but it is the slower route this question rules out. Bind exists so checkers can be added without editing the design.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.

Binding a Checker to an RTL Block

Your Answer

Self-Check

What Interviewers Listen For (Junior)

What Interviewers Listen For (Mid-Level)

What Interviewers Listen For (Senior)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What People Get Wrong

Learn It, Then Prove It

The Question

Your Answer

Self-Check

What Interviewers Listen For (Junior)

What Interviewers Listen For (Mid-Level)

What Interviewers Listen For (Senior)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What People Get Wrong

Learn It, Then Prove It