diff --git a/cli/src/main.rs b/cli/src/main.rs index f9b929d6..1a8aa773 100644 --- a/cli/src/main.rs +++ b/cli/src/main.rs @@ -23,6 +23,10 @@ struct Args { )] protocol: Vec, + /// Allow arguments to appear in while/if conditions + #[arg(long)] + allow_branch_on_arg: bool, + #[command(subcommand)] command: Option, } @@ -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 => {} diff --git a/interp/src/main.rs b/interp/src/main.rs index 9e4e7b19..ca1a1b6c 100644 --- a/interp/src/main.rs +++ b/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()), diff --git a/protocols/src/errors.rs b/protocols/src/errors.rs index d2e0b057..461b2f48 100644 --- a/protocols/src/errors.rs +++ b/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, diff --git a/protocols/src/scheduler.rs b/protocols/src/scheduler.rs index b264387c..9890123f 100644 --- a/protocols/src/scheduler.rs +++ b/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, ), )); diff --git a/runt/bi/runt.toml b/runt/bi/runt.toml index b1be5db9..63d4f7df 100644 --- a/runt/bi/runt.toml +++ b/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" diff --git a/runt/interp/runt.toml b/runt/interp/runt.toml index 428844fb..03703603 100644 --- a/runt/interp/runt.toml +++ b/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 = [ diff --git a/scripts/generate_runt_configs.py b/scripts/generate_runt_configs.py index 56e296a0..401c649d 100644 --- a/scripts/generate_runt_configs.py +++ b/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]) diff --git a/scripts/test_catalog.py b/scripts/test_catalog.py index 3b7def3c..8c048c8e 100644 --- a/scripts/test_catalog.py +++ b/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": { diff --git a/tests/adders/adder_d1/expects/add_incorrect.interp.expect b/tests/adders/adder_d1/expects/add_incorrect.interp.expect index d0eb1d14..d71f4222 100644 --- a/tests/adders/adder_d1/expects/add_incorrect.interp.expect +++ b/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--- diff --git a/tests/adders/adder_d1/expects/add_incorrect_implicit.interp.expect b/tests/adders/adder_d1/expects/add_incorrect_implicit.interp.expect index dddb0b90..bd12e778 100644 --- a/tests/adders/adder_d1/expects/add_incorrect_implicit.interp.expect +++ b/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--- diff --git a/tests/adders/adder_d1/expects/wait_and_add_incorrect_implicit.interp.expect b/tests/adders/adder_d1/expects/wait_and_add_incorrect_implicit.interp.expect index cf5d0666..8f0a1b3b 100644 --- a/tests/adders/adder_d1/expects/wait_and_add_incorrect_implicit.interp.expect +++ b/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--- diff --git a/tests/adders/adder_d2/expects/no_dontcare_conflict.interp.expect b/tests/adders/adder_d2/expects/no_dontcare_conflict.interp.expect index 10afa5ec..91f474f5 100644 --- a/tests/adders/adder_d2/expects/no_dontcare_conflict.interp.expect +++ b/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--- diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect index 204d6b80..b22c8c43 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_buggy.bi.expect +++ b/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 diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect index 5cbf6070..9a7036dc 100644 --- a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.bi.expect @@ -1,12 +1,12 @@ // 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_last(205); // [time: 200ns -> 200ns] + 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] + split_word(0xabcdabcdabcdabcd, 0x1f, 0x1); // [time: 75ns -> 200ns] + idle(); // [time: 200ns -> 200ns] } diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.interp.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.interp.expect new file mode 100644 index 00000000..f5f6cb49 --- /dev/null +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed.interp.expect @@ -0,0 +1 @@ +Trace 0 executed successfully! diff --git a/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed_tx.bi.expect b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed_tx.bi.expect new file mode 100644 index 00000000..9a51880f --- /dev/null +++ b/tests/fpga-debugging/axis-adapter-s3/expects/s3_fixed_tx.bi.expect @@ -0,0 +1,71 @@ +// trace 0 +trace { + idle(); [0] + reset(); [1 .. 2] + idle(); [2] + idle(); [4] + idle(); [5] + idle(); [6] + idle(); [7] + split_word(0xabcdabcdabcdabcd, 0x1f, 0x1); [3 .. 8] + idle(); [8] + idle(); [9] + reset(); [10 .. 11] + idle(); [11] + split_word(0x0000000000000011, 0x01, 0x0); [12 .. 13] + split_word(0x0000000000002211, 0x03, 0x0); [13 .. 15] + split_word(0x0000000000332211, 0x07, 0x0); [14 .. 18] + split_word(0x0000000044332211, 0x0f, 0x0); [16 .. 22] + split_word(0x0000005544332211, 0x1f, 0x0); [19 .. 27] + split_word(0x0000665544332211, 0x3f, 0x0); [23 .. 33] + split_word(0x0077665544332211, 0x7f, 0x0); [28 .. 40] + split_word(0x8877665544332211, 0xff, 0x0); [34 .. 48] + split_word(0x0000000000000011, 0x01, 0x0); [41 .. 49] + split_word(0x0000000000002211, 0x03, 0x1); [49 .. 51] + split_word(0x0000000000332211, 0x07, 0x1); [50 .. 54] + split_word(0x0000000044332211, 0x0f, 0x1); [52 .. 58] + split_word(0x0000005544332211, 0x1f, 0x1); [55 .. 63] + split_word(0x0000665544332211, 0x3f, 0x1); [59 .. 69] + split_word(0x0077665544332211, 0x7f, 0x1); [64 .. 76] + idle(); [77] + split_word(0x8877665544332211, 0xff, 0x1); [70 .. 84] + split_word(0x0000000000000011, 0x01, 0x0); [78 .. 85] + idle(); [85] + idle(); [87] + split_word(0x0000000000002211, 0x03, 0x0); [86 .. 88] + idle(); [89] + split_word(0x0000000000332211, 0x07, 0x0); [88 .. 91] + idle(); [92] + split_word(0x0000000044332211, 0x0f, 0x0); [90 .. 95] + idle(); [96] + split_word(0x0000005544332211, 0x1f, 0x0); [93 .. 100] + idle(); [101] + split_word(0x0000665544332211, 0x3f, 0x0); [97 .. 106] + idle(); [107] + split_word(0x0077665544332211, 0x7f, 0x0); [102 .. 113] + idle(); [114] + split_word(0x8877665544332211, 0xff, 0x0); [108 .. 121] + split_word(0x0000000000000011, 0x01, 0x0); [115 .. 122] + idle(); [122] + idle(); [124] + split_word(0x0000000000002211, 0x03, 0x1); [123 .. 125] + idle(); [126] + split_word(0x0000000000332211, 0x07, 0x1); [125 .. 128] + idle(); [129] + split_word(0x0000000044332211, 0x0f, 0x1); [127 .. 132] + idle(); [133] + split_word(0x0000005544332211, 0x1f, 0x1); [130 .. 137] + idle(); [138] + split_word(0x0000665544332211, 0x3f, 0x1); [134 .. 143] + idle(); [144] + split_word(0x0077665544332211, 0x7f, 0x1); [139 .. 150] + idle(); [151] + idle(); [152] + idle(); [153] + idle(); [154] + idle(); [155] + idle(); [156] + idle(); [157] + split_word(0x8877665544332211, 0xff, 0x1); [145 .. 158] + idle(); [158] +} diff --git a/tests/fpga-debugging/axis-adapter-s3/s3.prot b/tests/fpga-debugging/axis-adapter-s3/s3.prot new file mode 100644 index 00000000..fa99b267 --- /dev/null +++ b/tests/fpga-debugging/axis-adapter-s3/s3.prot @@ -0,0 +1,317 @@ +// This file describes an AXI-Stream width adapter which +// converts a 64-bit input into 8-bit output chunks over multiple cycles + +// Notes: +// - The DUT has 3 termination conditions: +// - 1. All 8 bytes have been emitted (in the fixed DUT, this only happens when `tkeep = 11111111`, i.e. all bytes of `tdata` are meaningful) +// - 2. When emitting the i-th byte, the DUT sees that `tkeep[i] = 0`, in which case it treats the i-th byte as the last one and stops emitting any further bytes +// - 3. For the fixed DUT only, if `tkeep[i] = 1` but `tkeep[i+1] = 0`, then the DUT treats the `i`-th byte as the last one +// and stops emitting any further bytes (the fixed DUT gains this "lookahead" logic) +// - The `tlast` parameter indicates if the data word corresponds to the final word of a packet +// (Note: there can be multiple words in a packet. Moreover, the last byte of a non-final word in a packet +// still gets `tlast = 0`, since it is not the last word of a packet.) +// - AXI-Stream spec says that for "downsizing" operations in which data with larger bit-widths +// are converted to smaller bitwidths (section 2.3.3), which this DUT is doing, +// if the input data word happens to be the last word of a packet (i.e. `tlast = 1` for the input), +// in the output sequence of bytes, `tlast` can only be asserted for the last byte emitted +// - The DUT cannot accept a new 64-bit input when it is still emitting the bytes of the existing data +// - The DUT examines `tkeep` from right to left, i.e. the 0th byte emitted +// corresponds to `tdata[7:0]` and `tkeep[0]` (the LSB of `tkeep`) +// - The fixed waveform has `tkeep = 0001 1111`, so only 5 bytes are emitted and the +// waveform ends after the 5 bytes are emitted +// - The `output_bytes` parameter to the `send_word` protocol below contains +// the bytes in the order they're emitted, and since the DUT examines `tdata` right to left, +// this means if `tdata = 0xABCD`, the output bytes are `[0xCD, 0xAB]` +// (i.e. the bytes corresponding to less significant bits are emitted first) + +struct AXIS { + // Reset is active-high + in rst: u1, + + // Signals related to the DUT accepting input data from the environment + + // 64-bit data that the DUT accepts as input from the environment + in input_axis_tdata: u64, + + // bitmask indicating which bytes of `tdata` are meaningful + in input_axis_tkeep: u8, + + // 1 if this is the last word in a packet + in input_axis_tlast: u1, + + // Indicates if `input_tdata` contains valid data + in input_axis_tvalid: u1, + + // Signal indicating whether the DUT + // is ready to accept data from the environment as input + out input_axis_tready: u1, + + //---------------------------------------------------------------- + // Signals related to the DUT emitting data as output + + // 8-bit data that the DUT emits as output + out output_axis_tdata: u8, + + // Output data is 8 bits, so `tkeep` is now just 1 bit wide + // `tkeep` is 1 if `output_tdata` contains meaningful data + out output_axis_tkeep: u1, + + // 1 if this is the last word in a packet + out output_axis_tlast: u1, + + // Indicates if `output_data` contains valid data + out output_axis_tvalid: u1, + + // Signal indicating whether the environment is ready to + // accept the data emitted by the DUT as output + in output_axis_tready: u1, +} + +prot reset() { + DUT.rst := 1'b1; + + // Valid pin (for both directions) must be low when + // reset is asserted (AXI-Stream spec section 2.7.2) + DUT.input_axis_tvalid := 1'b0; + step(); + + DUT.rst := X; + DUT.input_axis_tvalid := X; + // one cycle after reset, the output t_valid must be deasserted + assert_eq(DUT.output_axis_tvalid, 1'b0); + fork(); + step(); +} + +// When idle, the DUT neither accepts data from the environment, +// nor does it emit data as output +#[idle] +prot idle() { + DUT.rst := 1'b0; + DUT.input_axis_tvalid := 1'b0; + step(); +} + +// - `is_final_word_in_packet` is a parameter that represents `tlast` +// (this variable name was chosen to be more informative and to avoid confusion with our DSL's `is_last()` construct) +prot split_word(data: u64, keep: u8, is_final_word_in_packet: u1) { + DUT.rst := 1'b0; + DUT.input_axis_tdata := data; + DUT.input_axis_tkeep := keep; + DUT.input_axis_tlast := is_final_word_in_packet; + + // There is valid data (namely the input word), so set `valid = 1` + DUT.input_axis_tvalid := 1'b1; + + // Wait until the DUT signals it is ready to accept to the input word + while (!(DUT.input_axis_tready == 1'b1)) { + step(); + } + // One cycle for DUT to accept input data from environment + step(); + + // DUT has accepted input data, so we set the input pins to DontCare + DUT.input_axis_tdata := X; + DUT.input_axis_tkeep := X; + DUT.input_axis_tlast := X; + // valid can be anything from now on, it is on the DUT to assert backpressure until it is ready + DUT.input_axis_tvalid := X; + fork(); + + // Environment is now ready to accept the output data emitted by the DUT + DUT.output_axis_tready := 1'b1; + + // Wait until the DUT indicates that there is valid data to emit + while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); + step(); + } + // Both ready & valid are now 1 in the output direction, + // so the DUT can begin to emit the 0th byte + + // Rightmost 8 bits of `data` are now on the `output_tdata` pin + assert_eq(DUT.output_axis_tdata, data[7:0]); + + // Check if 0th byte is meaningful + if (keep[0] == 1'b1) { + // keep[0] = 1, so the output tkeep must also be 1 + assert_eq(DUT.output_axis_tkeep, 1'b1); + + // Lookahead and check if 1st byte is also meaningful + if (keep[1] == 1'b1) { + // 1st byte is meaningful, so the 0th byte can't be the end of the packet, + // so output tlast must be 0 for the 0th byte + assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); + + // One clock cycle to emit the 0th byte + step(); + + // Wait till DUT has valid data to emit for the 1st byte + while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); + step(); + } + + assert_eq(DUT.output_axis_tdata, data[15:8]); + + // We've already established above that keep[1] = 1, so output tkeep must be 1 for the 1st byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + // Lookahead and check if 2nd byte is meaningful + if (keep[2] == 1'b1) { + // 2nd byte is meaningful, so the 1st byte can't be the end of the packet, + // so output tlast must be 0 for the 1st byte + assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); + + // One clock cycle to emit the 1st byte + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); + step(); + } + assert_eq(DUT.output_axis_tdata, data[23:16]); + + // We've already established above that keep[2] = 1, so output tkeep must be 1 for the 2nd byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + // Check if 3rd byte is meaningful + if (keep[3] == 1'b1) { + // 3rd byte is meaningful, so the 2nd byte can't be the end of the packet, + // so output tlast must be 0 for the 2nd byte + assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); + + // One clock cycle to emit the 2nd byte + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); + step(); + } + assert_eq(DUT.output_axis_tdata, data[31:24]); + + // We've already established above that keep[3] = 1, so output tkeep must be 1 for the 3rd byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + if (keep[4] == 1'b1) { + // 4th byte is meaningful, so output tlast must be 0 for the 3rd byte + assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); + + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); + step(); + } + + assert_eq(DUT.output_axis_tdata, data[39:32]); + + // We've already established above that keep[4] = 1, so output tkeep must be 1 for the 4th byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + if (keep[5] == 1'b1) { + // 5th byte is meaningful, so output tlast must be 0 for the 4th byte + assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); + + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); + step(); + } + assert_eq(DUT.output_axis_tdata, data[47:40]); + + // We've already established above that keep[5] = 1, so output tkeep must be 1 for the 5th byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + if (keep[6] == 1'b1) { + // 6th byte is meaningful, so output tlast must be 0 for the 5th byte + assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); + + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); + step(); + } + assert_eq(DUT.output_axis_tdata, data[55:48]); + + // We've already established above that keep[6] = 1, so output tkeep must be 1 for the 6th byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + if (keep[7] == 1'b1) { + // 7th byte is meaningful, so output tlast must be 0 for the 6th byte + assert_eq(DUT.output_axis_tlast, 1'b0); + assert_eq(DUT.input_axis_tready, 1'b0); + + step(); + + while (!(DUT.output_axis_tvalid == 1'b1)) { + assert_eq(DUT.input_axis_tready, 1'b0); + step(); + } + assert_eq(DUT.output_axis_tdata, data[63:56]); + + // We've already established above that keep[7] = 1, so output tkeep must be 1 for the 7th byte + assert_eq(DUT.output_axis_tkeep, 1'b1); + + // The 7th byte is the last byte for a 64-bit word, + // so we don't need to inspect the `tkeep` bit for the "next" byte + // We only need to check whether this byte is the end of the + // of the entire packet, which is determined by the `is_final_word_in_packet` parameter + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + + // One clock cycle to emit the 7th and final byte + step(); + } else { + // keep[6] = 1, keep[7] = 0 + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // keep[5] = 1, keep[6] = 0 + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // keep[4] = 1, keep[5] = 0 + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // Here we have keep[3] = 1, keep[4] = 0 + // so the 3rd byte is the last byte emitted by the DUT + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // Here we have keep[2] = 1 and keep[3] = 0, + // so the 2nd byte is the last byte emitted by the DUT + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // Here we have keep[1] = 1 and keep[2] = 0, + // so the 1st byte is the last byte emitted by the DUT + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // Here we have keep[0] = 1 and keep[1] = 0, + // so the 0th byte is the last byte emitted by the DUT + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } + } else { + // keep[0] = 0, so output tkeep must also be 0 and no meaningful bytes are emitted + assert_eq(DUT.output_axis_tkeep, 1'b0); + assert_eq(DUT.output_axis_tlast, is_final_word_in_packet); + step(); + } +} diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot b/tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot deleted file mode 100644 index 023e0f32..00000000 --- a/tests/fpga-debugging/axis-adapter-s3/s3_buggy.prot +++ /dev/null @@ -1,113 +0,0 @@ -// Source (manager) that outputs a sequence of 8 words -struct AXISManager { - // Control signals - in rst: u1, // Active-low reset - - // AXI-Stream manager outputs (from DUT perspective) - out output_axis_tvalid: u1, // manager has valid data - out output_axis_tdata: u8, // Data payload - out output_axis_tlast: u1, // Last word in packet - - // AXI-Stream sub-ordinate input - in output_axis_tready: u1, // Downstream ready to accept -} - -// RESET: Assert reset (active-low) and wait for manager to be ready -// The manager waits C_M_START_COUNT cycles in INIT_COUNTER before sending -prot reset() { - DUT.rst := 1'b1; // Assert reset (active-high) - DUT.output_axis_tready := 1'b0; - step(); -} - -// RECV: Receive one data word from the AXI-Stream manager -// Data transfer occurs when output_axis_tvalid and output_axis_tready are both 1 -// Only matches when data is immediately available (output_axis_tvalid = 1) -// -// Output Arguments: -// data - Expected payload from manager -prot recv( - data: u8, -) { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b1; // Signal ready to receive - - // Only matches when data is available - // (use wait_for_data for cycles when tready=1 but tvalid=0) - assert_eq(DUT.output_axis_tvalid, 1'b1); - - // Verify output data - assert_eq(DUT.output_axis_tdata, data); - - // Assert that this is *not* the last data word - assert_eq(DUT.output_axis_tlast, 1'b0); - - // One cycle for the transfer to complete - step(); -} - -// RECV_LAST: Receive the last data word (with output_axis_tlast asserted) -// This verifies both the data and that output_axis_tlast is properly set -// Only matches when data is immediately available (output_axis_tvalid = 1) -// -// Output Arguments: -// data - Expected payload from manager (should be the last word) -prot recv_last( - data: u8, -) { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b1; // Signal ready to receive - - // Only matches when data is available - assert_eq(DUT.output_axis_tvalid, 1'b1); - - // Verify output data and output_axis_tlast - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tlast, 1'b1); - - // One cycle for the transfer to complete - step(); -} - -// STALL: Assert backpressure (output_axis_tready=0) while manager has valid data -// AXI-Stream requires output args (tdata, tlast) to remain stable during stall -// Only matches when the waveform contains output_axis_tvalid=1 (i.e. there is some valid data and it's available to stall) -prot stall(data: u8, last: u1) { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b0; // Apply backpressure - - // Stall only applies when manager has valid data - // If output_axis_tvalid=0, this fails and we instead have an `idle` transaction - assert_eq(DUT.output_axis_tvalid, 1'b1); - - // Capture output values before the stall cycle - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tlast, last); - - step(); - - // Verify outputs remained stable during the stall - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tlast, last); - - step(); -} - -// WAIT_FOR_DATA: Receiver is ready but no data is available -// Used when tready=1 but tvalid=0 (i.e. receiver is polling for data) -prot wait_for_data() { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b1; - - // Only matches when no data is available - assert_eq(DUT.output_axis_tvalid, 1'b0); - step(); -} - -// IDLE: No transaction - output_axis_tready is deasserted -#[idle] -prot idle() { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b0; - step(); -} diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot b/tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot deleted file mode 100644 index 023e0f32..00000000 --- a/tests/fpga-debugging/axis-adapter-s3/s3_fixed.prot +++ /dev/null @@ -1,113 +0,0 @@ -// Source (manager) that outputs a sequence of 8 words -struct AXISManager { - // Control signals - in rst: u1, // Active-low reset - - // AXI-Stream manager outputs (from DUT perspective) - out output_axis_tvalid: u1, // manager has valid data - out output_axis_tdata: u8, // Data payload - out output_axis_tlast: u1, // Last word in packet - - // AXI-Stream sub-ordinate input - in output_axis_tready: u1, // Downstream ready to accept -} - -// RESET: Assert reset (active-low) and wait for manager to be ready -// The manager waits C_M_START_COUNT cycles in INIT_COUNTER before sending -prot reset() { - DUT.rst := 1'b1; // Assert reset (active-high) - DUT.output_axis_tready := 1'b0; - step(); -} - -// RECV: Receive one data word from the AXI-Stream manager -// Data transfer occurs when output_axis_tvalid and output_axis_tready are both 1 -// Only matches when data is immediately available (output_axis_tvalid = 1) -// -// Output Arguments: -// data - Expected payload from manager -prot recv( - data: u8, -) { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b1; // Signal ready to receive - - // Only matches when data is available - // (use wait_for_data for cycles when tready=1 but tvalid=0) - assert_eq(DUT.output_axis_tvalid, 1'b1); - - // Verify output data - assert_eq(DUT.output_axis_tdata, data); - - // Assert that this is *not* the last data word - assert_eq(DUT.output_axis_tlast, 1'b0); - - // One cycle for the transfer to complete - step(); -} - -// RECV_LAST: Receive the last data word (with output_axis_tlast asserted) -// This verifies both the data and that output_axis_tlast is properly set -// Only matches when data is immediately available (output_axis_tvalid = 1) -// -// Output Arguments: -// data - Expected payload from manager (should be the last word) -prot recv_last( - data: u8, -) { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b1; // Signal ready to receive - - // Only matches when data is available - assert_eq(DUT.output_axis_tvalid, 1'b1); - - // Verify output data and output_axis_tlast - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tlast, 1'b1); - - // One cycle for the transfer to complete - step(); -} - -// STALL: Assert backpressure (output_axis_tready=0) while manager has valid data -// AXI-Stream requires output args (tdata, tlast) to remain stable during stall -// Only matches when the waveform contains output_axis_tvalid=1 (i.e. there is some valid data and it's available to stall) -prot stall(data: u8, last: u1) { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b0; // Apply backpressure - - // Stall only applies when manager has valid data - // If output_axis_tvalid=0, this fails and we instead have an `idle` transaction - assert_eq(DUT.output_axis_tvalid, 1'b1); - - // Capture output values before the stall cycle - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tlast, last); - - step(); - - // Verify outputs remained stable during the stall - assert_eq(DUT.output_axis_tdata, data); - assert_eq(DUT.output_axis_tlast, last); - - step(); -} - -// WAIT_FOR_DATA: Receiver is ready but no data is available -// Used when tready=1 but tvalid=0 (i.e. receiver is polling for data) -prot wait_for_data() { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b1; - - // Only matches when no data is available - assert_eq(DUT.output_axis_tvalid, 1'b0); - step(); -} - -// IDLE: No transaction - output_axis_tready is deasserted -#[idle] -prot idle() { - DUT.rst := 1'b0; // Keep out of reset - DUT.output_axis_tready := 1'b0; - step(); -} diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx b/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx new file mode 100644 index 00000000..1895f1a1 --- /dev/null +++ b/tests/fpga-debugging/axis-adapter-s3/s3_fixed.tx @@ -0,0 +1,63 @@ +trace { + idle(); + 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); + // enough idle transactions to wait for split_word to finish before we can assert reset + idle(); idle(); idle(); idle(); idle(); idle(); + + // test a couple of input argument values + reset(); + idle(); + split_word(0x0000000000000011, 0b00000001, 0); + split_word(0x0000000000002211, 0b00000011, 0); + split_word(0x0000000000332211, 0b00000111, 0); + split_word(0x0000000044332211, 0b00001111, 0); + split_word(0x0000005544332211, 0b00011111, 0); + split_word(0x0000665544332211, 0b00111111, 0); + split_word(0x0077665544332211, 0b01111111, 0); + split_word(0x8877665544332211, 0b11111111, 0); + split_word(0x0000000000000011, 0b00000001, 0); + split_word(0x0000000000002211, 0b00000011, 1); + split_word(0x0000000000332211, 0b00000111, 1); + split_word(0x0000000044332211, 0b00001111, 1); + split_word(0x0000005544332211, 0b00011111, 1); + split_word(0x0000665544332211, 0b00111111, 1); + split_word(0x0077665544332211, 0b01111111, 1); + split_word(0x8877665544332211, 0b11111111, 1); + idle(); + split_word(0x0000000000000011, 0b00000001, 0); + idle(); + split_word(0x0000000000002211, 0b00000011, 0); + idle(); + split_word(0x0000000000332211, 0b00000111, 0); + idle(); + split_word(0x0000000044332211, 0b00001111, 0); + idle(); + split_word(0x0000005544332211, 0b00011111, 0); + idle(); + split_word(0x0000665544332211, 0b00111111, 0); + idle(); + split_word(0x0077665544332211, 0b01111111, 0); + idle(); + split_word(0x8877665544332211, 0b11111111, 0); + idle(); + split_word(0x0000000000000011, 0b00000001, 0); + idle(); + split_word(0x0000000000002211, 0b00000011, 1); + idle(); + split_word(0x0000000000332211, 0b00000111, 1); + idle(); + split_word(0x0000000044332211, 0b00001111, 1); + idle(); + split_word(0x0000005544332211, 0b00011111, 1); + idle(); + split_word(0x0000665544332211, 0b00111111, 1); + idle(); + split_word(0x0077665544332211, 0b01111111, 1); + idle(); + split_word(0x8877665544332211, 0b11111111, 1); + // enough idle transactions to finish the last split_word + idle(); idle(); idle(); idle(); idle(); idle(); idle(); idle(); +} diff --git a/tests/fpga-debugging/axis-adapter-s3/s3_fixed_tx.fst b/tests/fpga-debugging/axis-adapter-s3/s3_fixed_tx.fst new file mode 100644 index 00000000..ae042ba4 Binary files /dev/null and b/tests/fpga-debugging/axis-adapter-s3/s3_fixed_tx.fst differ diff --git a/tests/identities/identity_d2/expects/two_different_assignments_error.interp.expect b/tests/identities/identity_d2/expects/two_different_assignments_error.interp.expect index 8240ded2..1fcd4e59 100644 --- a/tests/identities/identity_d2/expects/two_different_assignments_error.interp.expect +++ b/tests/identities/identity_d2/expects/two_different_assignments_error.interp.expect @@ -1,14 +1,14 @@ -error: Thread 0 (`multiple_assign`) attempted conflicting assignment to 'a': current=2, new=1 +error: @1 Thread 0 (`multiple_assign`) attempted conflicting assignment to 'a': current=2, new=1 ┌─ tests/identities/identity_d2/identity_d2.prot:12:3 │ 12 │ DUT.a := a; - │ ^^^^^^^^^^^ Thread 0 (`multiple_assign`) attempted conflicting assignment to 'a': current=2, new=1 + │ ^^^^^^^^^^^ @1 Thread 0 (`multiple_assign`) attempted conflicting assignment to 'a': current=2, new=1 -error: Thread 1 (`multiple_assign`) attempted conflicting assignment to 'a': current=1, new=2 +error: @1 Thread 1 (`multiple_assign`) attempted conflicting assignment to 'a': current=1, new=2 ┌─ tests/identities/identity_d2/identity_d2.prot:9:3 │ 9 │ DUT.a := a; - │ ^^^^^^^^^^^ Thread 1 (`multiple_assign`) attempted conflicting assignment to 'a': current=1, new=2 + │ ^^^^^^^^^^^ @1 Thread 1 (`multiple_assign`) attempted conflicting assignment to 'a': current=1, new=2 Trace 0 execution failed. ---CODE---