Update protocol for BNW AXI-Stream adapter bug (S3)

[ngernest]

This PR rewrites the protocol for the Brave New World AXI-Stream adapter bug (axis-adapter-s3) so that the BI fails on the buggy waveform and succeeds on the updated waveform using a single new .prot file (s3.prot). (I've deleted the old .prot files, since they were missing some pins)

The DUT is an adapter which converts 64-bit input data word into 8-bit output data chunks, emitted over multiple clock cycles. I drew this diagram below to figure out the directions of the pins. The DUT accepts 64-bit data from the environment as input, and emits 8-bit data as output. The tkeep signal is a bit-mask indicating which bytes of the corresponding tdata signal are meaningful, and the last signal is 1 if this is the last word of a packet.

In the new .prot file, besides the usual idle / reset transactions, we also have:

• accept_word: the DUT accepts a 64-bit input data word from the environment
• emit_byte: the DUT emits 8-bit data as output (tlast = 0)
• emit_last_byte: Like emit_byte, but last = 1 (last byte of a packet)

On the fixed waveform, the BI infers a trace successfully:

// trace 0
trace {
    reset();  // [time: 0ns -> 25ns]
    accept_word(12379739850550389709, 31, 1);  // [time: 75ns -> 100ns]
    emit_byte(205);  // [time: 100ns -> 125ns]
    emit_byte(171);  // [time: 125ns -> 150ns]
    emit_byte(205);  // [time: 150ns -> 175ns]
    emit_byte(171);  // [time: 175ns -> 200ns]
    emit_last_byte(205);  // [time: 200ns -> 200ns]
}

And on the buggy waveform, the BI reports an error for all 5 protocols:

// trace 0
trace {
    reset();  // [time: 0ns -> 25ns]
    accept_word(12379739850550389709, 31, 1);  // [time: 75ns -> 100ns]
    emit_byte(205);  // [time: 100ns -> 125ns]
    emit_byte(171);  // [time: 125ns -> 150ns]
    emit_byte(205);  // [time: 150ns -> 175ns]
    emit_byte(171);  // [time: 175ns -> 200ns]
    emit_byte(205);  // [time: 200ns -> 225ns]
}
error: [emit_last_byte@9] executing step 0 of the transaction: 0 != 1
    ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:108:5
    │
108 │     assert_eq(DUT.output_axis_tkeep, 1'b1);
    │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [emit_last_byte@9] executing step 0 of the transaction: 0 != 1


// trace 1
trace {
    reset();  // [time: 0ns -> 25ns]
    accept_word(12379739850550389709, 31, 1);  // [time: 75ns -> 100ns]
    emit_byte(205);  // [time: 100ns -> 125ns]
    emit_byte(171);  // [time: 125ns -> 150ns]
    emit_byte(205);  // [time: 150ns -> 175ns]
    emit_byte(171);  // [time: 175ns -> 200ns]
    emit_byte(205);  // [time: 200ns -> 225ns]
}
error: [emit_byte@9] executing step 0 of the transaction: 0 != 1
   ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:94:5
   │
94 │     assert_eq(DUT.output_axis_tkeep, 1'b1);
   │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [emit_byte@9] executing step 0 of the transaction: 0 != 1


// trace 2
trace {
    reset();  // [time: 0ns -> 25ns]
    accept_word(12379739850550389709, 31, 1);  // [time: 75ns -> 100ns]
    emit_byte(205);  // [time: 100ns -> 125ns]
    emit_byte(171);  // [time: 125ns -> 150ns]
    emit_byte(205);  // [time: 150ns -> 175ns]
    emit_byte(171);  // [time: 175ns -> 200ns]
    emit_byte(205);  // [time: 200ns -> 225ns]
}
error: [accept_word@9] executing step 0 of the transaction: 0 != 1
   ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:76:5
   │
76 │     DUT.input_axis_tvalid := 1'b1;
   │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [accept_word@9] executing step 0 of the transaction: 0 != 1


// trace 3
trace {
    reset();  // [time: 0ns -> 25ns]
    accept_word(12379739850550389709, 31, 1);  // [time: 75ns -> 100ns]
    emit_byte(205);  // [time: 100ns -> 125ns]
    emit_byte(171);  // [time: 125ns -> 150ns]
    emit_byte(205);  // [time: 150ns -> 175ns]
    emit_byte(171);  // [time: 175ns -> 200ns]
    emit_byte(205);  // [time: 200ns -> 225ns]
}
error: [idle@9] executing step 0 of the transaction: 1 != 0
   ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:63:5
   │
63 │     assert_eq(DUT.output_axis_tvalid, 1'b0);
   │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [idle@9] executing step 0 of the transaction: 1 != 0


// trace 4
trace {
    reset();  // [time: 0ns -> 25ns]
    accept_word(12379739850550389709, 31, 1);  // [time: 75ns -> 100ns]
    emit_byte(205);  // [time: 100ns -> 125ns]
    emit_byte(171);  // [time: 125ns -> 150ns]
    emit_byte(205);  // [time: 150ns -> 175ns]
    emit_byte(171);  // [time: 175ns -> 200ns]
    emit_byte(205);  // [time: 200ns -> 225ns]
}
error: [reset@9] executing step 0 of the transaction: 1 != 0
   ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:51:5
   │
51 │     assert_eq(DUT.output_axis_tvalid, 1'b0);
   │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [reset@9] executing step 0 of the transaction: 1 != 0

[ngernest]

Per our discussion today, the protocol has been rewritten so that it now branches on the value of tkeep for each output byte (see s3.prot). BI now succeeds on fixed waveform:

// trace 0
trace {
    reset();  // [time: 0ns -> 25ns]
    idle();  // [time: 25ns -> 50ns]
    idle();  // [time: 50ns -> 75ns]
    split_word(0xabcdabcdabcdabcd, 0x1f, 0x1);  // [time: 75ns -> 200ns]
}

and fails on the buggy waveform:

// trace 0
trace {
    reset();  // [time: 0ns -> 25ns]
    idle();  // [time: 25ns -> 50ns]
    idle();  // [time: 50ns -> 75ns]
}
error: [split_word@3] executing step 5 of the transaction: 0 != 1
    ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:237:45
    │
237 │                                             assert_eq(keep[5], 1'b1);
    │                                             ^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1

We can also run the interpreter and drive the fixed DUT (s3_fixed.v) with this trace:

trace {
  reset();
  idle();
  // Same transaction with the same input data, as in `s3_fixed.fst` (waveform from Brave New World artifact)
  split_word(0xabcdabcdabcdabcd, 0x1f, 0b1);
}

[ngernest]

When the DUT is emitting output bytes, for the i-th byte (where 0 <= i < 7), there are 3 cases in the split_word protocol:

• If tkeep = 1 and tlast = 1, i.e. the current byte is meaningful and we are at the end of a packet, then the (fixed) DUT stops emitting bytes from this further onwards, and sets tkeep[i + 1] = 0 (the next byte is no longer meaningful since we're done). In the protocol, we do the equivalent of assert_eq(tkeep[i + 1], 1'b0) (but with concrete values of I).
• If tkeep = 1 and tlast = 0, i.e. the current byte is meaningful but we're not at the end of a packet, then the DUT continues to emit bytes and sets tkeep[i + 1] = 1 (the next byte is still meaningful, we're not done yet). In the protocol, we do the equivalent of assert_eq(tkeep[i + 1], 1'b1) (but with concrete values of i).
• If tkeep = 0, i.e. the current byte is not meaningful, the DUT stops emitting bytes from this point onwards. In the protocol, in this case, we do assert_eq(output_axis_tlast, is_end_of_packet), i.e. the is_end_of_packet argument is the value of the tlast signal.

Note: when i = 7, we are at the last byte (since the input is 64-bits, we can emit at most 8 bytes, e.g. when tkeep = 11111111). In this case, we just do assert_eq(output_axis_tlast, is_end_of_packet).

[ngernest]

Pushed an alternate version of the protocol (s3_new.prot) that branches on the i-th bit of the input parameter keep[i]