diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index de6ab4ea..8a1d3111 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -36,6 +36,8 @@ jobs: run: runt runt/graph_interp - name: Run Runt tests for monitor run: runt runt/monitor + - name: Run Runt tests for bi + run: runt runt/bi test-freshness: name: Check Generated Runt Configs are Fresh diff --git a/.gitignore b/.gitignore index 20fbc471..6d40fff4 100644 --- a/.gitignore +++ b/.gitignore @@ -36,3 +36,4 @@ scripts/_catalog_gen.py !tests/fpga-debugging/axis-async-fifo-c4/*.png /*.fst +scripts/__pycache__/ diff --git a/justfile b/justfile index 264bdc23..ebc8eceb 100644 --- a/justfile +++ b/justfile @@ -1,8 +1,9 @@ # Runs the Runt snapshot suites that together cover every test runt: - cargo build --offline --package protocols-interp --package protocols-monitor --package graph-interp + cargo build --offline --package protocols-interp --package protocols-monitor --package graph-interp --package bi runt --max-futures 1 runt/interp runt --max-futures 1 runt/monitor + runt --max-futures 1 runt/bi runt --max-futures 1 runt/graph_interp runt --max-futures 1 runt/waveform diff --git a/runt/bi/runt.toml b/runt/bi/runt.toml new file mode 100644 index 00000000..bfa4e6d3 --- /dev/null +++ b/runt/bi/runt.toml @@ -0,0 +1,19 @@ +ver = "0.4.1" + +[[tests]] +name = "bi.tests_fpga_debugging_axi_lite_s1_s1_buggy.s1_buggy_bi" +paths = [ + "../../tests/fpga-debugging/axi-lite-s1/s1_buggy.prot", +] +expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects" +expect_name = "s1_buggy.bi.expect" +cmd = "cd ../.. && target/debug/bi --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot --wave tests/fpga-debugging/axi-lite-s1/s1_buggy_interp.fst --instances dut:WriteSubordinate --show-steps --include-in-progress 2>/dev/null" + +[[tests]] +name = "bi.tests_fpga_debugging_axi_lite_s1_s1_fixed.s1_fixed_bi" +paths = [ + "../../tests/fpga-debugging/axi-lite-s1/s1_fixed.prot", +] +expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects" +expect_name = "s1_fixed.bi.expect" +cmd = "cd ../.. && target/debug/bi --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed.prot --wave tests/fpga-debugging/axi-lite-s1/s1_fixed_interp.fst --instances dut:WriteSubordinate --show-steps 2>/dev/null" diff --git a/runt/interp/runt.toml b/runt/interp/runt.toml index 23b631a7..13a0223e 100644 --- a/runt/interp/runt.toml +++ b/runt/interp/runt.toml @@ -495,6 +495,24 @@ expect_dir = "../../tests/fifo/expects" expect_name = "push_pop_loop_not_empty.interp.expect" cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fifo/push_pop_loop_not_empty.tx --verilog tests/fifo/bsg_mem_1rw_sync.v tests/fifo/bsg_mem_1rw_sync_synth.v tests/fifo/bsg_circular_ptr.v tests/fifo/bsg_fifo_1rw_large.v tests/fifo/fifo_wrapper.v --protocol tests/fifo/fifo_bounded_loop.prot --module fifo_wrapper 2>&1" +[[tests]] +name = "interp.tests_fpga_debugging_axi_lite_s1_s1_buggy.s1_buggy_interp" +paths = [ + "../../tests/fpga-debugging/axi-lite-s1/s1_buggy.tx", +] +expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects" +expect_name = "s1_buggy.interp.expect" +cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axi-lite-s1/s1_buggy.tx --verilog tests/fpga-debugging/axi-lite-s1/s1_buggy.v --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot --module xlnxdemo --max-steps 300 2>&1" + +[[tests]] +name = "interp.tests_fpga_debugging_axi_lite_s1_s1_fixed.s1_fixed_interp" +paths = [ + "../../tests/fpga-debugging/axi-lite-s1/s1_fixed.tx", +] +expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects" +expect_name = "s1_fixed.interp.expect" +cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fpga-debugging/axi-lite-s1/s1_fixed.tx --verilog tests/fpga-debugging/axi-lite-s1/s1_fixed.v --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed.prot --module xlnxdemo --max-steps 300 2>&1" + [[tests]] name = "interp.tests_identities_dual_identity_d0_dual_identity_d0_combdep.dual_identity_d0_combdep_interp" paths = [ diff --git a/runt/monitor/runt.toml b/runt/monitor/runt.toml index aee94652..14513f8c 100644 --- a/runt/monitor/runt.toml +++ b/runt/monitor/runt.toml @@ -1240,7 +1240,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects" expect_name = "s1_buggy.monitor.expect" -cmd = "cd ../.. && target/debug/protocols-monitor --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot --wave tests/fpga-debugging/axi-lite-s1/s1_buggy_workload2.vcd --instances TOP.testbench.UUT:WriteSubordinate TOP.testbench.UUT:ReadSubordinate --sample-posedge TOP.testbench.UUT.S_AXI_ACLK --show-waveform-time --time-unit ns --include-idle 2>/dev/null" +cmd = "cd ../.. && target/debug/protocols-monitor --protocol tests/fpga-debugging/axi-lite-s1/s1_buggy.prot --wave tests/fpga-debugging/axi-lite-s1/s1_buggy_workload2.vcd --instances TOP.testbench.UUT:WriteSubordinate --sample-posedge TOP.testbench.UUT.S_AXI_ACLK --show-waveform-time --time-unit ns --include-idle 2>/dev/null" [[tests]] name = "monitor.tests_fpga_debugging_axi_lite_s1_s1_buggy_workload_1.s1_buggy_workload_1_monitor" @@ -1258,7 +1258,7 @@ paths = [ ] expect_dir = "../../tests/fpga-debugging/axi-lite-s1/expects" expect_name = "s1_fixed.monitor.expect" -cmd = "cd ../.. && target/debug/protocols-monitor --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed.prot --wave tests/fpga-debugging/axi-lite-s1/s1_fixed_workload2.vcd --instances TOP.testbench.UUT:WriteSubordinate TOP.testbench.UUT:ReadSubordinate --sample-posedge TOP.testbench.UUT.S_AXI_ACLK --show-waveform-time --time-unit ns --include-idle 2>/dev/null" +cmd = "cd ../.. && target/debug/protocols-monitor --protocol tests/fpga-debugging/axi-lite-s1/s1_fixed.prot --wave tests/fpga-debugging/axi-lite-s1/s1_fixed_workload2.vcd --instances TOP.testbench.UUT:WriteSubordinate --sample-posedge TOP.testbench.UUT.S_AXI_ACLK --show-waveform-time --time-unit ns --include-idle 2>/dev/null" [[tests]] name = "monitor.tests_fpga_debugging_axi_lite_s1_s1_fixed_workload_1.s1_fixed_workload_1_monitor" diff --git a/scripts/generate_runt_configs.py b/scripts/generate_runt_configs.py index 011e7293..d9695ea9 100644 --- a/scripts/generate_runt_configs.py +++ b/scripts/generate_runt_configs.py @@ -62,6 +62,25 @@ def load_monitor_cases() -> list[dict]: return out +def load_bi_cases() -> list[dict]: + """Same as load_monitor_cases but for the bi cases""" + out = [] + for case_id, c in test_catalog.BI_CASES.items(): + out.append( + { + "id": case_id, + "path": c["protocol"], + "wave": c.get("wave"), + "instances": c.get("instances", ()), + "max_steps": c.get("max_steps"), + "timeout_secs": c.get("timeout_secs"), + "extra_args": c.get("extra_args", ()), + "expected": c["expect"], + } + ) + return out + + # helper function to escape globs in places def runt_glob_literal(path: str) -> str: return path.replace("[", "[[]").replace("*", "[*]").replace("?", "[?]") @@ -195,6 +214,19 @@ def monitor_runt_command(case: dict) -> list[tuple[str, str]]: return [("", repo_root_command(cmd))] +# Same as `monitor_runt_command` above but for BI test cases +def bi_runt_command(case: dict) -> list[tuple[str, str]]: + cmd = [*binary_prefix("bi"), "--protocol", case["path"]] + if case["wave"]: + cmd += ["--wave", case["wave"]] + if case["instances"]: + cmd += ["--instances", *case["instances"]] + cmd += case["extra_args"] + if case["timeout_secs"] is not None: + cmd = timeout_cmd(case["timeout_secs"], cmd) + return [("", repo_root_command(cmd))] + + def waveform_runt_command(case: dict) -> list[tuple[str, str]]: ast_cmd = [ *binary_prefix("protocols-interp"), @@ -226,6 +258,7 @@ def waveform_runt_command(case: dict) -> list[tuple[str, str]]: "interp": interp_runt_command, "graph_interp": graph_interp_runt_command, "monitor": monitor_runt_command, + "bi": bi_runt_command, "waveform": waveform_runt_command, } @@ -330,11 +363,13 @@ def write_runt_toml(output_dir: Path, suites) -> None: def generate_runt_configs() -> None: tx = load_tx_cases() mon = load_monitor_cases() + bi = load_bi_cases() # Each suite maps a name to (runner, cases). interp + monitor + graph_interp # together cover every test. suite_specs = { "interp": ("interp", tx), "monitor": ("monitor", mon), + "bi": ("bi", bi), "graph_interp": ("graph_interp", graph_interp_cases(tx)), "waveform": ("waveform", waveform_cases(tx)), } diff --git a/scripts/test_catalog.py b/scripts/test_catalog.py index ff56b960..ee069389 100644 --- a/scripts/test_catalog.py +++ b/scripts/test_catalog.py @@ -1,7 +1,7 @@ # Checked-in test catalog. Hand-maintained source of truth. # Consumed by scripts/generate_runt_configs.py and scripts/benchmark_monitor.py. # -# TX_CASES are keyed by their .tx path. MONITOR_CASES are keyed by a unique id +# TX_CASES are keyed by their .tx path. MONITOR_CASES & BI_CASES are both keyed by a unique id TX_CASES = { "examples/picorv32/unsigned_mul.tx": { @@ -349,6 +349,20 @@ "top": "fifo_wrapper", "expect": "pass", }, + "tests/fpga-debugging/axi-lite-s1/s1_buggy.tx": { + "protocol": "tests/fpga-debugging/axi-lite-s1/s1_buggy.prot", + "verilog": ("tests/fpga-debugging/axi-lite-s1/s1_buggy.v",), + "top": "xlnxdemo", + "max_steps": 300, + "expect": "assignment_conflict", + }, + "tests/fpga-debugging/axi-lite-s1/s1_fixed.tx": { + "protocol": "tests/fpga-debugging/axi-lite-s1/s1_fixed.prot", + "verilog": ("tests/fpga-debugging/axi-lite-s1/s1_fixed.v",), + "top": "xlnxdemo", + "max_steps": 300, + "expect": "pass", + }, "tests/identities/dual_identity_d0/dual_identity_d0_combdep.tx": { "protocol": "tests/identities/dual_identity_d0/dual_identity_d0.prot", "verilog": ("tests/identities/dual_identity_d0/dual_identity_d0.v",), @@ -660,10 +674,7 @@ "tests.fpga-debugging.axi-lite-s1.s1_buggy": { "protocol": "tests/fpga-debugging/axi-lite-s1/s1_buggy.prot", "wave": "tests/fpga-debugging/axi-lite-s1/s1_buggy_workload2.vcd", - "instances": ( - "TOP.testbench.UUT:WriteSubordinate", - "TOP.testbench.UUT:ReadSubordinate", - ), + "instances": ("TOP.testbench.UUT:WriteSubordinate",), "expect": None, "extra_args": ( "--sample-posedge", @@ -694,11 +705,11 @@ "tests.fpga-debugging.axi-lite-s1.s1_fixed": { "protocol": "tests/fpga-debugging/axi-lite-s1/s1_fixed.prot", "wave": "tests/fpga-debugging/axi-lite-s1/s1_fixed_workload2.vcd", - "instances": ( - "TOP.testbench.UUT:WriteSubordinate", - "TOP.testbench.UUT:ReadSubordinate", - ), - "expect": "pass", + "instances": ("TOP.testbench.UUT:WriteSubordinate",), + # The monitor doesn't work for this protocol due to a known bug + # (inability to handle multiple assignments to the same port within the same cycle). + # See https://github.com/cucapra/protocols/issues/214 + "expect": None, "extra_args": ( "--sample-posedge", "TOP.testbench.UUT.S_AXI_ACLK", @@ -1099,3 +1110,24 @@ def _antmicro_case(stem): for stem in ANTMICRO_TRACE_STEMS } ) + +# The filepath supplied to the `wave` field are .fst files produced by the interpreter. +BI_CASES = { + "tests.fpga-debugging.axi-lite-s1.s1_buggy.bi": { + "protocol": "tests/fpga-debugging/axi-lite-s1/s1_buggy.prot", + "wave": "tests/fpga-debugging/axi-lite-s1/s1_buggy_interp.fst", + "instances": ("dut:WriteSubordinate",), + # `--include-in-progress` makes `bi` report the two writes that + # started but whose responses never completed, surfacing the + # lost-write-response bug on the monitoring side. + "expect": None, + "extra_args": ("--show-steps", "--include-in-progress"), + }, + "tests.fpga-debugging.axi-lite-s1.s1_fixed.bi": { + "protocol": "tests/fpga-debugging/axi-lite-s1/s1_fixed.prot", + "wave": "tests/fpga-debugging/axi-lite-s1/s1_fixed_interp.fst", + "instances": ("dut:WriteSubordinate",), + "expect": None, + "extra_args": ("--show-steps",), + }, +} diff --git a/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.bi.expect b/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.bi.expect new file mode 100644 index 00000000..2e3bfd1b --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.bi.expect @@ -0,0 +1,13 @@ +// trace 0 +trace { + reset(); [0] + write(8, 7, X, 0); [7 .. ] + write(4, 42, X, 4); [1 .. ] +} + +// trace 1 +trace { + reset(); [0] + write(8, 7, X, 0); [7 .. ] + write(4, 42, X, 3); [2 .. ] +} diff --git a/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.interp.expect b/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.interp.expect new file mode 100644 index 00000000..6bc54dd6 --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/expects/s1_buggy.interp.expect @@ -0,0 +1,15 @@ +error: Thread 1 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=1, new=0 + ┌─ tests/fpga-debugging/axi-lite-s1/s1_buggy.prot:83:5 + │ +83 │ DUT.S_AXI_BREADY := 1'b0; + │ ^^^^^^^^^^^^^^^^^^^^^^^^^ Thread 1 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=1, new=0 + +error: Thread 2 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=0, new=1 + ┌─ tests/fpga-debugging/axi-lite-s1/s1_buggy.prot:95:5 + │ +95 │ DUT.S_AXI_BREADY := 1'b1; + │ ^^^^^^^^^^^^^^^^^^^^^^^^^ Thread 2 (`write`) attempted conflicting assignment to 'S_AXI_BREADY': current=0, new=1 + +Trace 0 execution failed. +---CODE--- +101 diff --git a/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.bi.expect b/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.bi.expect new file mode 100644 index 00000000..d2661524 --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.bi.expect @@ -0,0 +1,43 @@ +// trace 0 +trace { + reset(); [0] + write(4, 42, 0, 4); [1 .. 12] + write(8, 7, 0, 0); [7 .. 14] +} + +// trace 1 +trace { + reset(); [0] + write(4, 42, 0, 4); [1 .. 12] + write(8, 7, 0, 0); [7 .. 14] +} + +// trace 2 +trace { + reset(); [0] + write(4, 42, 0, 4); [1 .. 12] + write(8, 7, 0, 0); [7 .. 14] +} + +// trace 3 +trace { + reset(); [0] + write(4, 42, 0, 4); [1 .. 12] + write(8, 7, 0, 0); [7 .. 14] +} + +// trace 4 +trace { + reset(); [0] + write(4, 42, 0, 4); [1 .. 12] + write(8, 7, 0, 0); [7 .. 14] +} + +// trace 5 +trace { + reset(); [0] + write(4, 42, 0, 4); [1 .. 12] + write(8, 7, 0, 0); [7 .. 14] +} +---CODE--- +1 diff --git a/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.interp.expect b/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.interp.expect new file mode 100644 index 00000000..f5f6cb49 --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.interp.expect @@ -0,0 +1 @@ +Trace 0 executed successfully! diff --git a/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.monitor.expect b/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.monitor.expect index aabbc981..6503598b 100644 --- a/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.monitor.expect +++ b/tests/fpga-debugging/axi-lite-s1/expects/s1_fixed.monitor.expect @@ -1,8 +1,2 @@ -// trace 0 -trace { - WriteSubordinate::idle(); // [time: 0ns -> 25ns] - ReadSubordinate::idle(); // [time: 0ns -> 25ns] - WriteSubordinate::write(64, 2147483648, 0, 0); // [time: 25ns -> 100ns] - ReadSubordinate::read_v2(68, 0, 1); // [time: 50ns -> 125ns] - ReadSubordinate::idle(); // [time: 125ns -> 150ns] -} +---CODE--- +1 diff --git a/tests/fpga-debugging/axi-lite-s1/s1_buggy.prot b/tests/fpga-debugging/axi-lite-s1/s1_buggy.prot index 2063b7e6..e10244d0 100644 --- a/tests/fpga-debugging/axi-lite-s1/s1_buggy.prot +++ b/tests/fpga-debugging/axi-lite-s1/s1_buggy.prot @@ -1,16 +1,7 @@ -struct ReadSubordinate { - // Read address channel - in S_AXI_ARVALID: u1, - in S_AXI_ARADDR: u7, - out S_AXI_ARREADY: u1, - - // Read data channel - in S_AXI_RREADY: u1, - out S_AXI_RVALID: u1, - out S_AXI_RDATA: u32, -} - struct WriteSubordinate { + // Active-low reset + in S_AXI_ARESETN: u1, + // Write address channel in S_AXI_AWVALID: u1, in S_AXI_AWADDR: u7, @@ -27,11 +18,32 @@ struct WriteSubordinate { out S_AXI_BRESP: u2, } -// Note: this is still WIP (this is simpler than the protocol we discussed -// yesterday for ease of debugging for now) +prot reset() { + // Reset is active-low + DUT.S_AXI_ARESETN := 1'b0; + + // Set valid = 0 for the write data / write address channels + DUT.S_AXI_AWVALID := 1'b0; + DUT.S_AXI_WVALID := 1'b0; + + // Set ready = 0 for write response + DUT.S_AXI_BREADY := 1'b0; + + step(); +} + +// Write transaction where the manager waits `n` cycles before setting AWVALID = 1. +// After the subordinate indicates `BVALID = 1`, the manager stalls the response channel +// for `n` cycles before setting BREADY = 1. +// The `resp` argument is a 2-bit pattern containing the subordinate's response +// to the write request (indicating whether the transaction succeeded). prot write(addr: u7, data: u32, resp: u2, n: uint) { + // Reset is active-low + DUT.S_AXI_ARESETN := 1'b1; + + // Wait for `n` cycles before starting write request + DUT.S_AXI_AWVALID := 1'b0; repeat n iterations { - DUT.S_AXI_AWVALID := 1'b0; step(); } DUT.S_AXI_AWVALID := 1'b1; @@ -40,137 +52,64 @@ prot write(addr: u7, data: u32, resp: u2, n: uint) { DUT.S_AXI_WVALID := 1'b1; DUT.S_AXI_WDATA := data; - // technically this should be `while !AWREADY && !WREADY { step() }` + // Technically this should be `while !AWREADY && !WREADY { step() }`, // but our DSL doesn't have `&&`. Without loss of generality, // we wait for AWREADY to become 1 while !(DUT.S_AXI_AWREADY == 1'b1) { step(); } - // Assuming AWREADY & WREADY become 1 together + // Here we're assuming AWREADY & WREADY become 1 together // (this is allowed in the AXI spec and the DUT exhibits this behavior) assert_eq(DUT.S_AXI_WREADY, 1'b1); step(); - // Remove constraints on AWVALID and WVALID + // The data transfer for the write address + write data is done, + // so we set these channels to `DontCare` DUT.S_AXI_AWVALID := X; DUT.S_AXI_WVALID := X; - - // Wait for BVALID to become 1 + DUT.S_AXI_AWADDR := X; + DUT.S_AXI_WDATA := X; + + // We use `fork` to indicate that another transaction can begin concurrently + // According to B1.1.4 of the AXI-Lite spec, a manager can send a + // new write request while awaiting a response for a previous request, + // but it is the subordinate's responsibility to acknowledge these + // requests in the order they were issued. + fork(); + + // Wait BVALID to become 1 + // Before BVALID becomes 1, we have to keep BVALID = 0 + DUT.S_AXI_BREADY := 1'b0; while !(DUT.S_AXI_BVALID == 1'b1) { step(); } // BVALID is now 1 - // Wait for some no. of cycles before BREADY becomes 1 + // Wait `n` cycles before asserting BREADY repeat n iterations { step(); // BVALID must remain stable after it becomes 1 assert_eq(DUT.S_AXI_BVALID, 1'b1); } + // Assert BREADY and check that the response is transffered DUT.S_AXI_BREADY := 1'b1; assert_eq(DUT.S_AXI_BRESP, resp); step(); -} - -#[idle] -prot idle() { - DUT.S_AXI_ARVALID := 1'b0; - DUT.S_AXI_ARADDR := X; - DUT.S_AXI_RREADY := 1'b0; + // Set BREADY back to 0 + // (transaction is over so there is no data on the response channel) + DUT.S_AXI_BREADY := 1'b0; step(); } #[idle] prot idle() { + // Reset is active-low, so we set reset = 1 here + // to indicate that the DUT is *not* reset during an `idle` transaction + DUT.S_AXI_ARESETN := 1'b1; DUT.S_AXI_AWVALID := 1'b0; DUT.S_AXI_AWADDR := X; DUT.S_AXI_WVALID := 1'b0; DUT.S_AXI_WDATA := X; step(); } - -// RREADY is asserted before RVALID -// (This is allowed in section A2.3.2.2 of the AXI spec) -prot read_v1(addr: u7, data: u32) { - DUT.S_AXI_ARVALID := 1'b1; - DUT.S_AXI_ARADDR := addr; - - // Wait for ARREADY to become 1 - while !(DUT.S_AXI_ARREADY == 1'b1) { - step(); - } - // ARREADY is now 1 - - step(); - - // While we are waiting for RREADY to become 1, - // another read address request cannot arrive - // (i.e. ARREADY has to remain 0). That is, we have to acknowledge - // the read data before another read address request can arrive. - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - - // Once ARREADY is de-asserted, ARVALID is allowed to be any value - DUT.S_AXI_ARVALID := X; - - // Manager sets RREADY to 1 to begin transfer on read data channel - DUT.S_AXI_RREADY := 1'b1; - - // Wait for RVALID to become 1 - // AXI spec says that ARVALID & ARREADY must both be 1 - // before RVALID can be asserted (A2.3.2.2) - while !(DUT.S_AXI_RVALID == 1'b1) { - step(); - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - } - assert_eq(DUT.S_AXI_RDATA, data); - step(); -} - -// RVALID is asserted before RREADY -// (This is allowed in section A2.3.2.2 of the AXI spec) -prot read_v2(addr: u7, data: u32, n: uint) { - DUT.S_AXI_ARVALID := 1'b1; - DUT.S_AXI_ARADDR := addr; - - // Wait for ARREADY to become 1 - while !(DUT.S_AXI_ARREADY == 1'b1) { - step(); - } - // ARREADY is now 1 - - step(); - - // Wait for RVALID to become 1 - // AXI spec says that ARVALID & ARREADY must both be 1 - // before RVALID can be asserted (A2.3.2.2) - while !(DUT.S_AXI_RVALID == 1'b1) { - step(); - } - // RVALID is now 1 - - // While we are waiting for RREADY to become 1, - // another read address request cannot arrive - // (i.e. ARREADY has to remain 0). That is, we have to acknowledge - // the read data before another read address request can arrive. - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - - // Once ARREADY is de-asserted, ARVALID is allowed to be any value - DUT.S_AXI_ARVALID := X; - - // Wait until RREADY becomes 1 - repeat n iterations { - DUT.S_AXI_RREADY := 1'b0; - // Check that RVALID remains stable - assert_eq(DUT.S_AXI_RVALID, 1'b1); - step(); - } - // Check that ARREADY remains 0 (i.e. no conflicting read address request) - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - - // Perform data transfer on the read data channel - DUT.S_AXI_RREADY := 1'b1; - assert_eq(DUT.S_AXI_RDATA, data); - - step(); -} diff --git a/tests/fpga-debugging/axi-lite-s1/s1_buggy.tx b/tests/fpga-debugging/axi-lite-s1/s1_buggy.tx new file mode 100644 index 00000000..a60a148d --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/s1_buggy.tx @@ -0,0 +1,13 @@ +// In the first write transaction, the manager waits 4 cycles before issuing a response +// (last argument to the `write` transaction). +// The second write transaction is pipelined and begins +// when the first `write` transaction calls `fork`. +// The buggy DUT only acknowledges the first write request +// and ignores the second one. +// Our interpreter emits an error message saying +// there are conflicting assignments to `BREADY`. +trace { + reset(); + write(4, 42, 0, 4); + write(8, 7, 0, 0); +} diff --git a/tests/fpga-debugging/axi-lite-s1/s1_buggy_interp.fst b/tests/fpga-debugging/axi-lite-s1/s1_buggy_interp.fst new file mode 100644 index 00000000..c46cd3af Binary files /dev/null and b/tests/fpga-debugging/axi-lite-s1/s1_buggy_interp.fst differ diff --git a/tests/fpga-debugging/axi-lite-s1/s1_fixed.prot b/tests/fpga-debugging/axi-lite-s1/s1_fixed.prot index 2063b7e6..e10244d0 100644 --- a/tests/fpga-debugging/axi-lite-s1/s1_fixed.prot +++ b/tests/fpga-debugging/axi-lite-s1/s1_fixed.prot @@ -1,16 +1,7 @@ -struct ReadSubordinate { - // Read address channel - in S_AXI_ARVALID: u1, - in S_AXI_ARADDR: u7, - out S_AXI_ARREADY: u1, - - // Read data channel - in S_AXI_RREADY: u1, - out S_AXI_RVALID: u1, - out S_AXI_RDATA: u32, -} - struct WriteSubordinate { + // Active-low reset + in S_AXI_ARESETN: u1, + // Write address channel in S_AXI_AWVALID: u1, in S_AXI_AWADDR: u7, @@ -27,11 +18,32 @@ struct WriteSubordinate { out S_AXI_BRESP: u2, } -// Note: this is still WIP (this is simpler than the protocol we discussed -// yesterday for ease of debugging for now) +prot reset() { + // Reset is active-low + DUT.S_AXI_ARESETN := 1'b0; + + // Set valid = 0 for the write data / write address channels + DUT.S_AXI_AWVALID := 1'b0; + DUT.S_AXI_WVALID := 1'b0; + + // Set ready = 0 for write response + DUT.S_AXI_BREADY := 1'b0; + + step(); +} + +// Write transaction where the manager waits `n` cycles before setting AWVALID = 1. +// After the subordinate indicates `BVALID = 1`, the manager stalls the response channel +// for `n` cycles before setting BREADY = 1. +// The `resp` argument is a 2-bit pattern containing the subordinate's response +// to the write request (indicating whether the transaction succeeded). prot write(addr: u7, data: u32, resp: u2, n: uint) { + // Reset is active-low + DUT.S_AXI_ARESETN := 1'b1; + + // Wait for `n` cycles before starting write request + DUT.S_AXI_AWVALID := 1'b0; repeat n iterations { - DUT.S_AXI_AWVALID := 1'b0; step(); } DUT.S_AXI_AWVALID := 1'b1; @@ -40,137 +52,64 @@ prot write(addr: u7, data: u32, resp: u2, n: uint) { DUT.S_AXI_WVALID := 1'b1; DUT.S_AXI_WDATA := data; - // technically this should be `while !AWREADY && !WREADY { step() }` + // Technically this should be `while !AWREADY && !WREADY { step() }`, // but our DSL doesn't have `&&`. Without loss of generality, // we wait for AWREADY to become 1 while !(DUT.S_AXI_AWREADY == 1'b1) { step(); } - // Assuming AWREADY & WREADY become 1 together + // Here we're assuming AWREADY & WREADY become 1 together // (this is allowed in the AXI spec and the DUT exhibits this behavior) assert_eq(DUT.S_AXI_WREADY, 1'b1); step(); - // Remove constraints on AWVALID and WVALID + // The data transfer for the write address + write data is done, + // so we set these channels to `DontCare` DUT.S_AXI_AWVALID := X; DUT.S_AXI_WVALID := X; - - // Wait for BVALID to become 1 + DUT.S_AXI_AWADDR := X; + DUT.S_AXI_WDATA := X; + + // We use `fork` to indicate that another transaction can begin concurrently + // According to B1.1.4 of the AXI-Lite spec, a manager can send a + // new write request while awaiting a response for a previous request, + // but it is the subordinate's responsibility to acknowledge these + // requests in the order they were issued. + fork(); + + // Wait BVALID to become 1 + // Before BVALID becomes 1, we have to keep BVALID = 0 + DUT.S_AXI_BREADY := 1'b0; while !(DUT.S_AXI_BVALID == 1'b1) { step(); } // BVALID is now 1 - // Wait for some no. of cycles before BREADY becomes 1 + // Wait `n` cycles before asserting BREADY repeat n iterations { step(); // BVALID must remain stable after it becomes 1 assert_eq(DUT.S_AXI_BVALID, 1'b1); } + // Assert BREADY and check that the response is transffered DUT.S_AXI_BREADY := 1'b1; assert_eq(DUT.S_AXI_BRESP, resp); step(); -} - -#[idle] -prot idle() { - DUT.S_AXI_ARVALID := 1'b0; - DUT.S_AXI_ARADDR := X; - DUT.S_AXI_RREADY := 1'b0; + // Set BREADY back to 0 + // (transaction is over so there is no data on the response channel) + DUT.S_AXI_BREADY := 1'b0; step(); } #[idle] prot idle() { + // Reset is active-low, so we set reset = 1 here + // to indicate that the DUT is *not* reset during an `idle` transaction + DUT.S_AXI_ARESETN := 1'b1; DUT.S_AXI_AWVALID := 1'b0; DUT.S_AXI_AWADDR := X; DUT.S_AXI_WVALID := 1'b0; DUT.S_AXI_WDATA := X; step(); } - -// RREADY is asserted before RVALID -// (This is allowed in section A2.3.2.2 of the AXI spec) -prot read_v1(addr: u7, data: u32) { - DUT.S_AXI_ARVALID := 1'b1; - DUT.S_AXI_ARADDR := addr; - - // Wait for ARREADY to become 1 - while !(DUT.S_AXI_ARREADY == 1'b1) { - step(); - } - // ARREADY is now 1 - - step(); - - // While we are waiting for RREADY to become 1, - // another read address request cannot arrive - // (i.e. ARREADY has to remain 0). That is, we have to acknowledge - // the read data before another read address request can arrive. - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - - // Once ARREADY is de-asserted, ARVALID is allowed to be any value - DUT.S_AXI_ARVALID := X; - - // Manager sets RREADY to 1 to begin transfer on read data channel - DUT.S_AXI_RREADY := 1'b1; - - // Wait for RVALID to become 1 - // AXI spec says that ARVALID & ARREADY must both be 1 - // before RVALID can be asserted (A2.3.2.2) - while !(DUT.S_AXI_RVALID == 1'b1) { - step(); - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - } - assert_eq(DUT.S_AXI_RDATA, data); - step(); -} - -// RVALID is asserted before RREADY -// (This is allowed in section A2.3.2.2 of the AXI spec) -prot read_v2(addr: u7, data: u32, n: uint) { - DUT.S_AXI_ARVALID := 1'b1; - DUT.S_AXI_ARADDR := addr; - - // Wait for ARREADY to become 1 - while !(DUT.S_AXI_ARREADY == 1'b1) { - step(); - } - // ARREADY is now 1 - - step(); - - // Wait for RVALID to become 1 - // AXI spec says that ARVALID & ARREADY must both be 1 - // before RVALID can be asserted (A2.3.2.2) - while !(DUT.S_AXI_RVALID == 1'b1) { - step(); - } - // RVALID is now 1 - - // While we are waiting for RREADY to become 1, - // another read address request cannot arrive - // (i.e. ARREADY has to remain 0). That is, we have to acknowledge - // the read data before another read address request can arrive. - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - - // Once ARREADY is de-asserted, ARVALID is allowed to be any value - DUT.S_AXI_ARVALID := X; - - // Wait until RREADY becomes 1 - repeat n iterations { - DUT.S_AXI_RREADY := 1'b0; - // Check that RVALID remains stable - assert_eq(DUT.S_AXI_RVALID, 1'b1); - step(); - } - // Check that ARREADY remains 0 (i.e. no conflicting read address request) - assert_eq(DUT.S_AXI_ARREADY, 1'b0); - - // Perform data transfer on the read data channel - DUT.S_AXI_RREADY := 1'b1; - assert_eq(DUT.S_AXI_RDATA, data); - - step(); -} diff --git a/tests/fpga-debugging/axi-lite-s1/s1_fixed.tx b/tests/fpga-debugging/axi-lite-s1/s1_fixed.tx new file mode 100644 index 00000000..1edf625a --- /dev/null +++ b/tests/fpga-debugging/axi-lite-s1/s1_fixed.tx @@ -0,0 +1,9 @@ +// This is the same transaction trace as s1_buggy.tx, +// but the DUT is fixed, so it doesn't accept the second +// write transaction until the first one is acknowledged. +// Our interpreter executes this list of transcations successfully. +trace { + reset(); + write(4, 42, 0, 4); + write(8, 7, 0, 0); +} diff --git a/tests/fpga-debugging/axi-lite-s1/s1_fixed_interp.fst b/tests/fpga-debugging/axi-lite-s1/s1_fixed_interp.fst new file mode 100644 index 00000000..2f07ed95 Binary files /dev/null and b/tests/fpga-debugging/axi-lite-s1/s1_fixed_interp.fst differ