Round-trip Testing

.github/workflows/test.yml

@@ -33,6 +33,15 @@ jobs:
     - name: Run Turnt tests for monitor
       run: turnt --env monitor $(find . -type f -name '*.prot')
 
+  roundtrip:
+    name: Roundtrip
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/actions/setup-test-environment
+      - name: Run Turnt roundtrip tests
+        run: turnt --env roundtrip $(find . -type f -name '*.tx') --diff
+
   msrv:
     name: Check Minimum Rust Version for protocols library
     runs-on: ubuntu-24.04

examples/picorv32/unsigned_mul.rt

@@ -0,0 +1,22 @@
+trace_block: 0
+trace_result: PASS
+matched_monitor_trace_index: 0
+interpreter_trace:
+trace {
+    pcpi_mul_reset();
+    pcpi_mul(1, 1, 1);
+    pcpi_mul(1, 100, 100);
+    pcpi_mul(100, 1, 100);
+    pcpi_mul(33554483, 200, 2415929304);
+}
+
+parsed_monitor_trace_candidates:
+candidate_monitor_trace: 0
+trace {
+    pcpi_mul_reset();
+    pcpi_mul(1, 1, 1);
+    pcpi_mul(1, 100, 100);
+    pcpi_mul(100, 1, 100);
+    pcpi_mul(33554483, 200, 2415929304);
+}
+

examples/serv/serv_regfile.rt

@@ -0,0 +1,16 @@
+trace_block: 0
+trace_result: PASS
+matched_monitor_trace_index: 0
+interpreter_trace:
+trace {
+    read_write(0, 0, 0, 0, 1, 5, 3735928559);
+    read_write(5, 3735928559, 0, 0, 0, 0, 0);
+}
+
+parsed_monitor_trace_candidates:
+candidate_monitor_trace: 0
+trace {
+    read_write(0, 0, 0, 0, 1, 5, 3735928559);
+    read_write(5, 3735928559, 0, 0, 0, 0, 0);
+}
+

examples/tinyaes128/aes128.rt

@@ -0,0 +1,16 @@
+trace_block: 0
+trace_result: PASS
+matched_monitor_trace_index: 0
+interpreter_trace:
+trace {
+    aes128(5233100606242806050955395731361295, 88962710306127702866241727433142015, 140591190147677442632770771134392354138);
+    aes128(0, 0, 136792598789324718765670228683992083246);
+}
+
+parsed_monitor_trace_candidates:
+candidate_monitor_trace: 0
+trace {
+    aes128(5233100606242806050955395731361295, 88962710306127702866241727433142015, 140591190147677442632770771134392354138);
+    aes128(0, 0, 136792598789324718765670228683992083246);
+}
+

examples/turnt.toml

@@ -1,2 +1,7 @@
 [envs.interp]
 command = "cargo run --package protocols-interp -- --color never --transactions {filename} {args}"
+
+[envs.roundtrip]
+command = "uv run ../scripts/roundtrip_case.py {filename} {args}"
+binary = true
+output.rt = "-"

interp/src/main.rs

@@ -54,6 +54,11 @@ struct Cli {
     /// of cycles specified with this option.
     #[arg(long)]
     max_steps: Option<u32>,
+
+    /// Mark this test as allowed to fail (ignored by interpreter, used only
+    /// round-trip test harness)
+    #[arg(long)]
+    allow_round_trip_failure: bool,
 }
 
 /// Examples (enables all tracing logs):

justfile

@@ -6,6 +6,10 @@ interp:
 monitor:
   turnt --env monitor $(find . -type f -name '*.prot') 
 
+# Run roundtrip checks (interp -> fst -> monitor) for all transactions
+roundtrip:
+  turnt --env roundtrip $(find . -type f -name '*.tx')
+
 # Run Turnt tests for the monitor based on the Brave New World artifacts
 bnw_monitor:
   turnt --env monitor $(find monitor/tests/fpga-debugging -type f -name '*.prot')   

protocols/src/scheduler.rs

@@ -403,6 +403,9 @@ impl<'a> Scheduler<'a> {
             }
         }
 
+        // Emit one trailing empty cycle so all generated .fst files having timing information
+        self.evaluator.sim_step();
+
         // Emit diagnostics for all errors after execution is complete
         self.emit_all_diagnostics();
         self.results.clone()

protocols/tests/adders/adder_d0/add_combinational.rt

@@ -0,0 +1,13 @@
+trace_block: 0
+trace_result: FAIL
+failure_kind: monitor_error
+interpreter_trace:
+trace {
+    add_combinational(100, 200, 300);
+}
+
+monitor_error:
+Transaction `add_combinational_illegal_observation_in_conditional`, cycle 0: Unable to find value for b (symbol5) in args_mapping, which is { (symbol4) a: 100
+(symbol6) s: 300 }
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+

protocols/tests/adders/adder_d0/illegal_assignment.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d0/illegal_observation_assertion.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d0/illegal_observation_conditional.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d1/add_incorrect.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d1/add_incorrect_implicit.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d1/add_multitrace.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d1/both_threads_fail.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d1/both_threads_pass.rt

@@ -0,0 +1,15 @@
+trace_block: 0
+trace_result: FAIL
+failure_kind: monitor_error
+interpreter_trace:
+trace {
+    add(1, 2, 3);
+    add(4, 5, 9);
+}
+
+monitor_error:
+All schedulers failed: No transactions match the waveform for DUT `Adder`
+Failure at cycle 1: No transactions match the waveform in `.roundtrip_tmp/adders-adder_d1-both_threads_pass_0.fst`.
+Possible transactions: [add, add_fork_early, add_doesnt_end_in_step, add_incorrect, add_incorrect_implicit, wait_and_add]
+Error: Monitor failed
+

protocols/tests/adders/adder_d1/busy_wait_fail.rt

@@ -0,0 +1 @@
+SKIP: allowed to fail round trip

protocols/tests/adders/adder_d1/busy_wait_fail.tx

@@ -1,4 +1,4 @@
-// ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/busy_wait.prot
+// ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/busy_wait.prot --allow-round-trip-failure
 // RETURN: 101
 trace {
     add_busy_wait(1, 2, 2, 999); // Wrong output value, this transaction fails

protocols/tests/adders/adder_d1/busy_wait_pass.rt

@@ -0,0 +1 @@
+SKIP: allowed to fail round trip

protocols/tests/adders/adder_d1/busy_wait_pass.tx

@@ -1,4 +1,4 @@
-// ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/busy_wait.prot
+// ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/busy_wait.prot --allow-round-trip-failure
 trace {
     add_busy_wait(1, 2, 1, 3);  // Runs busy-waiting loop for 1 iteration
     add_busy_wait(4, 5, 3, 9);  // Runs busy-waiting loop for 3 iterations 

protocols/tests/adders/adder_d1/didnt_end_in_step.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d1/double_fork_error.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d1/first_fail_second_norun.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d1/first_thread_fails.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d1/fork_before_step_error.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d1/loop_with_assigns.rt

@@ -0,0 +1 @@
+SKIP: allowed to fail round trip

protocols/tests/adders/adder_d1/loop_with_assigns.tx

@@ -1,4 +1,4 @@
-// ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/loop_with_assigns.prot
+// ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/loop_with_assigns.prot --allow-round-trip-failure
 trace {
     loop_add(1, 2, 3, 3);   // assert 1+2=3 on each of 3 iterations
     loop_add(10, 20, 1, 30); // assert 10+20=30 on 1 iteration

protocols/tests/adders/adder_d1/nested_busy_wait.rt

@@ -0,0 +1 @@
+SKIP: allowed to fail round trip

protocols/tests/adders/adder_d1/nested_busy_wait.tx

@@ -1,4 +1,4 @@
-// ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/nested_busy_wait.prot
+// ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/nested_busy_wait.prot --allow-round-trip-failure
 trace {
     nested_busy_wait(1, 2, 2, 3, 3);   // 6 inner steps + 2 outer steps = 8 cycles  
     nested_busy_wait(10, 20, 3, 2, 30); // 6 inner steps + 3 outer steps = 9 cycles

protocols/tests/adders/adder_d1/second_thread_fails.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d1/wait_and_add_correct.rt

@@ -0,0 +1,15 @@
+trace_block: 0
+trace_result: FAIL
+failure_kind: monitor_error
+interpreter_trace:
+trace {
+    wait_and_add(1, 2, 3);
+    add(4, 5, 9);
+}
+
+monitor_error:
+All schedulers failed: No transactions match the waveform for DUT `Adder`
+Failure at cycle 1: No transactions match the waveform in `.roundtrip_tmp/adders-adder_d1-wait_and_add_correct_0.fst`.
+Possible transactions: [add, add_fork_early, add_doesnt_end_in_step, add_incorrect, add_incorrect_implicit, wait_and_add]
+Error: Monitor failed
+

protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/adders/adder_d2/both_threads_pass.rt

@@ -0,0 +1,16 @@
+trace_block: 0
+trace_result: PASS
+matched_monitor_trace_index: 0
+interpreter_trace:
+trace {
+    add(1, 2, 3);
+    add(4, 5, 9);
+}
+
+parsed_monitor_trace_candidates:
+candidate_monitor_trace: 0
+trace {
+    add(1, 2, 3);
+    add(4, 5, 9);
+}
+

protocols/tests/adders/adder_d2/no_dontcare_conflict.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/alus/alu_d1.rt

@@ -0,0 +1,22 @@
+trace_block: 0
+trace_result: PASS
+matched_monitor_trace_index: 0
+interpreter_trace:
+trace {
+    add(1, 2, 3);
+    add(123, 245, 368);
+    sub(200, 200, 0);
+    and(100, 100, 100);
+    or(0, 230, 230);
+}
+
+parsed_monitor_trace_candidates:
+candidate_monitor_trace: 0
+trace {
+    add(1, 2, 3);
+    add(123, 245, 368);
+    sub(200, 200, 0);
+    and(100, 100, 100);
+    or(0, 230, 230);
+}
+

protocols/tests/alus/alu_d2.rt

@@ -0,0 +1,22 @@
+trace_block: 0
+trace_result: PASS
+matched_monitor_trace_index: 0
+interpreter_trace:
+trace {
+    add(1, 2, 3);
+    add(123, 245, 368);
+    sub(200, 200, 0);
+    and(100, 100, 100);
+    or(0, 230, 230);
+}
+
+parsed_monitor_trace_candidates:
+candidate_monitor_trace: 0
+trace {
+    add(1, 2, 3);
+    add(123, 245, 368);
+    sub(200, 200, 0);
+    and(100, 100, 100);
+    or(0, 230, 230);
+}
+

protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.rt

@@ -0,0 +1,14 @@
+trace_block: 0
+trace_result: PASS
+matched_monitor_trace_index: 0
+interpreter_trace:
+trace {
+    bit_truncation_fft(8386560, 2047);
+}
+
+parsed_monitor_trace_candidates:
+candidate_monitor_trace: 0
+trace {
+    bit_truncation_fft(8386560, 2047);
+}
+

protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.rt

@@ -0,0 +1,14 @@
+trace_block: 0
+trace_result: PASS
+matched_monitor_trace_index: 0
+interpreter_trace:
+trace {
+    bit_truncation_sha(4398046511104, 68719476736);
+}
+
+parsed_monitor_trace_candidates:
+candidate_monitor_trace: 0
+trace {
+    bit_truncation_sha(4398046511104, 68719476736);
+}
+

protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.rt

@@ -0,0 +1,14 @@
+trace_block: 0
+trace_result: PASS
+matched_monitor_trace_index: 0
+interpreter_trace:
+trace {
+    failure_to_update_sha();
+}
+
+parsed_monitor_trace_candidates:
+candidate_monitor_trace: 0
+trace {
+    failure_to_update_sha();
+}
+

protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.rt

@@ -0,0 +1,14 @@
+trace_block: 0
+trace_result: PASS
+matched_monitor_trace_index: 0
+interpreter_trace:
+trace {
+    signal_async(6, 7);
+}
+
+parsed_monitor_trace_candidates:
+candidate_monitor_trace: 0
+trace {
+    signal_async(6, 7);
+}
+

protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.rt

@@ -0,0 +1 @@
+SKIP: non-zero // RETURN

protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.rt

@@ -0,0 +1,14 @@
+trace_block: 0
+trace_result: PASS
+matched_monitor_trace_index: 0
+interpreter_trace:
+trace {
+    use_without_valid(5, 5);
+}
+
+parsed_monitor_trace_candidates:
+candidate_monitor_trace: 0
+trace {
+    use_without_valid(5, 5);
+}
+

protocols/tests/counters/counter.rt

@@ -0,0 +1,14 @@
+trace_block: 0
+trace_result: PASS
+matched_monitor_trace_index: 0
+interpreter_trace:
+trace {
+    count_up(10);
+}
+
+parsed_monitor_trace_candidates:
+candidate_monitor_trace: 0
+trace {
+    count_up(10);
+}
+