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

cli/src/main.rs

@@ -23,6 +23,10 @@ struct Args {
     )]
     protocol: Vec<String>,
 
+    /// Allow arguments to appear in while/if conditions
+    #[arg(long)]
+    allow_branch_on_arg: bool,
+
     #[command(subcommand)]
     command: Option<Cmds>,
 }
@@ -203,8 +207,13 @@ fn main() {
     // we always parse and type check the protocol file
     let skip_static_step_fork_checks = false;
     let mut d = DiagnosticHandler::new(ColorChoice::Auto, false, true, false);
-    let (st, modules) =
-        frontend(&args.protocol, &mut d, skip_static_step_fork_checks, false).unwrap();
+    let (st, modules) = frontend(
+        &args.protocol,
+        &mut d,
+        skip_static_step_fork_checks,
+        args.allow_branch_on_arg,
+    )
+    .unwrap();
 
     match args.command {
         None => {}

interp/src/main.rs

@@ -69,6 +69,10 @@ struct Cli {
     /// Prints only trace status lines and ASCII waveforms
     #[arg(long)]
     ascii_waveform: bool,
+
+    /// Allow arguments to appear in while/if conditions
+    #[arg(long)]
+    allow_branch_on_arg: bool,
 }
 
 /// Examples (enables all tracing logs):
@@ -136,7 +140,7 @@ fn main() -> anyhow::Result<()> {
         &cli.protocol,
         &mut protocols_handler,
         cli.skip_static_step_fork_checks,
-        false,
+        cli.allow_branch_on_arg,
     ) {
         Ok(result) => result,
         Err(error) => exit_after_setup_error(error, !protocols_handler.error_string().is_empty()),

protocols/src/errors.rs

@@ -120,6 +120,7 @@ pub enum ThreadError {
         thread_idx: usize,
         transaction_name: String,
         stmt_id: StmtId,
+        step_count: u32,
     },
     /// Thread execution limit exceeded (for infinite loop protection)
     ExecutionLimitExceeded { max_steps: usize },
@@ -344,11 +345,13 @@ impl fmt::Display for ThreadError {
                 new_value,
                 thread_idx,
                 transaction_name,
+                step_count,
                 ..
             } => {
                 write!(
                     f,
-                    "Thread {} (`{}`) attempted conflicting assignment to '{}': current={}, new={}",
+                    "@{} Thread {} (`{}`) attempted conflicting assignment to '{}': current={}, new={}",
+                    step_count,
                     thread_idx,
                     transaction_name,
                     symbol_name,
@@ -514,6 +517,7 @@ impl ExecutionError {
         thread_idx: usize,
         transaction_name: String,
         stmt_id: StmtId,
+        step_count: u32,
     ) -> Self {
         ExecutionError::Thread(ThreadError::ConflictingAssignment {
             symbol_name,
@@ -522,6 +526,7 @@ impl ExecutionError {
             thread_idx,
             transaction_name,
             stmt_id,
+            step_count,
         })
     }
 
@@ -895,13 +900,15 @@ impl DiagnosticEmitter {
                 thread_idx,
                 transaction_name,
                 stmt_id,
+                step_count,
                 ..
             } => {
                 handler.emit_diagnostic_stmt(
                     transaction,
                     stmt_id,
                     &format!(
-                        "Thread {} (`{}`) attempted conflicting assignment to '{}': current={}, new={}",
+                        "@{} Thread {} (`{}`) attempted conflicting assignment to '{}': current={}, new={}",
+                        step_count,
                         thread_idx,
                         transaction_name,
                         symbol_name,

protocols/src/scheduler.rs

@@ -448,6 +448,7 @@ impl<'a> Scheduler<'a> {
                                 *first_idx,
                                 first_transaction_name,
                                 first_stmt_id.expect("Concrete values should have stmt_id"),
+                                self.step_count,
                             ),
                         ));
 
@@ -461,6 +462,7 @@ impl<'a> Scheduler<'a> {
                                 *second_idx,
                                 second_transaction_name,
                                 second_stmt_id.expect("Concrete values should have stmt_id"),
+                                self.step_count,
                             ),
                         ));
 

runt/bi/runt.toml

@@ -2377,22 +2377,31 @@ expect_name = "s2_fixed.bi.expect"
 cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axi-stream-s2/s2.prot --wave tests/fpga-debugging/axi-stream-s2/s2_fixed.fst --instances TOP.testbench.UUT:AXISManager --sample-posedge TOP.testbench.UUT.M_AXIS_ACLK --show-waveform-time --time-unit ns 2>&1"
 
 [[tests]]
-name = "bi.tests_fpga_debugging_axis_adapter_s3_s3_buggy.s3_buggy_bi"
+name = "bi.tests_fpga_debugging_axis_adapter_s3_s3.s3_buggy_bi"
 paths = [
-  "../../tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot",
+  "../../tests/fpga-debugging/axis-adapter-s3/s3.prot",
 ]
 expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects"
 expect_name = "s3_buggy.bi.expect"
-cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_buggy.fst --instances TOP.test_axis_adapter_64_8.UUT:AXISManager --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --time-unit ns 2>&1"
+cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_buggy.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --include-idle --time-unit ns --display-hex --allow-branch-on-arg 2>&1"
 
 [[tests]]
-name = "bi.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_bi"
+name = "bi.tests_fpga_debugging_axis_adapter_s3_s3.s3_fixed_bi"
 paths = [
-  "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot",
+  "../../tests/fpga-debugging/axis-adapter-s3/s3.prot",
 ]
 expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects"
 expect_name = "s3_fixed.bi.expect"
-cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst --instances TOP.test_axis_adapter_64_8.UUT:AXISManager --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --time-unit ns 2>&1"
+cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst --instances TOP.test_axis_adapter_64_8.UUT:AXIS --sample-posedge TOP.test_axis_adapter_64_8.UUT.clk --show-waveform-time --include-idle --time-unit ns --display-hex --allow-branch-on-arg 2>&1"
+
+[[tests]]
+name = "bi.tests_fpga_debugging_axis_adapter_s3_s3.s3_fixed_tx_bi"
+paths = [
+  "../../tests/fpga-debugging/axis-adapter-s3/s3.prot",
+]
+expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects"
+expect_name = "s3_fixed_tx.bi.expect"
+cmd = "cd ../.. && target/debug/bi --color never --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --wave tests/fpga-debugging/axis-adapter-s3/s3_fixed_tx.fst --instances dut:AXIS --show-steps --include-idle --display-hex --allow-branch-on-arg 2>&1"
 
 [[tests]]
 name = "bi.tests_fpga_debugging_axis_async_fifo_c4_c4.c4_buggy_bi"

runt/interp/runt.toml

@@ -450,6 +450,15 @@ expect_dir = "../../tests/fpga-debugging/axi-stream-s2/expects"
 expect_name = "s2_fixed.interp.expect"
 cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axi-stream-s2/s2_fixed.tx --verilog tests/fpga-debugging/axi-stream-s2/s2_fixed.v --protocol tests/fpga-debugging/axi-stream-s2/s2.prot --module xlnxstream_2018_3 2>&1"
 
+[[tests]]
+name = "interp.tests_fpga_debugging_axis_adapter_s3_s3_fixed.s3_fixed_interp"
+paths = [
+  "../../tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx",
+]
+expect_dir = "../../tests/fpga-debugging/axis-adapter-s3/expects"
+expect_name = "s3_fixed.interp.expect"
+cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx --allow-branch-on-arg --verilog tests/fpga-debugging/axis-adapter-s3/s3_fixed.v --protocol tests/fpga-debugging/axis-adapter-s3/s3.prot --module axis_adapter 2>&1"
+
 [[tests]]
 name = "interp.tests_fpga_debugging_axis_async_fifo_c4_c4_buggy.c4_buggy_interp"
 paths = [

scripts/generate_runt_configs.py

@@ -252,9 +252,11 @@ def waveform_runt_command(case: dict) -> list[tuple[str, str]]:
     # (and still 1 min in release mode) to be worth running every time.
     # maybe in the future we can flag a slow/fast runt config
     # c4_fixed.tx is simply too long (stack overflows in execution) for now but is fixable
+    # Note: ignoring `s3_fixed.tx` for graph-interpreter for now as it is a Brave New World test case
     if (
         case["paths"][0] != "examples/picorv32/unsigned_mul.tx"
         and case["paths"][0] != "tests/fpga-debugging/axis-async-fifo-c4/c4_fixed.tx"
+        and case["paths"][0] != "tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx"
     ):
         variants.append(("bmc", repo_root_command(bounded_cmd, stderr="discard")))
 
@@ -329,6 +331,7 @@ def protocol_constructs(protocol_path: str) -> frozenset[str]:
             "--bin",
             "protocols-cli",
             "--",
+            "--allow-branch-on-arg",
             "-p",
             protocol_path,
             "constructs",
@@ -357,6 +360,10 @@ def graph_interp_cases(cases: list[dict]) -> list[dict]:
         if c["expected"] == "pass"
         and not graph_interp_unsupported & protocol_constructs(c["protocol_path"])
     ]
+    # exclude s3 from graph_interp cases
+    # TODO: re-include
+    selected = [c for c in selected if not c["protocol_path"].endswith("s3.prot")]
+
     return sorted(selected, key=lambda c: c["paths"][0])
 
 

scripts/test_catalog.py

@@ -305,6 +305,13 @@
         "top": "fifo_wrapper",
         "expect": "pass",
     },
+    "tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx": {
+        "protocol": "tests/fpga-debugging/axis-adapter-s3/s3.prot",
+        "verilog": ("tests/fpga-debugging/axis-adapter-s3/s3_fixed.v",),
+        "top": "axis_adapter",
+        "expect": "pass",
+        "extra_args": ("--allow-branch-on-arg",),
+    },
     "tests/fpga-debugging/axi-stream-s2/s2_fixed.tx": {
         "protocol": "tests/fpga-debugging/axi-stream-s2/s2.prot",
         "verilog": ("tests/fpga-debugging/axi-stream-s2/s2_fixed.v",),
@@ -699,29 +706,47 @@
         ),
     },
     "tests.fpga-debugging.axis-adapter-s3.s3_buggy": {
-        "protocol": "tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot",
+        "protocol": "tests/fpga-debugging/axis-adapter-s3/s3.prot",
         "wave": "tests/fpga-debugging/axis-adapter-s3/s3_buggy.fst",
-        "instances": ("TOP.test_axis_adapter_64_8.UUT:AXISManager",),
+        "instances": ("TOP.test_axis_adapter_64_8.UUT:AXIS",),
         "expect": "pass",
         "extra_args": (
             "--sample-posedge",
             "TOP.test_axis_adapter_64_8.UUT.clk",
             "--show-waveform-time",
+            "--include-idle",
             "--time-unit",
             "ns",
+            "--display-hex",
+            "--allow-branch-on-arg",
         ),
     },
     "tests.fpga-debugging.axis-adapter-s3.s3_fixed": {
-        "protocol": "tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot",
+        "protocol": "tests/fpga-debugging/axis-adapter-s3/s3.prot",
         "wave": "tests/fpga-debugging/axis-adapter-s3/s3_fixed.fst",
-        "instances": ("TOP.test_axis_adapter_64_8.UUT:AXISManager",),
+        "instances": ("TOP.test_axis_adapter_64_8.UUT:AXIS",),
         "expect": "pass",
         "extra_args": (
             "--sample-posedge",
             "TOP.test_axis_adapter_64_8.UUT.clk",
             "--show-waveform-time",
+            "--include-idle",
             "--time-unit",
             "ns",
+            "--display-hex",
+            "--allow-branch-on-arg",
+        ),
+    },
+    "tests.fpga-debugging.axis-adapter-s3.s3_fixed.on_test_trace": {
+        "protocol": "tests/fpga-debugging/axis-adapter-s3/s3.prot",
+        "wave": "tests/fpga-debugging/axis-adapter-s3/s3_fixed_tx.fst",
+        "instances": ("dut:AXIS",),
+        "expect": "pass",
+        "extra_args": (
+            "--show-steps",
+            "--include-idle",
+            "--display-hex",
+            "--allow-branch-on-arg",
         ),
     },
     "tests.fpga-debugging.axis-async-fifo-c4.c4_buggy": {

tests/adders/adder_d1/expects/add_incorrect.interp.expect

@@ -1,14 +1,14 @@
-error: Thread 0 (`add_incorrect`) attempted conflicting assignment to 'b': current=5, new=2
+error: @1 Thread 0 (`add_incorrect`) attempted conflicting assignment to 'b': current=5, new=2
    ┌─ tests/adders/adder_d1/add_d1.prot:35:3
    │
 35 │   DUT.b := b;
-   │   ^^^^^^^^^^^ Thread 0 (`add_incorrect`) attempted conflicting assignment to 'b': current=5, new=2
+   │   ^^^^^^^^^^^ @1 Thread 0 (`add_incorrect`) attempted conflicting assignment to 'b': current=5, new=2
 
-error: Thread 1 (`add_incorrect`) attempted conflicting assignment to 'b': current=2, new=5
+error: @1 Thread 1 (`add_incorrect`) attempted conflicting assignment to 'b': current=2, new=5
    ┌─ tests/adders/adder_d1/add_d1.prot:32:3
    │
 32 │   DUT.b := b;
-   │   ^^^^^^^^^^^ Thread 1 (`add_incorrect`) attempted conflicting assignment to 'b': current=2, new=5
+   │   ^^^^^^^^^^^ @1 Thread 1 (`add_incorrect`) attempted conflicting assignment to 'b': current=2, new=5
 
 Trace 0 execution failed.
 ---CODE---

tests/adders/adder_d1/expects/add_incorrect_implicit.interp.expect

@@ -1,14 +1,14 @@
-error: Thread 0 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=5, new=2
+error: @1 Thread 0 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=5, new=2
    ┌─ tests/adders/adder_d1/add_d1.prot:43:3
    │
 43 │   DUT.b := b;
-   │   ^^^^^^^^^^^ Thread 0 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=5, new=2
+   │   ^^^^^^^^^^^ @1 Thread 0 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=5, new=2
 
-error: Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5
+error: @1 Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5
    ┌─ tests/adders/adder_d1/add_d1.prot:43:3
    │
 43 │   DUT.b := b;
-   │   ^^^^^^^^^^^ Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5
+   │   ^^^^^^^^^^^ @1 Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5
 
 Trace 0 execution failed.
 ---CODE---

tests/adders/adder_d1/expects/wait_and_add_incorrect_implicit.interp.expect

@@ -1,14 +1,14 @@
-error: Thread 0 (`wait_and_add`) attempted conflicting assignment to 'b': current=5, new=2
+error: @2 Thread 0 (`wait_and_add`) attempted conflicting assignment to 'b': current=5, new=2
    ┌─ tests/adders/adder_d1/add_d1.prot:62:3
    │
 62 │   DUT.b := b;
-   │   ^^^^^^^^^^^ Thread 0 (`wait_and_add`) attempted conflicting assignment to 'b': current=5, new=2
+   │   ^^^^^^^^^^^ @2 Thread 0 (`wait_and_add`) attempted conflicting assignment to 'b': current=5, new=2
 
-error: Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5
+error: @2 Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5
    ┌─ tests/adders/adder_d1/add_d1.prot:43:3
    │
 43 │   DUT.b := b;
-   │   ^^^^^^^^^^^ Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5
+   │   ^^^^^^^^^^^ @2 Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'b': current=2, new=5
 
 Trace 0 execution failed.
 ---CODE---

tests/adders/adder_d2/expects/no_dontcare_conflict.interp.expect

@@ -1,14 +1,14 @@
-error: Thread 0 (`add`) attempted conflicting assignment to 'b': current=5, new=2
+error: @1 Thread 0 (`add`) attempted conflicting assignment to 'b': current=5, new=2
    ┌─ tests/adders/adder_d2/no_dontcare_conflict.prot:13:3
    │
 13 │   DUT.b := b;
-   │   ^^^^^^^^^^^ Thread 0 (`add`) attempted conflicting assignment to 'b': current=5, new=2
+   │   ^^^^^^^^^^^ @1 Thread 0 (`add`) attempted conflicting assignment to 'b': current=5, new=2
 
-error: Thread 1 (`add`) attempted conflicting assignment to 'b': current=2, new=5
+error: @1 Thread 1 (`add`) attempted conflicting assignment to 'b': current=2, new=5
    ┌─ tests/adders/adder_d2/no_dontcare_conflict.prot:13:3
    │
 13 │   DUT.b := b;
-   │   ^^^^^^^^^^^ Thread 1 (`add`) attempted conflicting assignment to 'b': current=2, new=5
+   │   ^^^^^^^^^^^ @1 Thread 1 (`add`) attempted conflicting assignment to 'b': current=2, new=5
 
 Trace 0 execution failed.
 ---CODE---

tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect

@@ -1,13 +1,32 @@
 // trace 0
 trace {
-    reset();  // [time: 0ns -> 25ns]
-    wait_for_data();  // [time: 25ns -> 50ns]
-    wait_for_data();  // [time: 50ns -> 75ns]
-    wait_for_data();  // [time: 75ns -> 100ns]
-    recv(205);  // [time: 100ns -> 125ns]
-    recv(171);  // [time: 125ns -> 150ns]
-    recv(205);  // [time: 150ns -> 175ns]
-    recv(171);  // [time: 175ns -> 200ns]
-    recv(205);  // [time: 200ns -> 225ns]
-    recv_last(171);  // [time: 225ns -> 225ns]
+    reset();  // [time: 0ns -> 50ns]
+    idle();  // [time: 25ns -> 50ns]
+    idle();  // [time: 50ns -> 75ns]
+    idle();  // [time: 100ns -> 125ns]
+    idle();  // [time: 125ns -> 150ns]
+    idle();  // [time: 150ns -> 175ns]
+    idle();  // [time: 175ns -> 200ns]
 }
+error: [split_word@3] executing step 5 of the transaction: 0 != 1
+    ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:284:29
+    │
+284 │                             assert_eq(DUT.output_axis_tlast, is_final_word_in_packet);
+    │                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1
+
+
+error: [split_word@3] executing step 5 of the transaction: 0 != 1
+    ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:284:29
+    │
+284 │                             assert_eq(DUT.output_axis_tlast, is_final_word_in_packet);
+    │                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1
+
+
+error: [split_word@3] executing step 5 of the transaction: 0 != 1
+    ┌─ tests/fpga-debugging/axis-adapter-s3/s3.prot:284:29
+    │
+284 │                             assert_eq(DUT.output_axis_tlast, is_final_word_in_packet);
+    │                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [split_word@3] executing step 5 of the transaction: 0 != 1
+
+---CODE---
+1