[Interp] Multi-trace interpreter

examples/picorv32/unsigned_mul.out

@@ -1 +1 @@
-Protocol executed successfully!
+Trace 0 executed successfully!

examples/picorv32/unsigned_mul.tx

@@ -1,6 +1,8 @@
 // ARGS: --verilog picorv32/picorv32.v --protocol picorv32/pcpi_mul.prot --module picorv32_pcpi_mul
-pcpi_mul_reset();
-pcpi_mul(1, 1, 1);
-pcpi_mul(1, 100, 100);
-pcpi_mul(100, 1, 100);
-pcpi_mul(33554483, 200, 2415929304);
+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.out

@@ -1 +1 @@
-Protocol executed successfully!
+Trace 0 executed successfully!

examples/serv/serv_regfile.tx

@@ -1,11 +1,13 @@
 // ARGS: --verilog serv/rtl/serv_regfile.v --protocol serv/serv_regfile.prot 
-// Arguments to transaction are:
-// rs1_addr: u5
-// rs1_data: u32 (output)
-// rs2_data: u32 (output)
-// rs2_addr: u5
-// rd_enable: u1
-// rd_addr: u5
-// rd_data: u32
-read_write(0, 0, 0, 0, 1, 5, 0xdeadbeef);
-read_write(5, 0xdeadbeef, 0, 0, 0, 0, 0);
+trace {
+    // Arguments to transaction are:
+    // rs1_addr: u5
+    // rs1_data: u32 (output)
+    // rs2_data: u32 (output)
+    // rs2_addr: u5
+    // rd_enable: u1
+    // rd_addr: u5
+    // rd_data: u32
+    read_write(0, 0, 0, 0, 1, 5, 0xdeadbeef);
+    read_write(5, 0xdeadbeef, 0, 0, 0, 0, 0);
+}

examples/tinyaes128/aes128.out

@@ -1 +1 @@
-Protocol executed successfully!
+Trace 0 executed successfully!

examples/tinyaes128/aes128.tx

@@ -1,4 +1,6 @@
 // ARGS: --verilog tinyaes128/aes_128.v --protocol tinyaes128/aes128.prot --module aes_128
-// Arguments are key, state, expected output
-aes128(0x000102030405060708090a0b0c0d0e0f, 0x00112233445566778899aabbccddeeff, 0x69c4e0d86a7b0430d8cdb78070b4c55a);
-aes128(0x00000000000000000000000000000000, 0x00000000000000000000000000000000, 0x66e94bd4ef8a2c3b884cfa59ca342b2e);
+trace {
+    // Arguments are key, state, expected output
+    aes128(0x000102030405060708090a0b0c0d0e0f, 0x00112233445566778899aabbccddeeff, 0x69c4e0d86a7b0430d8cdb78070b4c55a);
+    aes128(0x00000000000000000000000000000000, 0x00000000000000000000000000000000, 0x66e94bd4ef8a2c3b884cfa59ca342b2e);
+}

interp/src/main.rs

@@ -8,7 +8,7 @@ use clap_verbosity_flag::{Verbosity, WarnLevel, log::LevelFilter};
 use protocols::diagnostic::DiagnosticHandler;
 use protocols::ir::{SymbolTable, Transaction};
 use protocols::scheduler::Scheduler;
-use protocols::setup::{assert_ok, setup_test_environment};
+use protocols::setup::setup_test_environment;
 use protocols::transactions_parser::parse_transactions_file;
 use protocols::typecheck::type_check;
 use rustc_hash::FxHashMap;
@@ -62,6 +62,31 @@ struct Cli {
 /// $ cargo run --package protocols-interp -- --verilog protocols/tests/counters/counter.v -p protocols/tests/counters/counter.prot -t protocols/tests/counters/counter.tx -v
 /// $ cargo run --package protocols-interp -- --verilog protocols/tests/identities/dual_identity_d1/dual_identity_d1.v -p protocols/tests/identities/dual_identity_d1/dual_identity_d1.prot -t tests/identities/dual_identity_d1/dual_identity_d1.tx
 /// ```
+fn with_trace_suffix(path: &str, trace_index: usize) -> String {
+    let path = std::path::Path::new(path);
+    let stem = path.file_stem().and_then(|s| s.to_str()).unwrap_or("");
+    let ext = path.extension().and_then(|e| e.to_str());
+
+    let file_name = if stem.is_empty() {
+        if let Some(ext) = ext {
+            format!("trace_{}.{}", trace_index, ext)
+        } else {
+            format!("trace_{}", trace_index)
+        }
+    } else if let Some(ext) = ext {
+        format!("{}_{}.{}", stem, trace_index, ext)
+    } else {
+        format!("{}_{}", stem, trace_index)
+    };
+
+    match path.parent() {
+        Some(parent) if !parent.as_os_str().is_empty() => {
+            parent.join(file_name).to_string_lossy().to_string()
+        }
+        _ => file_name,
+    }
+}
+
 fn main() -> anyhow::Result<()> {
     // Parse CLI args
     let cli = Cli::parse();
@@ -107,34 +132,48 @@ fn main() -> anyhow::Result<()> {
     // Create a separate `DiagnosticHandler` when parsing the transactions file
     let transactions_handler =
         &mut DiagnosticHandler::new(color_choice, cli.no_error_locations, emit_warnings);
-    let todos: Vec<(String, Vec<baa::BitVecValue>)> = parse_transactions_file(
+    let traces: Vec<Vec<(String, Vec<baa::BitVecValue>)>> = parse_transactions_file(
         cli.transactions,
         transactions_handler,
         transaction_arg_types,
     )?;
 
-    // Run the interpreter and the scheduler on the parsed transaction file
-    let interpreter = if let Some(waveform_file) = cli.fst {
-        patronus::sim::Interpreter::new_with_wavedump(&ctx, &sys, waveform_file)
-    } else {
-        patronus::sim::Interpreter::new(&ctx, &sys)
-    };
-
-    let mut scheduler = Scheduler::new(
-        transactions_and_symbols,
-        todos,
-        &ctx,
-        &sys,
-        interpreter,
-        protocols_handler,
-        cli.max_steps.unwrap_or(u32::MAX),
-    );
-    let results = scheduler.execute_todos();
+    let mut any_failed = false;
+    for (trace_index, todos) in traces.into_iter().enumerate() {
+        if trace_index > 0 {
+            println!("\n---\n");
+        }
+
+        // Run each trace in isolation with a fresh interpreter and scheduler.
+        let interpreter = if let Some(waveform_file) = &cli.fst {
+            let waveform_file = with_trace_suffix(waveform_file, trace_index);
+            patronus::sim::Interpreter::new_with_wavedump(&ctx, &sys, waveform_file)
+        } else {
+            patronus::sim::Interpreter::new(&ctx, &sys)
+        };
+
+        let mut scheduler = Scheduler::new(
+            transactions_and_symbols.clone(),
+            todos,
+            &ctx,
+            &sys,
+            interpreter,
+            protocols_handler,
+            cli.max_steps.unwrap_or(u32::MAX),
+        );
+        let results = scheduler.execute_todos();
+        let trace_failed = results.iter().any(|res| res.is_err());
+
+        if trace_failed {
+            any_failed = true;
+            println!("Trace {} execution failed.", trace_index);
+        } else {
+            println!("Trace {} executed successfully!", trace_index);
+        }
+    }
 
-    // Check whether the protocol was executed successfully
-    for res in results {
-        assert_ok(&res)
+    if any_failed {
+        panic!("One or more traces failed.");
     }
-    println!("Protocol executed successfully!");
     Ok(())
 }

protocols/src/transactions.pest

@@ -17,6 +17,7 @@ decimal_integer = ${ ASCII_DIGIT ~ ("_"? ~ ASCII_DIGIT)* }
 arg = ${ binary_integer | hex_integer | decimal_integer }
 arglist = { (arg ~ "," ~ arglist) | arg ~ ","? }
 transaction = { ident ~ "(" ~ arglist? ~ ")" ~ ";" }
+trace = { "trace" ~ "{" ~ transaction* ~ "}" }
 
-// A transactions file is just a list of transactions
-file = { SOI ~ transaction* ~ EOI }
+// A transactions file is a list of trace blocks
+file = { SOI ~ trace* ~ EOI }

protocols/src/transactions_parser.rs

@@ -17,7 +17,7 @@ pub fn parse_transactions_file(
     filepath: impl AsRef<std::path::Path>,
     handler: &mut DiagnosticHandler,
     transaction_arg_types: FxHashMap<String, Vec<Type>>,
-) -> anyhow::Result<Vec<TodoItem>> {
+) -> anyhow::Result<Vec<Vec<TodoItem>>> {
     let filename = filepath.as_ref().to_str().unwrap().to_string();
     let input = std::fs::read_to_string(filepath).map_err(|e| anyhow!("failed to load: {}", e))?;
     let fileid = handler.add_file(filename, input.clone());
@@ -37,35 +37,44 @@ pub fn parse_transactions_file(
 
     // Access the `Rule`s contained within the parsed result
     let inner_rules = parse_result.unwrap().next().unwrap().into_inner();
-    let mut todos = vec![];
+    let mut traces: Vec<Vec<TodoItem>> = vec![];
 
-    // Parse each transaction
-    for transaction_pair in inner_rules {
-        if let Rule::transaction = transaction_pair.as_rule() {
-            let mut transaction_inner = transaction_pair.into_inner();
+    // Parse each trace block and each transaction within each block.
+    for trace_pair in inner_rules {
+        if trace_pair.as_rule() == Rule::trace {
+            let mut trace_todos: Vec<TodoItem> = vec![];
+            for transaction_pair in trace_pair.into_inner() {
+                if transaction_pair.as_rule() == Rule::transaction {
+                    let mut transaction_inner = transaction_pair.into_inner();
 
-            // First element should be the function name (ident)
-            let function_name = transaction_inner.next().unwrap().as_str().to_string();
+                    // First element should be the function name (ident)
+                    let function_name = transaction_inner.next().unwrap().as_str().to_string();
 
-            let arg_types = transaction_arg_types
-                .get(&function_name)
-                .unwrap_or_else(|| {
-                    panic!("Unable to fetch argument types for transaction {function_name}")
-                });
+                    let arg_types =
+                        transaction_arg_types
+                            .get(&function_name)
+                            .unwrap_or_else(|| {
+                                panic!(
+                                    "Unable to fetch argument types for transaction {function_name}"
+                                )
+                            });
 
-            // Parse arguments if they exist
-            let mut args: Vec<BitVecValue> = vec![];
-            if let Some(arglist_pair) = transaction_inner.next() {
-                if arglist_pair.as_rule() == Rule::arglist {
-                    args = parse_arglist(arglist_pair, handler, fileid, arg_types)?;
+                    // Parse arguments if they exist
+                    let mut args: Vec<BitVecValue> = vec![];
+                    if let Some(arglist_pair) = transaction_inner.next() {
+                        if arglist_pair.as_rule() == Rule::arglist {
+                            args = parse_arglist(arglist_pair, handler, fileid, arg_types)?;
+                        }
+                    }
+
+                    trace_todos.push((function_name, args));
                 }
             }
-
-            todos.push((function_name, args));
+            traces.push(trace_todos);
         }
     }
 
-    Ok(todos)
+    Ok(traces)
 }
 
 /// Parses a list of arguments that are supplied to a transaction,

protocols/tests/adders/adder_d0/add_combinational.out

@@ -1 +1 @@
-Protocol executed successfully!
+Trace 0 executed successfully!

protocols/tests/adders/adder_d0/add_combinational.tx

@@ -1,2 +1,4 @@
 // ARGS: --verilog adders/adder_d0/add_d0.v --protocol adders/adder_d0/add_d0.prot
-add_combinational(100, 200, 300);
+trace {
+    add_combinational(100, 200, 300);
+}

protocols/tests/adders/adder_d0/illegal_assignment.out

@@ -4,3 +4,4 @@ error: Output 'DUT.s' depends on input(s) 'DUT.b', 'DUT.a' which do not have ass
 30 │   if (DUT.s == 32'b0) {
    │       ^^^^^ Output 'DUT.s' depends on input(s) 'DUT.b', 'DUT.a' which do not have assigned values ('DUT.b', 'DUT.a' initialized to DontCare and were never assigned a concrete value)
 
+Trace 0 execution failed.

protocols/tests/adders/adder_d0/illegal_assignment.tx

@@ -1,3 +1,5 @@
 // ARGS: --verilog adders/adder_d0/add_d0.v --protocol adders/adder_d0/add_d0.prot
 // RETURN: 101
-add_combinational_legal_observation_illegal_assignment(7, 8, 15);
+trace {
+    add_combinational_legal_observation_illegal_assignment(7, 8, 15);
+}

protocols/tests/adders/adder_d0/illegal_observation_assertion.out

@@ -7,3 +7,4 @@ error: Output 'DUT.s' depends on input(s) 'DUT.b' which do not have assigned val
 25 │   assert_eq(DUT.s, s); // this should be illegal
    │             ^^^^^ Output 'DUT.s' depends on input(s) 'DUT.b' which do not have assigned values
 
+Trace 0 execution failed.

protocols/tests/adders/adder_d0/illegal_observation_assertion.tx

@@ -1,3 +1,5 @@
 // ARGS: --verilog adders/adder_d0/add_d0.v --protocol adders/adder_d0/add_d0.prot
 // RETURN: 101
-add_combinational_illegal_observation_in_assertion(10, 20, 30);
+trace {
+    add_combinational_illegal_observation_in_assertion(10, 20, 30);
+}

protocols/tests/adders/adder_d0/illegal_observation_conditional.out

@@ -7,3 +7,4 @@ error: Output 'DUT.s' depends on input(s) 'DUT.b' which do not have assigned val
 12 │   if (DUT.s == 32'b0) { // this should be illegal
    │       ^^^^^ Output 'DUT.s' depends on input(s) 'DUT.b' which do not have assigned values
 
+Trace 0 execution failed.

protocols/tests/adders/adder_d0/illegal_observation_conditional.tx

@@ -1,3 +1,5 @@
 // ARGS: --verilog adders/adder_d0/add_d0.v --protocol adders/adder_d0/add_d0.prot
 // RETURN: 101
-add_combinational_illegal_observation_in_conditional(5, 3, 8);
+trace {
+    add_combinational_illegal_observation_in_conditional(5, 3, 8);
+}

protocols/tests/adders/adder_d1/add_incorrect.out

@@ -10,3 +10,4 @@ error: Thread 1 (`add_incorrect`) attempted conflicting assignment to 'a': curre
 44 │   DUT.a := a;
    │   ^^^^^^^^^^^ Thread 1 (`add_incorrect`) attempted conflicting assignment to 'a': current=1, new=4
 
+Trace 0 execution failed.

protocols/tests/adders/adder_d1/add_incorrect.tx

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

protocols/tests/adders/adder_d1/add_incorrect_implicit.out

@@ -10,3 +10,4 @@ error: Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to '
 55 │   DUT.a := a;
    │   ^^^^^^^^^^^ Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'a': current=1, new=4
 
+Trace 0 execution failed.

protocols/tests/adders/adder_d1/add_incorrect_implicit.tx

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

protocols/tests/adders/adder_d1/add_multitrace.out

@@ -0,0 +1,11 @@
+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.

protocols/tests/adders/adder_d1/add_multitrace.tx

@@ -0,0 +1,11 @@
+// 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);
+}

protocols/tests/adders/adder_d1/both_threads_fail.out

@@ -10,3 +10,4 @@ error: The two expressions did not evaluate to the same value
 26 │   assert_eq(s, DUT.s);
    │             ^^^^^^^^ LHS Value: 10, RHS Value: 9
 
+Trace 0 execution failed.

protocols/tests/adders/adder_d1/both_threads_fail.tx

@@ -1,4 +1,6 @@
 // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot
 // RETURN: 101
-add_fork_early(1, 2, 5);
-add_fork_early(4, 5, 10);
+trace {
+    add_fork_early(1, 2, 5);
+    add_fork_early(4, 5, 10);
+}

protocols/tests/adders/adder_d1/both_threads_pass.out

@@ -1 +1 @@
-Protocol executed successfully!
+Trace 0 executed successfully!

protocols/tests/adders/adder_d1/both_threads_pass.tx

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

protocols/tests/adders/adder_d1/busy_wait_fail.out

@@ -4,3 +4,4 @@ error: The two expressions did not evaluate to the same value
 21 │     assert_eq(s, DUT.s);
    │               ^^^^^^^^ LHS Value: 999, RHS Value: 3
 
+Trace 0 execution failed.

protocols/tests/adders/adder_d1/busy_wait_fail.tx

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

protocols/tests/adders/adder_d1/busy_wait_pass.out

@@ -1 +1 @@
-Protocol executed successfully!
+Trace 0 executed successfully!

protocols/tests/adders/adder_d1/busy_wait_pass.tx

@@ -1,3 +1,5 @@
 // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/busy_wait.prot
-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 
+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 
+}