Encoding Protocol Legality

From spec table to constraint block

Protocol specs deliver legality as tables and bullet rules: legal opcode encodings, alignment requirements per transfer size, permitted burst/size combinations, reserved values. The verification task is mechanical translation — every table row becomes a constraint expression — but the architecture rules from the layering lesson apply with force here: legality lives in one constraint block, in one class, traceable line-by-line to the spec . When the spec revs, you diff one block. When a test needs illegal stimulus (error injection), it disables or partitions exactly this block, knowingly.

SPEC TABLE -> CONSTRAINT TRANSLATION

  Spec section 4.2 (bus transfer rules)        valid_c line
  ------------------------------------------------------------------
  T1: SIZE field: 0=byte 1=half 2=word,   ->  size != 2'd3;
      encoding 3 RESERVED
  T2: address aligned to transfer size    ->  addr % (1<<size) == 0;
  T3: WRAP bursts: length 2,4,8,16 only   ->  (btype == WRAP) ->
                                                 len_p1 inside {2,4,8,16};
  T4: FIXED bursts: length <= 16          ->  (btype == FIXED) ->
                                                 len_p1 <= 16;
  T5: burst must not cross 4KB boundary   ->  addr[11:0] + bytes <= 4096;
  T6: opcodes 0x6,0x7 RESERVED            ->  !(opc inside {3'h6,3'h7});
  T7: exclusive access: max 16 bytes,     ->  excl -> (bytes <= 16 &&
      aligned to total size                        addr % bytes == 0);

  one row : one line : one comment citing the spec section
  -> review = diff the table against the block

Worked example: AXI-lite-style transaction

typedef enum bit [1:0] { FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2 } btype_e;

class axil_txn;
  rand bit [31:0] addr;
  rand bit [2:0]  size;        // bytes = 2**size; spec: <= word
  rand bit [4:0]  len_p1;      // beats, 1..16 (len+1 form)
  rand btype_e    btype;
  rand bit [2:0]  opc;
  rand bit        excl;

  // Legality - each line cites its spec rule (T-numbers above)
  constraint valid_c {
    size <= 3'd2;                                       // T1
    addr % (1 << size) == 0;                            // T2
    len_p1 inside {[1:16]};                             // T4 (+floor)
    (btype == WRAP)  -> len_p1 inside {2, 4, 8, 16};    // T3
    (btype == WRAP)  -> addr % ((len_p1) << size) == 0; // T7-style wrap align
    addr[11:0] + (len_p1 << size) <= 13'd4096;          // T5
    !(opc inside {3'h6, 3'h7});                         // T6
    excl -> ((len_p1 << size) <= 16);                   // T7a
    excl -> (addr % (len_p1 << size) == 0);             // T7b
  }
endclass

module check;
  initial begin
    axil_txn t = new();
    repeat (10000) begin
      assert(t.randomize());
      // belt-and-braces: re-verify a sample of rules procedurally
      if (t.btype == WRAP && !(t.len_p1 inside {2,4,8,16}))
        $fatal(1, "T3 violated: wrap len %0d", t.len_p1);
      if (t.addr % (1 << t.size) != 0)
        $fatal(1, "T2 violated: addr %h size %0d", t.addr, t.size);
    end
    $display("10k legal transactions generated");
  end
endmodule

Translation craft notes. The len+1 representation (len_p1) avoids the classic off-by-one where the wire format encodes beats-1 — convert at the driver, constrain in natural units. Power-of-two byte counts are expressed with shifts, not multiplication, keeping expressions integer-exact. Watch widths on arithmetic rows: addr[11:0] + (len_p1 << size) must not overflow its evaluation width or T5 silently passes illegal crossings — the 13-bit literal comparison forces adequate width. The procedural re-check loop is bring-up scaffolding: it catches translation typos (a wrong relational direction passes the solver happily) in the first ten seconds of use.

Legality is not coverage: keep the goals out

A recurring confusion: because corner values matter for coverage, engineers add “make corners likely” terms to the legality block — a dist pushing addr toward page boundaries, weights favoring max-length wraps. Now legality and stimulus-shaping are fused: error injection that disables valid_c also loses the corner bias, every test inherits the skew whether wanted or not, and the spec-diff property of the block is destroyed. The separation discipline:

• valid_c contains pure legality — every solution it admits is spec-legal, every spec-legal value is admitted. No dist, no soft, no preferences.

• Coverage pressure (corner biasing) is typicality/intent: dist weights in a separate soft block, a corner_policy object, or knob weights — all escapable, all composable.

• Coverage measurement is a covergroup on the monitor side — never a constraint at all. Constraints shape what you try; covergroups record what happened.

• Test for the split: 'could I hand valid_c alone to a colleague as a spec summary?' If a line needs justification beyond a spec citation, it is in the wrong block.

// Corner pressure as a SEPARATE, escapable layer - not in valid_c
class axil_corner_txn extends axil_txn;
  constraint corner_bias_c {
    soft addr[11:0] dist { [12'hFF0:12'hFFF] :/ 3,    // near 4KB edge
                           [12'h000:12'h00F] :/ 3,    // page start
                           [12'h010:12'hFEF] :/ 4 };  // body
    soft len_p1 dist { 16 := 3, [1:15] :/ 7 };        // favor max burst
  }
endclass
// valid_c untouched: still pure spec. Tests choose the corner
// subclass (or a policy) when they want the pressure.

Interview angle

Interviewers hand you a mini spec table — “WRAP bursts must be length 2/4/8/16 and aligned to total size; encoding 3 of SIZE is reserved” — and watch you translate. Score points by: writing implications for conditional rows (btype == WRAP -> ...), excluding reserved encodings with negated inside, raising the width/overflow hazard on the 4KB-boundary arithmetic unprompted, and keeping every line annotated with its spec rule ID. The discriminating follow-up is “would you also add a dist here to hit corners?” — the correct answer is no: legality admits exactly the spec, corner pressure goes in a separate soft/policy layer, and measurement is the covergroup's job. That three-way separation (legal / likely / measured) is the senior signal.

Key takeaways

• One spec row, one constraint line, one citation comment — the block is diffable against the spec.

• Conditional table rows become implications; reserved encodings become negated inside sets.

• Constrain in natural units (beats, bytes) and convert encodings (len-1) at the driver boundary.

• Watch arithmetic widths in boundary rules — silent overflow legalizes illegal crossings.

• Legal / likely / measured are three layers: valid_c, soft-dist or policy bias, monitor covergroup.

Common pitfalls

• dist or soft terms inside valid_c — legality fused with preference, spec-diff property destroyed.

• Constraining the wire encoding (len-1) directly — off-by-one in every burst rule.

• 4KB-boundary sum evaluated in too few bits — overflow wraps and the rule never fires.

• Translating 'reserved' as ignore-in-coverage instead of exclude-in-constraints — reserved values get driven.

• No procedural re-check at bring-up — a flipped relational in one row generates plausible illegal stimulus for weeks.