(WIP) Use same protocol to both drive DUT + infer transactions for BNW axi-lite-s1 bug

[ngernest]

(Work in progress, not ready for review yet) (The Edit: notes below describe my current progress)

This PR updates s1_buggy.prot / s1_fixed.prot (which corresponds to a Brave New World bug axi-lite-s1) so that we can both drive the DUT using the AST interpreter and infer transactions using BI using the same `.prot program.

(BI was used and not the monitor, as the monitor has a known bug where it does not properly handle multiple assignments to the same signal within the same cycle -- see issue #214)

The bug is described in this blogpost (see Figure 4):
an AXI-Lite manager issues two write requests, but an acknowledgement is missing for the second request. Here is a waveform showing the bug (taken from the blogpost):

Edit (EoD 7/5, main difficulty with this bug):
There are actually 2 workloads for this BNW example, which surface two different bugs:

• Workload 1: Two consecutive write requests, only first one is acknowledged (mentioned above, Figure 4 in the blogpost)
• Workload 2: Two consecutive read requests, only first one is acknowledged (Figure 5 in the blogpost)
  (The current PR focuses on Workload 1 but it may be simpler to look at Workload 2 since it involves fewer channels -- need to investigate this further)

Changes to protocol file:

1. The current frontend implementation only handles .prot files with one struct (see this line). Previously, the .prot file contained two structs (WriteSubordinate & ReadSubordinate), so to drive the design, we keep only the WriteSubordinate struct since the bug only pertains to write requests.

(Edit: need to experiment with having a .prot file that contains one struct containing all the signals for reads/writes)

2. Added a reset transaction + a reset pin to the WriteSubordinate struct (when driving the design, we first invoke the reset() transaction first to reset all signals before invoking other transactions)

3. Added a call to fork() in the write protocol after the data transfer is complete (this was previously missing). The bug happens when there are two concurrent write transactions, so this call to fork() allows the interpreter to drive the DUT to perform two write transactions in a pipelined manner.

Running interpreter + BI on fixed DUT

Interpreter:
When we run the interpreter with the following transaction trace (s1_fixed.tx) and the fixed DUT (s1_buggy.v), the interpreter succeeds.

trace {
  reset();
  write(4, 42, 0, 4);
  write(8, 7, 0, 0);
}

If we take the waveform produced by the interpreter (s1_fixed_interp.fst) and run BI on it, BI is able to infer the same trace:

$ cargo bi -p s1_fixed.prot --wave s1_fixed_interp.fst --instances dut:WriteSubordinate --show-steps --max-traces 1 
 
// trace 0
trace {
    reset(); [0]
    write(4, 42, 0, 4); [1 .. 12]
    write(8, 7, 0, 0); [7 .. 14]
}

... // Other traces reported are duplicates

To reproduce:

# Run interpreter on fixed DUT, this produces a waveform called s1_0.fst
$ cargo interp --verilog tests/fpga-debugging/axi-lite-s1/s1_fixed.v \
    -p tests/fpga-debugging/axi-lite-s1/s1_fixed.prot \
    -t tests/fpga-debugging/axi-lite-s1/s1_fixed.tx \
    -m xlnxdemo --max-steps 300 --fst s1.fst       
# Run BI on the waveform produced by interpreter
$ cargo bi -p tests/fpga-debugging/axi-lite-s1/s1_fixed.prot \
    --wave s1_0.fst --instances dut:WriteSubordinate --show-steps

Running BI on waveform for buggy DUT

When we run BI on the waveform for the buggy DUT (s1_buggy_workload1.vcd, obtained from the Brave New World artifact), BI reports a protocol violation bug:

$ cargo bi --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot \
    --wave tests/fpga-debugging/axi-lite-s1/s1_buggy_workload1.vcd \
    --instances TOP.testbench.UUT:WriteSubordinate \
    --sample-posedge TOP.testbench.UUT.S_AXI_ACLK \
    --show-waveform-time --time-unit ns --include-idle

// trace 0
trace {
}
error: [write@01?1!] executing step 4 of the transaction: 0 != 1
   ┌─ tests/fpga-debugging/axi-lite-s1/s1_buggy.prot:95:5
   │
95 │     DUT.S_AXI_BREADY := 1'b1;
   │     ^^^^^^^^^^^^^^^^^^^^^^^^^ [write@01?1!] executing step 4 of the transaction: 0 != 1

Error: "Monitor failed"

Edit: The BI / monitor also fail on the waveform for the fixed DUT (s1_fixed_workload1.vcd), so I think the .prot file needs some modification. It may be worth examining the fixed / buggy waveforms for workload 2 instead (since that pertains to reads and not writes, i.e. involves one fewer channel).

[ekiwi]

Do we really need to specify separate BI_CASES? @ngernest : can you try using the MONITOR_CASES instead?

[ngernest]

Ah good point, bi and monitor take mostly the same CLI args (IIRC) so maybe we can use MONITOR_CASES -- will try this out!

[ekiwi]

@ngernest : now that we have the new testing infrastructure, can you have just one protocol for s1 instead of separate ones for buggy and fixed?

[ngernest]

Ah yes, I think that should be possible since we're no longer using Turnt -- good point, thanks!

[ekiwi]

I know that you are still working on fixing the protocol, so I did not look at that.
However, there are a couple of other changes in here that I want to provide some feedback on:

• Can you make a separate PR for adding the bi to the tests and to CI? Then we can iterate on how to best integrate this with the new testing infrastrucutre.
• You should also try to only have a single .prot for each one of the brave new world benchmarks. After all, our claim is that a single correct protocol can distinguish between buggy and fixed version. I think the reason we used to maintain two copies was because of how turnt test discovery works. With the new testing infrastructure, we should not have to do that anymore.

[ngernest]

Sounds good, thanks! I will make the testing infrastructure changes in a separate PR (hopefully later in the week). I may also try a simpler BNW bug to drive/monitor in the meantime, e.g., an AXI-Stream one since it has fewer channels than AXI-Lite (this bug). (I picked this axi-lite-s1 bug to begin with because the Verilog DUT code is contained within the one file, unlike some of the other BNW bugs, but it might be worth starting with a simpler protocol before proceeding to AXI-Lite.)