Skip to content

Comments

[Interp] Multi-trace interpreter#186

Merged
Nikil-Shyamsunder merged 3 commits intomainfrom
multitrace-interpreter
Feb 15, 2026
Merged

[Interp] Multi-trace interpreter#186
Nikil-Shyamsunder merged 3 commits intomainfrom
multitrace-interpreter

Conversation

@Nikil-Shyamsunder
Copy link
Collaborator

@Nikil-Shyamsunder Nikil-Shyamsunder commented Feb 15, 2026

PR Summary

This change adds multi-trace execution support to the interpreter. If we merge this, then update the monitor PR #181 to reflect this syntax (very minor change), we can then do round trip testing where the interpreter .tx file and .fst file can go into the monitor, and the monitor-produces .out file of transactions can go straight back into the interpreter, and we can even check if the fsts generated by the interpreter on the monitor executed transactions are equivalent to the fst generated by the interpreter on the original .tx file modulo DontCares!

In interp/src/main.rs, the interpreter now parses a .tx file as multiple traces and runs them one by one in full isolation (fresh scheduler/interpreter state per trace). main only prints a per-trace status line (Trace N executed successfully! or Trace N execution failed.), and detailed errors still come from the existing diagnostic path (Scheduler::execute_todos -> diagnostic emitter). If --fst is provided, output filenames are suffixed by trace index (_0, _1, ...). The process still exits with failure if any trace fails.

In protocols/src/transactions.pest, the grammar explicitly supports a file as a sequence of trace blocks:

trace = { "trace" ~ "{" ~ transaction* ~ "}" }
file = { SOI ~ trace* ~ EOI }

Example multi-trace test:

protocols/tests/adders/adder_d1/add_multitrace.tx

// ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot
// RETURN: 101
trace {
    add(1, 2, 3);
    add(4, 5, 9);
}

trace {
    add(1, 2, 3);
    add(4, 5, 10);
}

Observed output:

protocols/tests/adders/adder_d1/add_multitrace.out

Trace 0 executed successfully!

---

error: The two expressions did not evaluate to the same value
   ┌─ adders/adder_d1/add_d1.prot:14:13
   │
14 │   assert_eq(s, DUT.s);
   │             ^^^^^^^^ LHS Value: 10, RHS Value: 9

Trace 1 execution failed.

It's a little unfortunate that the "Trace 1 execution failed." message comes at the end and not at the beginnign (before the error), but to change this would require significant code changes to the routing of the diagnostics that I don't think is worth changing (especially given a rewrite of that error handling part of the codebase is warranted sometime in the future).

@Nikil-Shyamsunder Nikil-Shyamsunder marked this pull request as ready for review February 15, 2026 05:27
Copy link
Contributor

@ngernest ngernest left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great idea -- thanks for implementing this, looks good!

@Nikil-Shyamsunder Nikil-Shyamsunder merged commit 1a5fd9d into main Feb 15, 2026
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants