From 2c5d408043f277bf77d7b66e7b73878e0e5654b0 Mon Sep 17 00:00:00 2001 From: Nikil-Shyamsunder Date: Sat, 14 Feb 2026 20:53:21 -0800 Subject: [PATCH 1/3] modify interpreter transaction syntax and outputs --- examples/picorv32/unsigned_mul.out | 2 +- examples/picorv32/unsigned_mul.tx | 3 + examples/serv/serv_regfile.out | 2 +- examples/serv/serv_regfile.tx | 3 + examples/tinyaes128/aes128.out | 2 +- examples/tinyaes128/aes128.tx | 3 + interp/src/main.rs | 90 ++++++++++++++----- protocols/src/transactions.pest | 5 +- protocols/src/transactions_parser.rs | 48 +++++----- .../adders/adder_d0/add_combinational.out | 2 +- .../adders/adder_d0/add_combinational.tx | 3 + .../adders/adder_d0/illegal_assignment.out | 2 + .../adders/adder_d0/illegal_assignment.tx | 3 + .../illegal_observation_assertion.out | 2 + .../adder_d0/illegal_observation_assertion.tx | 3 + .../illegal_observation_conditional.out | 2 + .../illegal_observation_conditional.tx | 3 + .../tests/adders/adder_d1/add_incorrect.out | 3 + .../tests/adders/adder_d1/add_incorrect.tx | 3 + .../adder_d1/add_incorrect_implicit.out | 3 + .../adders/adder_d1/add_incorrect_implicit.tx | 3 + .../adders/adder_d1/both_threads_fail.out | 3 + .../adders/adder_d1/both_threads_fail.tx | 3 + .../adders/adder_d1/both_threads_pass.out | 2 +- .../adders/adder_d1/both_threads_pass.tx | 4 +- .../tests/adders/adder_d1/busy_wait_fail.out | 2 + .../tests/adders/adder_d1/busy_wait_fail.tx | 3 + .../tests/adders/adder_d1/busy_wait_pass.out | 2 +- .../tests/adders/adder_d1/busy_wait_pass.tx | 3 + .../adders/adder_d1/didnt_end_in_step.out | 2 + .../adders/adder_d1/didnt_end_in_step.tx | 3 + .../adders/adder_d1/double_fork_error.out | 3 + .../adders/adder_d1/double_fork_error.tx | 3 + .../adder_d1/first_fail_second_norun.out | 2 + .../adder_d1/first_fail_second_norun.tx | 3 + .../adders/adder_d1/first_thread_fails.out | 2 + .../adders/adder_d1/first_thread_fails.tx | 4 +- .../adder_d1/fork_before_step_error.out | 2 + .../adders/adder_d1/fork_before_step_error.tx | 3 + .../adders/adder_d1/loop_with_assigns.out | 2 +- .../adders/adder_d1/loop_with_assigns.tx | 3 + .../adders/adder_d1/nested_busy_wait.out | 2 +- .../tests/adders/adder_d1/nested_busy_wait.tx | 3 + .../adders/adder_d1/second_thread_fails.out | 2 + .../adders/adder_d1/second_thread_fails.tx | 4 +- .../adders/adder_d1/wait_and_add_correct.out | 2 +- .../adders/adder_d1/wait_and_add_correct.tx | 3 + .../wait_and_add_incorrect_implicit.out | 3 + .../wait_and_add_incorrect_implicit.tx | 3 + .../adders/adder_d2/both_threads_pass.out | 2 +- .../adders/adder_d2/both_threads_pass.tx | 3 + .../adders/adder_d2/no_dontcare_conflict.out | 3 + .../adders/adder_d2/no_dontcare_conflict.tx | 3 + protocols/tests/alus/alu_d1.out | 2 +- protocols/tests/alus/alu_d1.tx | 3 + protocols/tests/alus/alu_d2.out | 2 +- protocols/tests/alus/alu_d2.tx | 3 + .../bit_truncation/bit_truncation_fft_bug.out | 2 + .../bit_truncation/bit_truncation_fft_bug.tx | 4 +- .../bit_truncation/bit_truncation_fft_fix.out | 2 +- .../bit_truncation/bit_truncation_fft_fix.tx | 4 +- .../bit_truncation/bit_truncation_sha_bug.out | 2 + .../bit_truncation/bit_truncation_sha_bug.tx | 4 +- .../bit_truncation/bit_truncation_sha_fix.out | 2 +- .../bit_truncation/bit_truncation_sha_fix.tx | 4 +- .../failure_to_update/ftu_sha_bug.out | 2 + .../failure_to_update/ftu_sha_bug.tx | 4 +- .../failure_to_update/ftu_sha_fix.out | 2 +- .../failure_to_update/ftu_sha_fix.tx | 4 +- .../signal_asynchrony/signal_async_bug.out | 2 + .../signal_asynchrony/signal_async_bug.tx | 4 +- .../signal_asynchrony/signal_async_fix.out | 2 +- .../signal_asynchrony/signal_async_fix.tx | 4 +- .../use_without_valid_bug.out | 2 + .../use_without_valid_bug.tx | 4 +- .../use_without_valid_fix.out | 2 +- .../use_without_valid_fix.tx | 4 +- protocols/tests/counters/counter.out | 2 +- protocols/tests/counters/counter.tx | 3 + protocols/tests/fifo/fifo.out | 2 +- protocols/tests/fifo/fifo.tx | 3 + protocols/tests/fifo/pop_before_push_fail.out | 2 + protocols/tests/fifo/pop_before_push_fail.tx | 4 +- protocols/tests/fifo/pop_empty_fail.out | 2 + protocols/tests/fifo/pop_empty_fail.tx | 4 +- protocols/tests/fifo/push_pop_conflict.out | 2 + protocols/tests/fifo/push_pop_conflict.tx | 3 + protocols/tests/fifo/push_pop_identity_ok.out | 2 +- protocols/tests/fifo/push_pop_identity_ok.tx | 4 +- protocols/tests/fifo/push_pop_loop_empty.out | 2 +- protocols/tests/fifo/push_pop_loop_empty.tx | 3 + .../tests/fifo/push_pop_loop_not_empty.out | 2 +- .../tests/fifo/push_pop_loop_not_empty.tx | 3 + .../dual_identity_d0_combdep.out | 2 + .../dual_identity_d0_combdep.tx | 3 + .../dual_identity_d1/dual_identity_d1.tx | 3 + .../identity_d0/passthrough_combdep.out | 2 +- .../identity_d0/passthrough_combdep.tx | 3 + .../identities/identity_d1/explicit_fork.out | 2 + .../identities/identity_d1/explicit_fork.tx | 3 + .../identities/identity_d1/slicing_err.tx | 4 +- .../identities/identity_d1/slicing_invalid.tx | 4 +- .../identities/identity_d1/slicing_ok.out | 2 +- .../identities/identity_d1/slicing_ok.tx | 4 +- .../identity_d2/single_thread_passes.out | 2 +- .../identity_d2/single_thread_passes.tx | 3 + .../two_assignments_same_value.out | 2 +- .../identity_d2/two_assignments_same_value.tx | 3 + .../two_different_assignments_error.out | 3 + .../two_different_assignments_error.tx | 3 + .../identities/identity_d2/two_fork_err.out | 2 + .../identities/identity_d2/two_fork_err.tx | 3 + .../identity_d2/two_fork_ill_formed.tx | 3 + protocols/tests/inverters/inverter_d0.out | 2 + protocols/tests/inverters/inverter_d0.tx | 3 + protocols/tests/multi/multi0/multi0.out | 2 +- protocols/tests/multi/multi0/multi0.tx | 3 + .../tests/multi/multi0keep/multi0keep.out | 2 +- .../tests/multi/multi0keep/multi0keep.tx | 3 + .../multi0keep2const/multi0keep2const.out | 2 +- .../multi0keep2const/multi0keep2const.tx | 3 + .../tests/multi/multi2const/multi2const.out | 2 +- .../tests/multi/multi2const/multi2const.tx | 3 + .../tests/multi/multi2multi/multi2multi.out | 2 +- .../tests/multi/multi2multi/multi2multi.tx | 3 + .../tests/multi/multi_data/multi_data.out | 2 +- .../tests/multi/multi_data/multi_data.tx | 3 + .../multipliers/mult_d2/both_threads_fail.out | 3 + .../multipliers/mult_d2/both_threads_fail.tx | 3 + .../multipliers/mult_d2/both_threads_pass.out | 2 +- .../multipliers/mult_d2/both_threads_pass.tx | 3 + .../mult_d2/first_thread_fails.out | 2 + .../multipliers/mult_d2/first_thread_fails.tx | 3 + .../mult_d2/second_thread_fails.out | 2 + .../mult_d2/second_thread_fails.tx | 3 + .../tests/picorv32/unsigned_mul_no_reset.out | 2 + .../tests/picorv32/unsigned_mul_no_reset.tx | 4 +- ...no_reset_thread_assignment_persistence.out | 2 + ..._no_reset_thread_assignment_persistence.tx | 4 +- 139 files changed, 414 insertions(+), 100 deletions(-) diff --git a/examples/picorv32/unsigned_mul.out b/examples/picorv32/unsigned_mul.out index c6eb0316..f5f6cb49 100644 --- a/examples/picorv32/unsigned_mul.out +++ b/examples/picorv32/unsigned_mul.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/examples/picorv32/unsigned_mul.tx b/examples/picorv32/unsigned_mul.tx index d391b59a..c49259b8 100644 --- a/examples/picorv32/unsigned_mul.tx +++ b/examples/picorv32/unsigned_mul.tx @@ -1,6 +1,9 @@ +trace { // 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); + +} diff --git a/examples/serv/serv_regfile.out b/examples/serv/serv_regfile.out index c6eb0316..f5f6cb49 100644 --- a/examples/serv/serv_regfile.out +++ b/examples/serv/serv_regfile.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/examples/serv/serv_regfile.tx b/examples/serv/serv_regfile.tx index 50fe248c..b45d1ad0 100644 --- a/examples/serv/serv_regfile.tx +++ b/examples/serv/serv_regfile.tx @@ -1,3 +1,4 @@ +trace { // ARGS: --verilog serv/rtl/serv_regfile.v --protocol serv/serv_regfile.prot // Arguments to transaction are: // rs1_addr: u5 @@ -9,3 +10,5 @@ // rd_data: u32 read_write(0, 0, 0, 0, 1, 5, 0xdeadbeef); read_write(5, 0xdeadbeef, 0, 0, 0, 0, 0); + +} diff --git a/examples/tinyaes128/aes128.out b/examples/tinyaes128/aes128.out index c6eb0316..f5f6cb49 100644 --- a/examples/tinyaes128/aes128.out +++ b/examples/tinyaes128/aes128.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/examples/tinyaes128/aes128.tx b/examples/tinyaes128/aes128.tx index 674f6581..a8acbb5a 100644 --- a/examples/tinyaes128/aes128.tx +++ b/examples/tinyaes128/aes128.tx @@ -1,4 +1,7 @@ +trace { // 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); + +} diff --git a/interp/src/main.rs b/interp/src/main.rs index 2771c579..2788cb88 100644 --- a/interp/src/main.rs +++ b/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,32 @@ 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 +133,52 @@ 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)> = parse_transactions_file( + let traces: Vec)>> = 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() { + // 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(); + + // Report each trace result to stdout so it is captured in .out files. + let mut trace_failed = false; + for res in results { + if let Err(err) = res { + trace_failed = true; + println!("Trace {} failed: {:?}", trace_index, 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(()) } diff --git a/protocols/src/transactions.pest b/protocols/src/transactions.pest index 58b511e9..69eb0590 100644 --- a/protocols/src/transactions.pest +++ b/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 } \ No newline at end of file +// A transactions file is a list of trace blocks +file = { SOI ~ trace* ~ EOI } diff --git a/protocols/src/transactions_parser.rs b/protocols/src/transactions_parser.rs index 7799fe29..84a84b27 100644 --- a/protocols/src/transactions_parser.rs +++ b/protocols/src/transactions_parser.rs @@ -17,7 +17,7 @@ pub fn parse_transactions_file( filepath: impl AsRef, handler: &mut DiagnosticHandler, transaction_arg_types: FxHashMap>, -) -> anyhow::Result> { +) -> anyhow::Result>> { 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,41 @@ 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![]; - // 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 = 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 = 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 = 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, diff --git a/protocols/tests/adders/adder_d0/add_combinational.out b/protocols/tests/adders/adder_d0/add_combinational.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/adders/adder_d0/add_combinational.out +++ b/protocols/tests/adders/adder_d0/add_combinational.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/adders/adder_d0/add_combinational.tx b/protocols/tests/adders/adder_d0/add_combinational.tx index 5b0cbf35..8f75b04d 100644 --- a/protocols/tests/adders/adder_d0/add_combinational.tx +++ b/protocols/tests/adders/adder_d0/add_combinational.tx @@ -1,2 +1,5 @@ +trace { // ARGS: --verilog adders/adder_d0/add_d0.v --protocol adders/adder_d0/add_d0.prot add_combinational(100, 200, 300); + +} diff --git a/protocols/tests/adders/adder_d0/illegal_assignment.out b/protocols/tests/adders/adder_d0/illegal_assignment.out index f991efad..e18da9f7 100644 --- a/protocols/tests/adders/adder_d0/illegal_assignment.out +++ b/protocols/tests/adders/adder_d0/illegal_assignment.out @@ -4,3 +4,5 @@ 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 failed: Evaluation(ForbiddenPortRead { port_name: "DUT.s", unassigned_inputs: [("DUT.b", None), ("DUT.a", None)], expr_id: expr1 }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d0/illegal_assignment.tx b/protocols/tests/adders/adder_d0/illegal_assignment.tx index 12c78934..c7387898 100644 --- a/protocols/tests/adders/adder_d0/illegal_assignment.tx +++ b/protocols/tests/adders/adder_d0/illegal_assignment.tx @@ -1,3 +1,6 @@ +trace { // 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); + +} diff --git a/protocols/tests/adders/adder_d0/illegal_observation_assertion.out b/protocols/tests/adders/adder_d0/illegal_observation_assertion.out index e9e8457d..6e6f441d 100644 --- a/protocols/tests/adders/adder_d0/illegal_observation_assertion.out +++ b/protocols/tests/adders/adder_d0/illegal_observation_assertion.out @@ -7,3 +7,5 @@ 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 failed: Evaluation(ForbiddenPortRead { port_name: "DUT.s", unassigned_inputs: [("DUT.b", Some(stmt2))], expr_id: expr4 }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d0/illegal_observation_assertion.tx b/protocols/tests/adders/adder_d0/illegal_observation_assertion.tx index b72dfd09..87b5063c 100644 --- a/protocols/tests/adders/adder_d0/illegal_observation_assertion.tx +++ b/protocols/tests/adders/adder_d0/illegal_observation_assertion.tx @@ -1,3 +1,6 @@ +trace { // 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); + +} diff --git a/protocols/tests/adders/adder_d0/illegal_observation_conditional.out b/protocols/tests/adders/adder_d0/illegal_observation_conditional.out index af6bb99d..5c3cb6d8 100644 --- a/protocols/tests/adders/adder_d0/illegal_observation_conditional.out +++ b/protocols/tests/adders/adder_d0/illegal_observation_conditional.out @@ -7,3 +7,5 @@ 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 failed: Evaluation(ForbiddenPortRead { port_name: "DUT.s", unassigned_inputs: [("DUT.b", Some(stmt2))], expr_id: expr4 }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d0/illegal_observation_conditional.tx b/protocols/tests/adders/adder_d0/illegal_observation_conditional.tx index 78fdd6ea..e87ba3f8 100644 --- a/protocols/tests/adders/adder_d0/illegal_observation_conditional.tx +++ b/protocols/tests/adders/adder_d0/illegal_observation_conditional.tx @@ -1,3 +1,6 @@ +trace { // 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); + +} diff --git a/protocols/tests/adders/adder_d1/add_incorrect.out b/protocols/tests/adders/adder_d1/add_incorrect.out index 32e962d1..311a3d35 100644 --- a/protocols/tests/adders/adder_d1/add_incorrect.out +++ b/protocols/tests/adders/adder_d1/add_incorrect.out @@ -10,3 +10,6 @@ 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 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000100), new_value: ValueOwned(00000000000000000000000000000001), thread_idx: 0, transaction_name: "add_incorrect", stmt_id: stmt4 }) +Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000001), new_value: ValueOwned(00000000000000000000000000000100), thread_idx: 1, transaction_name: "add_incorrect", stmt_id: stmt1 }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/add_incorrect.tx b/protocols/tests/adders/adder_d1/add_incorrect.tx index f55750fd..dfc6856a 100644 --- a/protocols/tests/adders/adder_d1/add_incorrect.tx +++ b/protocols/tests/adders/adder_d1/add_incorrect.tx @@ -1,4 +1,7 @@ +trace { // 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); + +} diff --git a/protocols/tests/adders/adder_d1/add_incorrect_implicit.out b/protocols/tests/adders/adder_d1/add_incorrect_implicit.out index f5da2d6b..05494e9a 100644 --- a/protocols/tests/adders/adder_d1/add_incorrect_implicit.out +++ b/protocols/tests/adders/adder_d1/add_incorrect_implicit.out @@ -10,3 +10,6 @@ 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 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000100), new_value: ValueOwned(00000000000000000000000000000001), thread_idx: 0, transaction_name: "add_incorrect_implicit", stmt_id: stmt1 }) +Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000001), new_value: ValueOwned(00000000000000000000000000000100), thread_idx: 1, transaction_name: "add_incorrect_implicit", stmt_id: stmt1 }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/add_incorrect_implicit.tx b/protocols/tests/adders/adder_d1/add_incorrect_implicit.tx index 13966a09..dddd7483 100644 --- a/protocols/tests/adders/adder_d1/add_incorrect_implicit.tx +++ b/protocols/tests/adders/adder_d1/add_incorrect_implicit.tx @@ -1,4 +1,7 @@ +trace { // 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); + +} diff --git a/protocols/tests/adders/adder_d1/both_threads_fail.out b/protocols/tests/adders/adder_d1/both_threads_fail.out index 8178f4d7..ced952de 100644 --- a/protocols/tests/adders/adder_d1/both_threads_fail.out +++ b/protocols/tests/adders/adder_d1/both_threads_fail.out @@ -10,3 +10,6 @@ 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 failed: Assertion(EqualityFailed { expr1_id: expr5, expr2_id: expr6, value1: ValueOwned(00000000000000000000000000000101), value2: ValueOwned(00000000000000000000000000000011) }) +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr5, expr2_id: expr6, value1: ValueOwned(00000000000000000000000000001010), value2: ValueOwned(00000000000000000000000000001001) }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/both_threads_fail.tx b/protocols/tests/adders/adder_d1/both_threads_fail.tx index 3014f0bb..552e6324 100644 --- a/protocols/tests/adders/adder_d1/both_threads_fail.tx +++ b/protocols/tests/adders/adder_d1/both_threads_fail.tx @@ -1,4 +1,7 @@ +trace { // 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); + +} diff --git a/protocols/tests/adders/adder_d1/both_threads_pass.out b/protocols/tests/adders/adder_d1/both_threads_pass.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/adders/adder_d1/both_threads_pass.out +++ b/protocols/tests/adders/adder_d1/both_threads_pass.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/adders/adder_d1/both_threads_pass.tx b/protocols/tests/adders/adder_d1/both_threads_pass.tx index 590853bf..8ffe5992 100644 --- a/protocols/tests/adders/adder_d1/both_threads_pass.tx +++ b/protocols/tests/adders/adder_d1/both_threads_pass.tx @@ -1,3 +1,5 @@ +trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot add(1, 2, 3); -add(4, 5, 9); \ No newline at end of file +add(4, 5, 9); +} diff --git a/protocols/tests/adders/adder_d1/busy_wait_fail.out b/protocols/tests/adders/adder_d1/busy_wait_fail.out index 761cd89f..fbf92b57 100644 --- a/protocols/tests/adders/adder_d1/busy_wait_fail.out +++ b/protocols/tests/adders/adder_d1/busy_wait_fail.out @@ -4,3 +4,5 @@ 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 failed: Assertion(EqualityFailed { expr1_id: expr4, expr2_id: expr5, value1: ValueOwned(00000000000000000000001111100111), value2: ValueOwned(00000000000000000000000000000011) }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/busy_wait_fail.tx b/protocols/tests/adders/adder_d1/busy_wait_fail.tx index bfe7f705..e45dfe14 100644 --- a/protocols/tests/adders/adder_d1/busy_wait_fail.tx +++ b/protocols/tests/adders/adder_d1/busy_wait_fail.tx @@ -1,3 +1,6 @@ +trace { // 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 + +} diff --git a/protocols/tests/adders/adder_d1/busy_wait_pass.out b/protocols/tests/adders/adder_d1/busy_wait_pass.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/adders/adder_d1/busy_wait_pass.out +++ b/protocols/tests/adders/adder_d1/busy_wait_pass.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/adders/adder_d1/busy_wait_pass.tx b/protocols/tests/adders/adder_d1/busy_wait_pass.tx index 1c7161a3..90b5ebea 100644 --- a/protocols/tests/adders/adder_d1/busy_wait_pass.tx +++ b/protocols/tests/adders/adder_d1/busy_wait_pass.tx @@ -1,3 +1,6 @@ +trace { // 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 + +} diff --git a/protocols/tests/adders/adder_d1/didnt_end_in_step.out b/protocols/tests/adders/adder_d1/didnt_end_in_step.out index 16b6b59e..7eb2505a 100644 --- a/protocols/tests/adders/adder_d1/didnt_end_in_step.out +++ b/protocols/tests/adders/adder_d1/didnt_end_in_step.out @@ -4,3 +4,5 @@ error: The last executed statement in Thread 0 (transaction 'add_doesnt_end_in_s 39 │ fork(); │ ^^^^^^^ last statement wasn't `step()` +Trace 0 failed: Thread(DidntEndWithStep { thread_idx: 0, transaction_name: "add_doesnt_end_in_step", last_executed_stmt_id: stmt7 }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/didnt_end_in_step.tx b/protocols/tests/adders/adder_d1/didnt_end_in_step.tx index a7ff0b30..671823a3 100644 --- a/protocols/tests/adders/adder_d1/didnt_end_in_step.tx +++ b/protocols/tests/adders/adder_d1/didnt_end_in_step.tx @@ -1,4 +1,7 @@ +trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 add_doesnt_end_in_step(1, 2, 3); + +} diff --git a/protocols/tests/adders/adder_d1/double_fork_error.out b/protocols/tests/adders/adder_d1/double_fork_error.out index 3178405a..c92cbd4e 100644 --- a/protocols/tests/adders/adder_d1/double_fork_error.out +++ b/protocols/tests/adders/adder_d1/double_fork_error.out @@ -16,3 +16,6 @@ error: Thread 1 (transaction 'add_double_fork') attempted to fork more than once 15 │ fork(); │ ^^^^^^^ second fork() called here +Trace 0 failed: Thread(DoubleFork { thread_idx: 0, transaction_name: "add_double_fork", first_fork_stmt_id: stmt4, second_fork_stmt_id: stmt7 }) +Trace 0 failed: Thread(DoubleFork { thread_idx: 1, transaction_name: "add_double_fork", first_fork_stmt_id: stmt4, second_fork_stmt_id: stmt7 }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/double_fork_error.tx b/protocols/tests/adders/adder_d1/double_fork_error.tx index 0e59459a..b8883aba 100644 --- a/protocols/tests/adders/adder_d1/double_fork_error.tx +++ b/protocols/tests/adders/adder_d1/double_fork_error.tx @@ -1,4 +1,7 @@ +trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/double_fork_error.prot // RETURN: 101 add_double_fork(1, 2, 3); add_double_fork(4, 5, 9); + +} diff --git a/protocols/tests/adders/adder_d1/first_fail_second_norun.out b/protocols/tests/adders/adder_d1/first_fail_second_norun.out index d777153b..81103238 100644 --- a/protocols/tests/adders/adder_d1/first_fail_second_norun.out +++ b/protocols/tests/adders/adder_d1/first_fail_second_norun.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 14 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 4, RHS Value: 3 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr5, expr2_id: expr6, value1: ValueOwned(00000000000000000000000000000100), value2: ValueOwned(00000000000000000000000000000011) }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/first_fail_second_norun.tx b/protocols/tests/adders/adder_d1/first_fail_second_norun.tx index 2335a609..229a75b6 100644 --- a/protocols/tests/adders/adder_d1/first_fail_second_norun.tx +++ b/protocols/tests/adders/adder_d1/first_fail_second_norun.tx @@ -1,4 +1,7 @@ +trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 add(1, 2, 4); add(4, 5, 10); + +} diff --git a/protocols/tests/adders/adder_d1/first_thread_fails.out b/protocols/tests/adders/adder_d1/first_thread_fails.out index d777153b..81103238 100644 --- a/protocols/tests/adders/adder_d1/first_thread_fails.out +++ b/protocols/tests/adders/adder_d1/first_thread_fails.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 14 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 4, RHS Value: 3 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr5, expr2_id: expr6, value1: ValueOwned(00000000000000000000000000000100), value2: ValueOwned(00000000000000000000000000000011) }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/first_thread_fails.tx b/protocols/tests/adders/adder_d1/first_thread_fails.tx index fe20cedf..d3a2cd8f 100644 --- a/protocols/tests/adders/adder_d1/first_thread_fails.tx +++ b/protocols/tests/adders/adder_d1/first_thread_fails.tx @@ -1,4 +1,6 @@ +trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 add(1, 2, 4); -add(4, 5, 9); \ No newline at end of file +add(4, 5, 9); +} diff --git a/protocols/tests/adders/adder_d1/fork_before_step_error.out b/protocols/tests/adders/adder_d1/fork_before_step_error.out index 0e0c58c5..068911af 100644 --- a/protocols/tests/adders/adder_d1/fork_before_step_error.out +++ b/protocols/tests/adders/adder_d1/fork_before_step_error.out @@ -4,3 +4,5 @@ error: Thread 0 (transaction 'add_fork_before_step') called `fork()` before call 11 │ fork(); │ ^^^^^^^ Thread 0 (transaction 'add_fork_before_step') called `fork()` before calling `step()` +Trace 0 failed: Thread(ForkBeforeStep { thread_idx: 0, transaction_name: "add_fork_before_step", stmt_id: stmt3 }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/fork_before_step_error.tx b/protocols/tests/adders/adder_d1/fork_before_step_error.tx index a6ca997e..3ba3de97 100644 --- a/protocols/tests/adders/adder_d1/fork_before_step_error.tx +++ b/protocols/tests/adders/adder_d1/fork_before_step_error.tx @@ -1,4 +1,7 @@ +trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/fork_before_step_error.prot // RETURN: 101 add_fork_before_step(1, 2, 3); add_fork_before_step(4, 5, 9); + +} diff --git a/protocols/tests/adders/adder_d1/loop_with_assigns.out b/protocols/tests/adders/adder_d1/loop_with_assigns.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/adders/adder_d1/loop_with_assigns.out +++ b/protocols/tests/adders/adder_d1/loop_with_assigns.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/adders/adder_d1/loop_with_assigns.tx b/protocols/tests/adders/adder_d1/loop_with_assigns.tx index b701debb..a811100f 100644 --- a/protocols/tests/adders/adder_d1/loop_with_assigns.tx +++ b/protocols/tests/adders/adder_d1/loop_with_assigns.tx @@ -1,3 +1,6 @@ +trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/loop_with_assigns.prot 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 + +} diff --git a/protocols/tests/adders/adder_d1/nested_busy_wait.out b/protocols/tests/adders/adder_d1/nested_busy_wait.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/adders/adder_d1/nested_busy_wait.out +++ b/protocols/tests/adders/adder_d1/nested_busy_wait.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/adders/adder_d1/nested_busy_wait.tx b/protocols/tests/adders/adder_d1/nested_busy_wait.tx index cd16b841..6cd1b0ed 100644 --- a/protocols/tests/adders/adder_d1/nested_busy_wait.tx +++ b/protocols/tests/adders/adder_d1/nested_busy_wait.tx @@ -1,3 +1,6 @@ +trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/nested_busy_wait.prot 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 + +} diff --git a/protocols/tests/adders/adder_d1/second_thread_fails.out b/protocols/tests/adders/adder_d1/second_thread_fails.out index 181c1fd3..627708fc 100644 --- a/protocols/tests/adders/adder_d1/second_thread_fails.out +++ b/protocols/tests/adders/adder_d1/second_thread_fails.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 14 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 10, RHS Value: 9 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr5, expr2_id: expr6, value1: ValueOwned(00000000000000000000000000001010), value2: ValueOwned(00000000000000000000000000001001) }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/second_thread_fails.tx b/protocols/tests/adders/adder_d1/second_thread_fails.tx index bbd980e0..f648fd2a 100644 --- a/protocols/tests/adders/adder_d1/second_thread_fails.tx +++ b/protocols/tests/adders/adder_d1/second_thread_fails.tx @@ -1,4 +1,6 @@ +trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 add(1, 2, 3); -add(4, 5, 10); \ No newline at end of file +add(4, 5, 10); +} diff --git a/protocols/tests/adders/adder_d1/wait_and_add_correct.out b/protocols/tests/adders/adder_d1/wait_and_add_correct.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/adders/adder_d1/wait_and_add_correct.out +++ b/protocols/tests/adders/adder_d1/wait_and_add_correct.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/adders/adder_d1/wait_and_add_correct.tx b/protocols/tests/adders/adder_d1/wait_and_add_correct.tx index 16951564..773a4b58 100644 --- a/protocols/tests/adders/adder_d1/wait_and_add_correct.tx +++ b/protocols/tests/adders/adder_d1/wait_and_add_correct.tx @@ -1,4 +1,7 @@ +trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 0 wait_and_add(1, 2, 3); add(4, 5, 9); + +} diff --git a/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.out b/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.out index 1cf5f891..df6b2059 100644 --- a/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.out +++ b/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.out @@ -10,3 +10,6 @@ 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 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000100), new_value: ValueOwned(00000000000000000000000000000001), thread_idx: 0, transaction_name: "wait_and_add", stmt_id: stmt4 }) +Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000001), new_value: ValueOwned(00000000000000000000000000000100), thread_idx: 1, transaction_name: "add_incorrect_implicit", stmt_id: stmt1 }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.tx b/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.tx index 509827d5..4530d130 100644 --- a/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.tx +++ b/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.tx @@ -1,4 +1,7 @@ +trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 wait_and_add(1, 2, 3); add_incorrect_implicit(4, 5, 9); + +} diff --git a/protocols/tests/adders/adder_d2/both_threads_pass.out b/protocols/tests/adders/adder_d2/both_threads_pass.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/adders/adder_d2/both_threads_pass.out +++ b/protocols/tests/adders/adder_d2/both_threads_pass.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/adders/adder_d2/both_threads_pass.tx b/protocols/tests/adders/adder_d2/both_threads_pass.tx index 81ec54f1..3013a8eb 100644 --- a/protocols/tests/adders/adder_d2/both_threads_pass.tx +++ b/protocols/tests/adders/adder_d2/both_threads_pass.tx @@ -1,4 +1,7 @@ +trace { // ARGS: --verilog adders/adder_d2/add_d2.v --protocol adders/adder_d2/add_d2.prot --max-steps 4 // RETURN: 0 add(1, 2, 3); add(4, 5, 9); + +} diff --git a/protocols/tests/adders/adder_d2/no_dontcare_conflict.out b/protocols/tests/adders/adder_d2/no_dontcare_conflict.out index 58bc092e..e43c2cc0 100644 --- a/protocols/tests/adders/adder_d2/no_dontcare_conflict.out +++ b/protocols/tests/adders/adder_d2/no_dontcare_conflict.out @@ -10,3 +10,6 @@ error: Thread 1 (`add`) attempted conflicting assignment to 'a': current=1, new= 12 │ DUT.a := a; │ ^^^^^^^^^^^ Thread 1 (`add`) attempted conflicting assignment to 'a': current=1, new=4 +Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000100), new_value: ValueOwned(00000000000000000000000000000001), thread_idx: 0, transaction_name: "add", stmt_id: stmt1 }) +Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000001), new_value: ValueOwned(00000000000000000000000000000100), thread_idx: 1, transaction_name: "add", stmt_id: stmt1 }) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d2/no_dontcare_conflict.tx b/protocols/tests/adders/adder_d2/no_dontcare_conflict.tx index 07822946..0939aca2 100644 --- a/protocols/tests/adders/adder_d2/no_dontcare_conflict.tx +++ b/protocols/tests/adders/adder_d2/no_dontcare_conflict.tx @@ -1,4 +1,7 @@ +trace { // ARGS: --verilog adders/adder_d2/add_d2.v --protocol adders/adder_d2/no_dontcare_conflict.prot // RETURN: 101 add(1, 2, 3); add(4, 5, 9); + +} diff --git a/protocols/tests/alus/alu_d1.out b/protocols/tests/alus/alu_d1.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/alus/alu_d1.out +++ b/protocols/tests/alus/alu_d1.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/alus/alu_d1.tx b/protocols/tests/alus/alu_d1.tx index fc5f1692..6bbfe8a9 100644 --- a/protocols/tests/alus/alu_d1.tx +++ b/protocols/tests/alus/alu_d1.tx @@ -1,6 +1,9 @@ +trace { // ARGS: --verilog=alus/alu_d1.v --protocol=alus/alu_d1.prot --module alu_d1 add(1, 2, 3); add(123, 245, 368); sub(200, 200, 0); and(100, 100, 100); or(0, 230, 230); + +} diff --git a/protocols/tests/alus/alu_d2.out b/protocols/tests/alus/alu_d2.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/alus/alu_d2.out +++ b/protocols/tests/alus/alu_d2.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/alus/alu_d2.tx b/protocols/tests/alus/alu_d2.tx index 32554397..ebc6a596 100644 --- a/protocols/tests/alus/alu_d2.tx +++ b/protocols/tests/alus/alu_d2.tx @@ -1,6 +1,9 @@ +trace { // ARGS: --verilog=alus/alu_d2.v --protocol=alus/alu_d2.prot --module alu_d2 add(1, 2, 3); add(123, 245, 368); sub(200, 200, 0); and(100, 100, 100); or(0, 230, 230); + +} diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.out b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.out index 39bc4515..015c6f2d 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.out +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 10 │ assert_eq(data_out, dut.output_data); │ ^^^^^^^^^^^^^^^^^^^^^^^^^ LHS Value: 2047, RHS Value: 0 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr2, expr2_id: expr3, value1: ValueOwned(11111111111), value2: ValueOwned(00000000000) }) +Trace 0 execution failed. diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.tx b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.tx index b9ec6026..acf66cde 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.tx +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.tx @@ -1,3 +1,5 @@ +trace { // ARGS: --verilog=brave_new_world/bit_truncation/bit_truncation_fft_bug.v --protocol=brave_new_world/bit_truncation/bit_truncation_fft.prot --module bit_truncation_fft_bug // RETURN: 101 -bit_truncation_fft(8386560, 2047); \ No newline at end of file +bit_truncation_fft(8386560, 2047); +} diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.out b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.out +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.tx b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.tx index d9427085..c2145282 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.tx +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.tx @@ -1,2 +1,4 @@ +trace { // ARGS: --verilog=brave_new_world/bit_truncation/bit_truncation_fft_fix.v --protocol=brave_new_world/bit_truncation/bit_truncation_fft.prot --module round11_rne_unsigned_fixed -bit_truncation_fft(8386560, 2047); \ No newline at end of file +bit_truncation_fft(8386560, 2047); +} diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.out b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.out index 89ecef55..c06584bc 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.out +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 9 │ assert_eq(data_out, dut.left); │ ^^^^^^^^^^^^^^^^^^ LHS Value: 68719476736, RHS Value: 0 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr2, expr2_id: expr3, value1: ValueOwned(000001000000000000000000000000000000000000), value2: ValueOwned(000000000000000000000000000000000000000000) }) +Trace 0 execution failed. diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.tx b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.tx index ee78387c..ecd45a2c 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.tx +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.tx @@ -1,3 +1,5 @@ +trace { // ARGS: --verilog=brave_new_world/bit_truncation/bit_truncation_sha_bug.v --protocol=brave_new_world/bit_truncation/bit_truncation_sha.prot --module bit_truncation_sha_bug // RETURN: 101 -bit_truncation_sha(4398046511104, 68719476736); \ No newline at end of file +bit_truncation_sha(4398046511104, 68719476736); +} diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.out b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.out +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.tx b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.tx index f59313f9..bd3a9004 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.tx +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.tx @@ -1,2 +1,4 @@ +trace { // ARGS: --verilog=brave_new_world/bit_truncation/bit_truncation_sha_fix.v --protocol=brave_new_world/bit_truncation/bit_truncation_sha.prot --module bit_truncation_sha_fixed -bit_truncation_sha(4398046511104, 68719476736); \ No newline at end of file +bit_truncation_sha(4398046511104, 68719476736); +} diff --git a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.out b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.out index 24c950e5..7d45fbf6 100644 --- a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.out +++ b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 29 │ assert_eq(dut.valid, 1'b0); │ ^^^^^^^^^^^^^^^ LHS Value: 1, RHS Value: 0 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr9, expr2_id: expr10, value1: ValueOwned(1), value2: ValueOwned(0) }) +Trace 0 execution failed. diff --git a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.tx b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.tx index 2e197702..8c1fd7be 100644 --- a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.tx +++ b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.tx @@ -1,3 +1,5 @@ +trace { // ARGS: --verilog=brave_new_world/failure_to_update/ftu_sha_bug.v --protocol=brave_new_world/failure_to_update/ftu_sha.prot --module fsm_update_buggy // RETURN: 101 -failure_to_update_sha(); \ No newline at end of file +failure_to_update_sha(); +} diff --git a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.out b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.out +++ b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.tx b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.tx index 7bbd2a91..20c289ad 100644 --- a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.tx +++ b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.tx @@ -1,2 +1,4 @@ +trace { // ARGS: --verilog=brave_new_world/failure_to_update/ftu_sha_fix.v --protocol=brave_new_world/failure_to_update/ftu_sha.prot --module fsm_update_fixed_gated -failure_to_update_sha(); \ No newline at end of file +failure_to_update_sha(); +} diff --git a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.out b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.out index 2cf2e4f6..ba5a1a89 100644 --- a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.out +++ b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 18 │ assert_eq(data_out, dut.final_resp); │ ^^^^^^^^^^^^^^^^^^^^^^^^ LHS Value: 7, RHS Value: 0 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr6, expr2_id: expr7, value1: ValueOwned(00000000000000000000000000000111), value2: ValueOwned(00000000000000000000000000000000) }) +Trace 0 execution failed. diff --git a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.tx b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.tx index 4761c12b..2a792bc0 100644 --- a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.tx +++ b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.tx @@ -1,3 +1,5 @@ +trace { // ARGS: --verilog=brave_new_world/signal_asynchrony/signal_async_bug.v --protocol=brave_new_world/signal_asynchrony/signal_async.prot --module signal_async_bug // RETURN: 101 -signal_async(6, 7); \ No newline at end of file +signal_async(6, 7); +} diff --git a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.out b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.out +++ b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.tx b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.tx index 685bcd63..c4fd3abb 100644 --- a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.tx +++ b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.tx @@ -1,2 +1,4 @@ +trace { // ARGS: --verilog=brave_new_world/signal_asynchrony/signal_async_fix.v --protocol=brave_new_world/signal_asynchrony/signal_async.prot --module signal_async_fix -signal_async(6, 7); \ No newline at end of file +signal_async(6, 7); +} diff --git a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.out b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.out index 65fae905..6ea5a165 100644 --- a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.out +++ b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 16 │ assert_eq(data_out, dut.sum); │ ^^^^^^^^^^^^^^^^^ LHS Value: 5, RHS Value: 15 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr4, expr2_id: expr5, value1: ValueOwned(00000000000000000000000000000101), value2: ValueOwned(00000000000000000000000000001111) }) +Trace 0 execution failed. diff --git a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.tx b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.tx index 70ebb55a..d2989a2b 100644 --- a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.tx +++ b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.tx @@ -1,3 +1,5 @@ +trace { // ARGS: --verilog=brave_new_world/use_without_valid/use_without_valid_bug.v --protocol=brave_new_world/use_without_valid/use_without_valid.prot --module use_without_valid_bug // RETURN: 101 -use_without_valid(5, 5); \ No newline at end of file +use_without_valid(5, 5); +} diff --git a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.out b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.out +++ b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.tx b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.tx index 61c7851e..b674dbf2 100644 --- a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.tx +++ b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.tx @@ -1,2 +1,4 @@ +trace { // ARGS: --verilog=brave_new_world/use_without_valid/use_without_valid_fix.v --protocol=brave_new_world/use_without_valid/use_without_valid.prot --module use_without_valid_fix -use_without_valid(5, 5); \ No newline at end of file +use_without_valid(5, 5); +} diff --git a/protocols/tests/counters/counter.out b/protocols/tests/counters/counter.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/counters/counter.out +++ b/protocols/tests/counters/counter.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/counters/counter.tx b/protocols/tests/counters/counter.tx index 2f205364..1fc4a509 100644 --- a/protocols/tests/counters/counter.tx +++ b/protocols/tests/counters/counter.tx @@ -1,2 +1,5 @@ +trace { // ARGS: --verilog counters/counter.v --protocol counters/counter.prot count_up(10); + +} diff --git a/protocols/tests/fifo/fifo.out b/protocols/tests/fifo/fifo.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/fifo/fifo.out +++ b/protocols/tests/fifo/fifo.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/fifo/fifo.tx b/protocols/tests/fifo/fifo.tx index aca3b397..eabe10ae 100644 --- a/protocols/tests/fifo/fifo.tx +++ b/protocols/tests/fifo/fifo.tx @@ -1,3 +1,4 @@ +trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo.prot --module fifo_wrapper reset(); push(3); @@ -5,3 +6,5 @@ push(4); idle(); pop(3); pop(4); + +} diff --git a/protocols/tests/fifo/pop_before_push_fail.out b/protocols/tests/fifo/pop_before_push_fail.out index 8b9c925b..bc91e459 100644 --- a/protocols/tests/fifo/pop_before_push_fail.out +++ b/protocols/tests/fifo/pop_before_push_fail.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 43 │ assert_eq(DUT.data_o, output); │ ^^^^^^^^^^^^^^^^^^ LHS Value: 0, RHS Value: 3 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr8, expr2_id: expr9, value1: ValueOwned(00000000000000000000000000000000), value2: ValueOwned(00000000000000000000000000000011) }) +Trace 0 execution failed. diff --git a/protocols/tests/fifo/pop_before_push_fail.tx b/protocols/tests/fifo/pop_before_push_fail.tx index a88c4af0..c6a9fcc0 100644 --- a/protocols/tests/fifo/pop_before_push_fail.tx +++ b/protocols/tests/fifo/pop_before_push_fail.tx @@ -1,3 +1,4 @@ +trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo.prot --module fifo_wrapper // RETURN: 101 @@ -6,4 +7,5 @@ push(4); pop(4); idle(); pop(3); // this line should fail since we're trying to `pop` a non-existent value -push(3); \ No newline at end of file +push(3); +} diff --git a/protocols/tests/fifo/pop_empty_fail.out b/protocols/tests/fifo/pop_empty_fail.out index 8b9c925b..bc91e459 100644 --- a/protocols/tests/fifo/pop_empty_fail.out +++ b/protocols/tests/fifo/pop_empty_fail.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 43 │ assert_eq(DUT.data_o, output); │ ^^^^^^^^^^^^^^^^^^ LHS Value: 0, RHS Value: 3 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr8, expr2_id: expr9, value1: ValueOwned(00000000000000000000000000000000), value2: ValueOwned(00000000000000000000000000000011) }) +Trace 0 execution failed. diff --git a/protocols/tests/fifo/pop_empty_fail.tx b/protocols/tests/fifo/pop_empty_fail.tx index d70a215d..a2154ec6 100644 --- a/protocols/tests/fifo/pop_empty_fail.tx +++ b/protocols/tests/fifo/pop_empty_fail.tx @@ -1,6 +1,8 @@ +trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo.prot --module fifo_wrapper // RETURN: 101 reset(); pop(3); // this line should fail since we're trying to `pop` an empty FIFO -push(3); \ No newline at end of file +push(3); +} diff --git a/protocols/tests/fifo/push_pop_conflict.out b/protocols/tests/fifo/push_pop_conflict.out index bddcdc3e..4ef05cb5 100644 --- a/protocols/tests/fifo/push_pop_conflict.out +++ b/protocols/tests/fifo/push_pop_conflict.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 43 │ assert_eq(DUT.data_o, output); │ ^^^^^^^^^^^^^^^^^^ LHS Value: 2, RHS Value: 3 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr8, expr2_id: expr9, value1: ValueOwned(00000000000000000000000000000010), value2: ValueOwned(00000000000000000000000000000011) }) +Trace 0 execution failed. diff --git a/protocols/tests/fifo/push_pop_conflict.tx b/protocols/tests/fifo/push_pop_conflict.tx index a3d69597..c790f136 100644 --- a/protocols/tests/fifo/push_pop_conflict.tx +++ b/protocols/tests/fifo/push_pop_conflict.tx @@ -1,6 +1,9 @@ +trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo.prot --module fifo_wrapper // RETURN: 101 reset(); push(2); pop(3); // this line should fail, since 3 isn't in the FIFO + +} diff --git a/protocols/tests/fifo/push_pop_identity_ok.out b/protocols/tests/fifo/push_pop_identity_ok.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/fifo/push_pop_identity_ok.out +++ b/protocols/tests/fifo/push_pop_identity_ok.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/fifo/push_pop_identity_ok.tx b/protocols/tests/fifo/push_pop_identity_ok.tx index e832de41..db7e4442 100644 --- a/protocols/tests/fifo/push_pop_identity_ok.tx +++ b/protocols/tests/fifo/push_pop_identity_ok.tx @@ -1,3 +1,4 @@ +trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo.prot --module fifo_wrapper reset(); @@ -5,4 +6,5 @@ push(2); pop(2); idle(); push(3); -pop(3); \ No newline at end of file +pop(3); +} diff --git a/protocols/tests/fifo/push_pop_loop_empty.out b/protocols/tests/fifo/push_pop_loop_empty.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/fifo/push_pop_loop_empty.out +++ b/protocols/tests/fifo/push_pop_loop_empty.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/fifo/push_pop_loop_empty.tx b/protocols/tests/fifo/push_pop_loop_empty.tx index 89573579..a85ae512 100644 --- a/protocols/tests/fifo/push_pop_loop_empty.tx +++ b/protocols/tests/fifo/push_pop_loop_empty.tx @@ -1,5 +1,8 @@ +trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo_bounded_loop.prot --module fifo_wrapper reset(); push_n_times(42, 4); // Push 42 four times pop_n_times(42, 4); // Pop four times check_empty(); // FIFO should be empty after pushing and popping the same no. of times + +} diff --git a/protocols/tests/fifo/push_pop_loop_not_empty.out b/protocols/tests/fifo/push_pop_loop_not_empty.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/fifo/push_pop_loop_not_empty.out +++ b/protocols/tests/fifo/push_pop_loop_not_empty.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/fifo/push_pop_loop_not_empty.tx b/protocols/tests/fifo/push_pop_loop_not_empty.tx index 284d37de..a99b1ea1 100644 --- a/protocols/tests/fifo/push_pop_loop_not_empty.tx +++ b/protocols/tests/fifo/push_pop_loop_not_empty.tx @@ -1,5 +1,8 @@ +trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo_bounded_loop.prot --module fifo_wrapper reset(); push_n_times(7, 3); pop_n_times(7, 2); check_not_empty(); // FIFO is non-empty (has one element remaining) + +} diff --git a/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.out b/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.out index b5b23005..9eb2f39c 100644 --- a/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.out +++ b/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.out @@ -4,3 +4,5 @@ error: Cannot assign to forbidden input 'b' after observing a combinationally de 24 │ dut.b := b; │ ^ Cannot assign to forbidden input 'b' after observing a combinationally dependent output +Trace 0 failed: Evaluation(ForbiddenInputAssignment { input_name: "b", expr_id: expr7 }) +Trace 0 execution failed. diff --git a/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.tx b/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.tx index 625f6b79..eaf23f90 100644 --- a/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.tx +++ b/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.tx @@ -1,3 +1,4 @@ +trace { // ARGS: --verilog identities/dual_identity_d0/dual_identity_d0.v --protocol identities/dual_identity_d0/dual_identity_d0.prot // RETURN: 101 // This test demonstrates how combinational dependency tracking should catch @@ -6,3 +7,5 @@ // Observing s2 should forbid assignments to b, but both branches assign to b. // With comb dependency tracking: should error with "ASSIGNED FORBIDDEN PORT" identity(1, 1); + +} diff --git a/protocols/tests/identities/dual_identity_d1/dual_identity_d1.tx b/protocols/tests/identities/dual_identity_d1/dual_identity_d1.tx index 496a95d8..98932f1e 100644 --- a/protocols/tests/identities/dual_identity_d1/dual_identity_d1.tx +++ b/protocols/tests/identities/dual_identity_d1/dual_identity_d1.tx @@ -1,4 +1,7 @@ +trace { // ARGS: --verilog identities/dual_identity_d1/dual_identity_d1.v --protocol identities/dual_identity_d1/dual_identity_d1.prot // RETURN: 1 one(3); two(2, 3); + +} diff --git a/protocols/tests/identities/identity_d0/passthrough_combdep.out b/protocols/tests/identities/identity_d0/passthrough_combdep.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/identities/identity_d0/passthrough_combdep.out +++ b/protocols/tests/identities/identity_d0/passthrough_combdep.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/identities/identity_d0/passthrough_combdep.tx b/protocols/tests/identities/identity_d0/passthrough_combdep.tx index 51051293..e7bebdc7 100644 --- a/protocols/tests/identities/identity_d0/passthrough_combdep.tx +++ b/protocols/tests/identities/identity_d0/passthrough_combdep.tx @@ -1,3 +1,6 @@ +trace { // ARGS: --verilog identities/identity_d0/identity_d0.v --protocol identities/identity_d0/identity_d0.prot // RETURN: 0 passthrough(); + +} diff --git a/protocols/tests/identities/identity_d1/explicit_fork.out b/protocols/tests/identities/identity_d1/explicit_fork.out index 860a4602..0ab2a325 100644 --- a/protocols/tests/identities/identity_d1/explicit_fork.out +++ b/protocols/tests/identities/identity_d1/explicit_fork.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 12 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 4, RHS Value: 3 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr3, expr2_id: expr4, value1: ValueOwned(00000000000000000000000000000100), value2: ValueOwned(00000000000000000000000000000011) }) +Trace 0 execution failed. diff --git a/protocols/tests/identities/identity_d1/explicit_fork.tx b/protocols/tests/identities/identity_d1/explicit_fork.tx index 24fc8c77..bde62664 100644 --- a/protocols/tests/identities/identity_d1/explicit_fork.tx +++ b/protocols/tests/identities/identity_d1/explicit_fork.tx @@ -1,6 +1,9 @@ +trace { // ARGS: --verilog identities/identity_d1/identity_d1.v --protocol identities/identity_d1/identity_d1.prot // RETURN: 101 explicit_fork(1, 1); explicit_fork(2, 2); explicit_fork(3, 4); explicit_fork(4, 4); + +} diff --git a/protocols/tests/identities/identity_d1/slicing_err.tx b/protocols/tests/identities/identity_d1/slicing_err.tx index e2b6b5d5..4d94831c 100644 --- a/protocols/tests/identities/identity_d1/slicing_err.tx +++ b/protocols/tests/identities/identity_d1/slicing_err.tx @@ -1,3 +1,5 @@ +trace { // ARGS: --verilog identities/identity_d1/identity_d1.v --protocol identities/identity_d1/slicing_err.prot // RETURN: 1 -slicing_err(1, 1); \ No newline at end of file +slicing_err(1, 1); +} diff --git a/protocols/tests/identities/identity_d1/slicing_invalid.tx b/protocols/tests/identities/identity_d1/slicing_invalid.tx index 06a8ed0c..c72f46bf 100644 --- a/protocols/tests/identities/identity_d1/slicing_invalid.tx +++ b/protocols/tests/identities/identity_d1/slicing_invalid.tx @@ -1,3 +1,5 @@ +trace { // ARGS: --verilog identities/identity_d1/identity_d1.v --protocol identities/identity_d1/slicing_invalid.prot // RETURN: 1 -slicing_invalid(1, 1); \ No newline at end of file +slicing_invalid(1, 1); +} diff --git a/protocols/tests/identities/identity_d1/slicing_ok.out b/protocols/tests/identities/identity_d1/slicing_ok.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/identities/identity_d1/slicing_ok.out +++ b/protocols/tests/identities/identity_d1/slicing_ok.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/identities/identity_d1/slicing_ok.tx b/protocols/tests/identities/identity_d1/slicing_ok.tx index dd269f4d..8fb72543 100644 --- a/protocols/tests/identities/identity_d1/slicing_ok.tx +++ b/protocols/tests/identities/identity_d1/slicing_ok.tx @@ -1,2 +1,4 @@ +trace { // ARGS: --verilog identities/identity_d1/identity_d1.v --protocol identities/identity_d1/identity_d1.prot -slicing_ok(1, 1); \ No newline at end of file +slicing_ok(1, 1); +} diff --git a/protocols/tests/identities/identity_d2/single_thread_passes.out b/protocols/tests/identities/identity_d2/single_thread_passes.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/identities/identity_d2/single_thread_passes.out +++ b/protocols/tests/identities/identity_d2/single_thread_passes.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/identities/identity_d2/single_thread_passes.tx b/protocols/tests/identities/identity_d2/single_thread_passes.tx index a51f300c..b7c97043 100644 --- a/protocols/tests/identities/identity_d2/single_thread_passes.tx +++ b/protocols/tests/identities/identity_d2/single_thread_passes.tx @@ -1,2 +1,5 @@ +trace { // ARGS: --verilog identities/identity_d2/identity_d2.v --protocol identities/identity_d2/identity_d2.prot multiple_assign(1, 1); + +} diff --git a/protocols/tests/identities/identity_d2/two_assignments_same_value.out b/protocols/tests/identities/identity_d2/two_assignments_same_value.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/identities/identity_d2/two_assignments_same_value.out +++ b/protocols/tests/identities/identity_d2/two_assignments_same_value.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/identities/identity_d2/two_assignments_same_value.tx b/protocols/tests/identities/identity_d2/two_assignments_same_value.tx index 6fc54522..bea1e3ec 100644 --- a/protocols/tests/identities/identity_d2/two_assignments_same_value.tx +++ b/protocols/tests/identities/identity_d2/two_assignments_same_value.tx @@ -1,3 +1,6 @@ +trace { // ARGS: --verilog identities/identity_d2/identity_d2.v --protocol identities/identity_d2/identity_d2.prot multiple_assign(1, 1); multiple_assign(1, 1); + +} diff --git a/protocols/tests/identities/identity_d2/two_different_assignments_error.out b/protocols/tests/identities/identity_d2/two_different_assignments_error.out index 6281ccf4..e5ce19db 100644 --- a/protocols/tests/identities/identity_d2/two_different_assignments_error.out +++ b/protocols/tests/identities/identity_d2/two_different_assignments_error.out @@ -10,3 +10,6 @@ error: Thread 1 (`multiple_assign`) attempted conflicting assignment to 'a': cur 9 │ DUT.a := a; │ ^^^^^^^^^^^ Thread 1 (`multiple_assign`) attempted conflicting assignment to 'a': current=1, new=2 +Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000010), new_value: ValueOwned(00000000000000000000000000000001), thread_idx: 0, transaction_name: "multiple_assign", stmt_id: stmt4 }) +Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000001), new_value: ValueOwned(00000000000000000000000000000010), thread_idx: 1, transaction_name: "multiple_assign", stmt_id: stmt1 }) +Trace 0 execution failed. diff --git a/protocols/tests/identities/identity_d2/two_different_assignments_error.tx b/protocols/tests/identities/identity_d2/two_different_assignments_error.tx index e97b5c1c..2c49dc78 100644 --- a/protocols/tests/identities/identity_d2/two_different_assignments_error.tx +++ b/protocols/tests/identities/identity_d2/two_different_assignments_error.tx @@ -1,4 +1,7 @@ +trace { // ARGS: --verilog identities/identity_d2/identity_d2.v --protocol identities/identity_d2/identity_d2.prot // RETURN: 101 multiple_assign(1, 1); multiple_assign(2, 2); + +} diff --git a/protocols/tests/identities/identity_d2/two_fork_err.out b/protocols/tests/identities/identity_d2/two_fork_err.out index 49c327d2..b7b891f3 100644 --- a/protocols/tests/identities/identity_d2/two_fork_err.out +++ b/protocols/tests/identities/identity_d2/two_fork_err.out @@ -7,3 +7,5 @@ error: Thread 0 (transaction 'two_fork_err') attempted to fork more than once 25 │ fork(); │ ^^^^^^^ second fork() called here +Trace 0 failed: Thread(DoubleFork { thread_idx: 0, transaction_name: "two_fork_err", first_fork_stmt_id: stmt3, second_fork_stmt_id: stmt6 }) +Trace 0 execution failed. diff --git a/protocols/tests/identities/identity_d2/two_fork_err.tx b/protocols/tests/identities/identity_d2/two_fork_err.tx index 4f175d5f..2e5bc00b 100644 --- a/protocols/tests/identities/identity_d2/two_fork_err.tx +++ b/protocols/tests/identities/identity_d2/two_fork_err.tx @@ -1,3 +1,6 @@ +trace { // ARGS: --verilog identities/identity_d2/identity_d2.v --protocol identities/identity_d2/identity_d2.prot // RETURN: 101 two_fork_err(1, 1); + +} diff --git a/protocols/tests/identities/identity_d2/two_fork_ill_formed.tx b/protocols/tests/identities/identity_d2/two_fork_ill_formed.tx index 0dfba0d7..2ae6f28b 100644 --- a/protocols/tests/identities/identity_d2/two_fork_ill_formed.tx +++ b/protocols/tests/identities/identity_d2/two_fork_ill_formed.tx @@ -1,3 +1,6 @@ +trace { // ARGS: --verilog identities/identity_d2/identity_d2.v --protocol identities/identity_d2/two_fork_ill_formed.prot // RETURN: 1 two_fork_ok(1, 1); + +} diff --git a/protocols/tests/inverters/inverter_d0.out b/protocols/tests/inverters/inverter_d0.out index b59ab5dc..575a48c8 100644 --- a/protocols/tests/inverters/inverter_d0.out +++ b/protocols/tests/inverters/inverter_d0.out @@ -4,3 +4,5 @@ error: Output 'DUT.s' depends on input(s) 'DUT.a' which do not have assigned val 7 │ DUT.a := DUT.s; │ ^^^^^ Output 'DUT.s' depends on input(s) 'DUT.a' which do not have assigned values ('DUT.a' initialized to DontCare and were never assigned a concrete value) +Trace 0 failed: Evaluation(ForbiddenPortRead { port_name: "DUT.s", unassigned_inputs: [("DUT.a", None)], expr_id: expr1 }) +Trace 0 execution failed. diff --git a/protocols/tests/inverters/inverter_d0.tx b/protocols/tests/inverters/inverter_d0.tx index 4a527b1b..eb95ba13 100644 --- a/protocols/tests/inverters/inverter_d0.tx +++ b/protocols/tests/inverters/inverter_d0.tx @@ -1,3 +1,6 @@ +trace { // ARGS: --verilog inverters/inverter_d0.v --protocol inverters/inverter_d0.prot // RETURN: 101 invert(0, 1); + +} diff --git a/protocols/tests/multi/multi0/multi0.out b/protocols/tests/multi/multi0/multi0.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/multi/multi0/multi0.out +++ b/protocols/tests/multi/multi0/multi0.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/multi/multi0/multi0.tx b/protocols/tests/multi/multi0/multi0.tx index ad63d159..0470861b 100644 --- a/protocols/tests/multi/multi0/multi0.tx +++ b/protocols/tests/multi/multi0/multi0.tx @@ -1,2 +1,5 @@ +trace { // ARGS: --verilog multi/multi0/multi0.v --protocol multi/multi0/multi0.prot --module multi0 multi(10, 10); + +} diff --git a/protocols/tests/multi/multi0keep/multi0keep.out b/protocols/tests/multi/multi0keep/multi0keep.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/multi/multi0keep/multi0keep.out +++ b/protocols/tests/multi/multi0keep/multi0keep.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/multi/multi0keep/multi0keep.tx b/protocols/tests/multi/multi0keep/multi0keep.tx index 75597708..cfbabb05 100644 --- a/protocols/tests/multi/multi0keep/multi0keep.tx +++ b/protocols/tests/multi/multi0keep/multi0keep.tx @@ -1,2 +1,5 @@ +trace { // ARGS: --verilog multi/multi0keep/multi0keep.v --protocol multi/multi0keep/multi0keep.prot --module multi0keep multi(10, 10); + +} diff --git a/protocols/tests/multi/multi0keep2const/multi0keep2const.out b/protocols/tests/multi/multi0keep2const/multi0keep2const.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/multi/multi0keep2const/multi0keep2const.out +++ b/protocols/tests/multi/multi0keep2const/multi0keep2const.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/multi/multi0keep2const/multi0keep2const.tx b/protocols/tests/multi/multi0keep2const/multi0keep2const.tx index fb53a658..10aaf230 100644 --- a/protocols/tests/multi/multi0keep2const/multi0keep2const.tx +++ b/protocols/tests/multi/multi0keep2const/multi0keep2const.tx @@ -1,2 +1,5 @@ +trace { // ARGS: --verilog multi/multi0keep2const/multi0keep2const.v multi/multi0keep/multi0keep.v --protocol multi/multi0keep2const/multi0keep2const.prot --module multi0keep2const multi(10, 10); + +} diff --git a/protocols/tests/multi/multi2const/multi2const.out b/protocols/tests/multi/multi2const/multi2const.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/multi/multi2const/multi2const.out +++ b/protocols/tests/multi/multi2const/multi2const.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/multi/multi2const/multi2const.tx b/protocols/tests/multi/multi2const/multi2const.tx index 5ba85073..0f34956f 100644 --- a/protocols/tests/multi/multi2const/multi2const.tx +++ b/protocols/tests/multi/multi2const/multi2const.tx @@ -1,2 +1,5 @@ +trace { // ARGS: --verilog multi/multi2const/multi2const.v multi/multi0/multi0.v --protocol multi/multi2const/multi2const.prot --module multi2const multi(10, 10); + +} diff --git a/protocols/tests/multi/multi2multi/multi2multi.out b/protocols/tests/multi/multi2multi/multi2multi.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/multi/multi2multi/multi2multi.out +++ b/protocols/tests/multi/multi2multi/multi2multi.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/multi/multi2multi/multi2multi.tx b/protocols/tests/multi/multi2multi/multi2multi.tx index d4777b49..f9fe3b70 100644 --- a/protocols/tests/multi/multi2multi/multi2multi.tx +++ b/protocols/tests/multi/multi2multi/multi2multi.tx @@ -1,2 +1,5 @@ +trace { // ARGS: --verilog multi/multi2multi/multi2multi.v multi/multi0/multi0.v --protocol multi/multi2multi/multi2multi.prot --module multi2multi multi(10, 10); + +} diff --git a/protocols/tests/multi/multi_data/multi_data.out b/protocols/tests/multi/multi_data/multi_data.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/multi/multi_data/multi_data.out +++ b/protocols/tests/multi/multi_data/multi_data.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/multi/multi_data/multi_data.tx b/protocols/tests/multi/multi_data/multi_data.tx index 700452cf..a13b8e6d 100644 --- a/protocols/tests/multi/multi_data/multi_data.tx +++ b/protocols/tests/multi/multi_data/multi_data.tx @@ -1,2 +1,5 @@ +trace { // ARGS: --verilog multi/multi_data/multi_data.v --protocol multi/multi_data/multi_data.prot multi(10, 10); + +} diff --git a/protocols/tests/multipliers/mult_d2/both_threads_fail.out b/protocols/tests/multipliers/mult_d2/both_threads_fail.out index b095a57b..d1f62fcb 100644 --- a/protocols/tests/multipliers/mult_d2/both_threads_fail.out +++ b/protocols/tests/multipliers/mult_d2/both_threads_fail.out @@ -10,3 +10,6 @@ error: The two expressions did not evaluate to the same value 22 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 47, RHS Value: 48 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr7, expr2_id: expr8, value1: ValueOwned(00000000000000000000000000000011), value2: ValueOwned(00000000000000000000000000000010) }) +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr7, expr2_id: expr8, value1: ValueOwned(00000000000000000000000000101111), value2: ValueOwned(00000000000000000000000000110000) }) +Trace 0 execution failed. diff --git a/protocols/tests/multipliers/mult_d2/both_threads_fail.tx b/protocols/tests/multipliers/mult_d2/both_threads_fail.tx index 4cbe4fe4..ec23026b 100644 --- a/protocols/tests/multipliers/mult_d2/both_threads_fail.tx +++ b/protocols/tests/multipliers/mult_d2/both_threads_fail.tx @@ -1,6 +1,9 @@ +trace { // ARGS: --verilog multipliers/mult_d2/mult_d2.v --protocol multipliers/mult_d2/mult_d2.prot // RETURN: 101 mul(1, 2, 3); mul(6, 8, 47); + +} diff --git a/protocols/tests/multipliers/mult_d2/both_threads_pass.out b/protocols/tests/multipliers/mult_d2/both_threads_pass.out index c6eb0316..f5f6cb49 100644 --- a/protocols/tests/multipliers/mult_d2/both_threads_pass.out +++ b/protocols/tests/multipliers/mult_d2/both_threads_pass.out @@ -1 +1 @@ -Protocol executed successfully! +Trace 0 executed successfully! diff --git a/protocols/tests/multipliers/mult_d2/both_threads_pass.tx b/protocols/tests/multipliers/mult_d2/both_threads_pass.tx index dabd0e7d..9ab45831 100644 --- a/protocols/tests/multipliers/mult_d2/both_threads_pass.tx +++ b/protocols/tests/multipliers/mult_d2/both_threads_pass.tx @@ -1,3 +1,6 @@ +trace { // ARGS: --verilog multipliers/mult_d2/mult_d2.v --protocol multipliers/mult_d2/mult_d2.prot mul(1, 2, 2); mul(6, 8, 48); + +} diff --git a/protocols/tests/multipliers/mult_d2/first_thread_fails.out b/protocols/tests/multipliers/mult_d2/first_thread_fails.out index 2e83c080..9c5317fa 100644 --- a/protocols/tests/multipliers/mult_d2/first_thread_fails.out +++ b/protocols/tests/multipliers/mult_d2/first_thread_fails.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 22 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 3, RHS Value: 2 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr7, expr2_id: expr8, value1: ValueOwned(00000000000000000000000000000011), value2: ValueOwned(00000000000000000000000000000010) }) +Trace 0 execution failed. diff --git a/protocols/tests/multipliers/mult_d2/first_thread_fails.tx b/protocols/tests/multipliers/mult_d2/first_thread_fails.tx index 422acf37..b6205f97 100644 --- a/protocols/tests/multipliers/mult_d2/first_thread_fails.tx +++ b/protocols/tests/multipliers/mult_d2/first_thread_fails.tx @@ -1,6 +1,9 @@ +trace { // ARGS: --verilog multipliers/mult_d2/mult_d2.v --protocol multipliers/mult_d2/mult_d2.prot // RETURN: 101 mul(1, 2, 3); mul(6, 8, 48); + +} diff --git a/protocols/tests/multipliers/mult_d2/second_thread_fails.out b/protocols/tests/multipliers/mult_d2/second_thread_fails.out index 25010251..24675e70 100644 --- a/protocols/tests/multipliers/mult_d2/second_thread_fails.out +++ b/protocols/tests/multipliers/mult_d2/second_thread_fails.out @@ -4,3 +4,5 @@ error: The two expressions did not evaluate to the same value 22 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 47, RHS Value: 48 +Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr7, expr2_id: expr8, value1: ValueOwned(00000000000000000000000000101111), value2: ValueOwned(00000000000000000000000000110000) }) +Trace 0 execution failed. diff --git a/protocols/tests/multipliers/mult_d2/second_thread_fails.tx b/protocols/tests/multipliers/mult_d2/second_thread_fails.tx index b9d1adee..90294af2 100644 --- a/protocols/tests/multipliers/mult_d2/second_thread_fails.tx +++ b/protocols/tests/multipliers/mult_d2/second_thread_fails.tx @@ -1,6 +1,9 @@ +trace { // ARGS: --verilog multipliers/mult_d2/mult_d2.v --protocol multipliers/mult_d2/mult_d2.prot // RETURN: 101 mul(1, 2, 2); mul(6, 8, 47); + +} diff --git a/protocols/tests/picorv32/unsigned_mul_no_reset.out b/protocols/tests/picorv32/unsigned_mul_no_reset.out index c842c3d8..d2b8cd34 100644 --- a/protocols/tests/picorv32/unsigned_mul_no_reset.out +++ b/protocols/tests/picorv32/unsigned_mul_no_reset.out @@ -1,3 +1,5 @@ Error error: Reached the maximum number of steps: 200 +Trace 0 failed: MaxStepsReached(200) +Trace 0 execution failed. diff --git a/protocols/tests/picorv32/unsigned_mul_no_reset.tx b/protocols/tests/picorv32/unsigned_mul_no_reset.tx index a03b9863..2bf630c6 100644 --- a/protocols/tests/picorv32/unsigned_mul_no_reset.tx +++ b/protocols/tests/picorv32/unsigned_mul_no_reset.tx @@ -1,7 +1,9 @@ +trace { // ARGS: --verilog ../../examples/picorv32/picorv32.v --protocol picorv32/pcpi_mul_no_reset.prot --module picorv32_pcpi_mul --max-steps 200 // RETURN: 101 pcpi_mul_reset_normal(); pcpi_mul(1, 1, 1); pcpi_mul(1, 100, 100); pcpi_mul(100, 1, 100); -pcpi_mul(33554483, 200, 2415929304); \ No newline at end of file +pcpi_mul(33554483, 200, 2415929304); +} diff --git a/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.out b/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.out index c842c3d8..d2b8cd34 100644 --- a/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.out +++ b/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.out @@ -1,3 +1,5 @@ Error error: Reached the maximum number of steps: 200 +Trace 0 failed: MaxStepsReached(200) +Trace 0 execution failed. diff --git a/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.tx b/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.tx index 58e1aacd..d782f82e 100644 --- a/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.tx +++ b/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.tx @@ -1,7 +1,9 @@ +trace { // ARGS: --verilog ../../examples/picorv32/picorv32.v --protocol picorv32/pcpi_mul_no_reset.prot --module picorv32_pcpi_mul --max-steps 200 // RETURN: 101 pcpi_mul_reset_one(); pcpi_mul(1, 1, 1); pcpi_mul(1, 100, 100); pcpi_mul(100, 1, 100); -pcpi_mul(33554483, 200, 2415929304); \ No newline at end of file +pcpi_mul(33554483, 200, 2415929304); +} From 78cd42622afcc2c0ff1ff10b494c8e58bea42a71 Mon Sep 17 00:00:00 2001 From: Nikil-Shyamsunder Date: Sat, 14 Feb 2026 21:23:18 -0800 Subject: [PATCH 2/3] make outputs prettier, traces pretter, and add a multitrace test case --- examples/picorv32/unsigned_mul.tx | 13 +++++------ examples/serv/serv_regfile.tx | 23 +++++++++---------- examples/tinyaes128/aes128.tx | 9 ++++---- interp/src/main.rs | 14 ++++------- .../adders/adder_d0/add_combinational.tx | 5 ++-- .../adders/adder_d0/illegal_assignment.out | 1 - .../adders/adder_d0/illegal_assignment.tx | 5 ++-- .../illegal_observation_assertion.out | 1 - .../adder_d0/illegal_observation_assertion.tx | 5 ++-- .../illegal_observation_conditional.out | 1 - .../illegal_observation_conditional.tx | 5 ++-- .../tests/adders/adder_d1/add_incorrect.out | 2 -- .../tests/adders/adder_d1/add_incorrect.tx | 7 +++--- .../adder_d1/add_incorrect_implicit.out | 2 -- .../adders/adder_d1/add_incorrect_implicit.tx | 7 +++--- .../tests/adders/adder_d1/add_multitrace.out | 11 +++++++++ .../tests/adders/adder_d1/add_multitrace.tx | 11 +++++++++ .../adders/adder_d1/both_threads_fail.out | 2 -- .../adders/adder_d1/both_threads_fail.tx | 7 +++--- .../adders/adder_d1/both_threads_pass.tx | 6 ++--- .../tests/adders/adder_d1/busy_wait_fail.out | 1 - .../tests/adders/adder_d1/busy_wait_fail.tx | 5 ++-- .../tests/adders/adder_d1/busy_wait_pass.tx | 7 +++--- .../adders/adder_d1/didnt_end_in_step.out | 1 - .../adders/adder_d1/didnt_end_in_step.tx | 6 ++--- .../adders/adder_d1/double_fork_error.out | 2 -- .../adders/adder_d1/double_fork_error.tx | 7 +++--- .../adder_d1/first_fail_second_norun.out | 1 - .../adder_d1/first_fail_second_norun.tx | 7 +++--- .../adders/adder_d1/first_thread_fails.out | 1 - .../adders/adder_d1/first_thread_fails.tx | 6 ++--- .../adder_d1/fork_before_step_error.out | 1 - .../adders/adder_d1/fork_before_step_error.tx | 7 +++--- .../adders/adder_d1/loop_with_assigns.tx | 7 +++--- .../tests/adders/adder_d1/nested_busy_wait.tx | 7 +++--- .../adders/adder_d1/second_thread_fails.out | 1 - .../adders/adder_d1/second_thread_fails.tx | 6 ++--- .../adders/adder_d1/wait_and_add_correct.tx | 7 +++--- .../wait_and_add_incorrect_implicit.out | 2 -- .../wait_and_add_incorrect_implicit.tx | 7 +++--- .../adders/adder_d2/both_threads_pass.tx | 7 +++--- .../adders/adder_d2/no_dontcare_conflict.out | 2 -- .../adders/adder_d2/no_dontcare_conflict.tx | 7 +++--- protocols/tests/alus/alu_d1.tx | 13 +++++------ protocols/tests/alus/alu_d2.tx | 13 +++++------ .../bit_truncation/bit_truncation_fft_bug.out | 1 - .../bit_truncation/bit_truncation_fft_bug.tx | 4 ++-- .../bit_truncation/bit_truncation_fft_fix.tx | 4 ++-- .../bit_truncation/bit_truncation_sha_bug.out | 1 - .../bit_truncation/bit_truncation_sha_bug.tx | 4 ++-- .../bit_truncation/bit_truncation_sha_fix.tx | 4 ++-- .../failure_to_update/ftu_sha_bug.out | 1 - .../failure_to_update/ftu_sha_bug.tx | 4 ++-- .../failure_to_update/ftu_sha_fix.tx | 4 ++-- .../signal_asynchrony/signal_async_bug.out | 1 - .../signal_asynchrony/signal_async_bug.tx | 4 ++-- .../signal_asynchrony/signal_async_fix.tx | 4 ++-- .../use_without_valid_bug.out | 1 - .../use_without_valid_bug.tx | 4 ++-- .../use_without_valid_fix.tx | 4 ++-- protocols/tests/counters/counter.tx | 5 ++-- protocols/tests/fifo/fifo.tx | 15 ++++++------ protocols/tests/fifo/pop_before_push_fail.out | 1 - protocols/tests/fifo/pop_before_push_fail.tx | 14 +++++------ protocols/tests/fifo/pop_empty_fail.out | 1 - protocols/tests/fifo/pop_empty_fail.tx | 8 +++---- protocols/tests/fifo/push_pop_conflict.out | 1 - protocols/tests/fifo/push_pop_conflict.tx | 9 ++++---- protocols/tests/fifo/push_pop_identity_ok.tx | 14 +++++------ protocols/tests/fifo/push_pop_loop_empty.tx | 11 ++++----- .../tests/fifo/push_pop_loop_not_empty.tx | 11 ++++----- .../dual_identity_d0_combdep.out | 1 - .../dual_identity_d0_combdep.tx | 15 ++++++------ .../dual_identity_d1/dual_identity_d1.tx | 7 +++--- .../identity_d0/passthrough_combdep.tx | 5 ++-- .../identities/identity_d1/explicit_fork.out | 1 - .../identities/identity_d1/explicit_fork.tx | 11 ++++----- .../identities/identity_d1/slicing_err.tx | 4 ++-- .../identities/identity_d1/slicing_invalid.tx | 4 ++-- .../identities/identity_d1/slicing_ok.tx | 4 ++-- .../identity_d2/single_thread_passes.tx | 5 ++-- .../identity_d2/two_assignments_same_value.tx | 7 +++--- .../two_different_assignments_error.out | 2 -- .../two_different_assignments_error.tx | 7 +++--- .../identities/identity_d2/two_fork_err.out | 1 - .../identities/identity_d2/two_fork_err.tx | 5 ++-- .../identity_d2/two_fork_ill_formed.tx | 5 ++-- protocols/tests/inverters/inverter_d0.out | 1 - protocols/tests/inverters/inverter_d0.tx | 5 ++-- protocols/tests/multi/multi0/multi0.tx | 5 ++-- .../tests/multi/multi0keep/multi0keep.tx | 5 ++-- .../multi0keep2const/multi0keep2const.tx | 5 ++-- .../tests/multi/multi2const/multi2const.tx | 5 ++-- .../tests/multi/multi2multi/multi2multi.tx | 5 ++-- .../tests/multi/multi_data/multi_data.tx | 5 ++-- .../multipliers/mult_d2/both_threads_fail.out | 2 -- .../multipliers/mult_d2/both_threads_fail.tx | 9 +++----- .../multipliers/mult_d2/both_threads_pass.tx | 7 +++--- .../mult_d2/first_thread_fails.out | 1 - .../multipliers/mult_d2/first_thread_fails.tx | 9 +++----- .../mult_d2/second_thread_fails.out | 1 - .../mult_d2/second_thread_fails.tx | 9 +++----- .../tests/picorv32/unsigned_mul_no_reset.out | 1 - .../tests/picorv32/unsigned_mul_no_reset.tx | 12 +++++----- ...no_reset_thread_assignment_persistence.out | 1 - ..._no_reset_thread_assignment_persistence.tx | 12 +++++----- 106 files changed, 254 insertions(+), 333 deletions(-) create mode 100644 protocols/tests/adders/adder_d1/add_multitrace.out create mode 100644 protocols/tests/adders/adder_d1/add_multitrace.tx diff --git a/examples/picorv32/unsigned_mul.tx b/examples/picorv32/unsigned_mul.tx index c49259b8..561ed954 100644 --- a/examples/picorv32/unsigned_mul.tx +++ b/examples/picorv32/unsigned_mul.tx @@ -1,9 +1,8 @@ -trace { // 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); } diff --git a/examples/serv/serv_regfile.tx b/examples/serv/serv_regfile.tx index b45d1ad0..cf85cc11 100644 --- a/examples/serv/serv_regfile.tx +++ b/examples/serv/serv_regfile.tx @@ -1,14 +1,13 @@ -trace { // 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); } diff --git a/examples/tinyaes128/aes128.tx b/examples/tinyaes128/aes128.tx index a8acbb5a..ebfeb5b0 100644 --- a/examples/tinyaes128/aes128.tx +++ b/examples/tinyaes128/aes128.tx @@ -1,7 +1,6 @@ -trace { // 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); } diff --git a/interp/src/main.rs b/interp/src/main.rs index 2788cb88..7bfa304a 100644 --- a/interp/src/main.rs +++ b/interp/src/main.rs @@ -141,6 +141,10 @@ fn main() -> anyhow::Result<()> { 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); @@ -159,15 +163,7 @@ fn main() -> anyhow::Result<()> { cli.max_steps.unwrap_or(u32::MAX), ); let results = scheduler.execute_todos(); - - // Report each trace result to stdout so it is captured in .out files. - let mut trace_failed = false; - for res in results { - if let Err(err) = res { - trace_failed = true; - println!("Trace {} failed: {:?}", trace_index, err); - } - } + let trace_failed = results.iter().any(|res| res.is_err()); if trace_failed { any_failed = true; diff --git a/protocols/tests/adders/adder_d0/add_combinational.tx b/protocols/tests/adders/adder_d0/add_combinational.tx index 8f75b04d..d7dcc15a 100644 --- a/protocols/tests/adders/adder_d0/add_combinational.tx +++ b/protocols/tests/adders/adder_d0/add_combinational.tx @@ -1,5 +1,4 @@ -trace { // 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); } diff --git a/protocols/tests/adders/adder_d0/illegal_assignment.out b/protocols/tests/adders/adder_d0/illegal_assignment.out index e18da9f7..02ca04ca 100644 --- a/protocols/tests/adders/adder_d0/illegal_assignment.out +++ b/protocols/tests/adders/adder_d0/illegal_assignment.out @@ -4,5 +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 failed: Evaluation(ForbiddenPortRead { port_name: "DUT.s", unassigned_inputs: [("DUT.b", None), ("DUT.a", None)], expr_id: expr1 }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d0/illegal_assignment.tx b/protocols/tests/adders/adder_d0/illegal_assignment.tx index c7387898..281169ad 100644 --- a/protocols/tests/adders/adder_d0/illegal_assignment.tx +++ b/protocols/tests/adders/adder_d0/illegal_assignment.tx @@ -1,6 +1,5 @@ -trace { // 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); } diff --git a/protocols/tests/adders/adder_d0/illegal_observation_assertion.out b/protocols/tests/adders/adder_d0/illegal_observation_assertion.out index 6e6f441d..b6878884 100644 --- a/protocols/tests/adders/adder_d0/illegal_observation_assertion.out +++ b/protocols/tests/adders/adder_d0/illegal_observation_assertion.out @@ -7,5 +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 failed: Evaluation(ForbiddenPortRead { port_name: "DUT.s", unassigned_inputs: [("DUT.b", Some(stmt2))], expr_id: expr4 }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d0/illegal_observation_assertion.tx b/protocols/tests/adders/adder_d0/illegal_observation_assertion.tx index 87b5063c..d42f3269 100644 --- a/protocols/tests/adders/adder_d0/illegal_observation_assertion.tx +++ b/protocols/tests/adders/adder_d0/illegal_observation_assertion.tx @@ -1,6 +1,5 @@ -trace { // 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); } diff --git a/protocols/tests/adders/adder_d0/illegal_observation_conditional.out b/protocols/tests/adders/adder_d0/illegal_observation_conditional.out index 5c3cb6d8..91c0704e 100644 --- a/protocols/tests/adders/adder_d0/illegal_observation_conditional.out +++ b/protocols/tests/adders/adder_d0/illegal_observation_conditional.out @@ -7,5 +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 failed: Evaluation(ForbiddenPortRead { port_name: "DUT.s", unassigned_inputs: [("DUT.b", Some(stmt2))], expr_id: expr4 }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d0/illegal_observation_conditional.tx b/protocols/tests/adders/adder_d0/illegal_observation_conditional.tx index e87ba3f8..4c287cda 100644 --- a/protocols/tests/adders/adder_d0/illegal_observation_conditional.tx +++ b/protocols/tests/adders/adder_d0/illegal_observation_conditional.tx @@ -1,6 +1,5 @@ -trace { // 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); } diff --git a/protocols/tests/adders/adder_d1/add_incorrect.out b/protocols/tests/adders/adder_d1/add_incorrect.out index 311a3d35..83d34e59 100644 --- a/protocols/tests/adders/adder_d1/add_incorrect.out +++ b/protocols/tests/adders/adder_d1/add_incorrect.out @@ -10,6 +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 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000100), new_value: ValueOwned(00000000000000000000000000000001), thread_idx: 0, transaction_name: "add_incorrect", stmt_id: stmt4 }) -Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000001), new_value: ValueOwned(00000000000000000000000000000100), thread_idx: 1, transaction_name: "add_incorrect", stmt_id: stmt1 }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/add_incorrect.tx b/protocols/tests/adders/adder_d1/add_incorrect.tx index dfc6856a..fee34936 100644 --- a/protocols/tests/adders/adder_d1/add_incorrect.tx +++ b/protocols/tests/adders/adder_d1/add_incorrect.tx @@ -1,7 +1,6 @@ -trace { // 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); } diff --git a/protocols/tests/adders/adder_d1/add_incorrect_implicit.out b/protocols/tests/adders/adder_d1/add_incorrect_implicit.out index 05494e9a..cb716a66 100644 --- a/protocols/tests/adders/adder_d1/add_incorrect_implicit.out +++ b/protocols/tests/adders/adder_d1/add_incorrect_implicit.out @@ -10,6 +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 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000100), new_value: ValueOwned(00000000000000000000000000000001), thread_idx: 0, transaction_name: "add_incorrect_implicit", stmt_id: stmt1 }) -Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000001), new_value: ValueOwned(00000000000000000000000000000100), thread_idx: 1, transaction_name: "add_incorrect_implicit", stmt_id: stmt1 }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/add_incorrect_implicit.tx b/protocols/tests/adders/adder_d1/add_incorrect_implicit.tx index dddd7483..84b4bf5e 100644 --- a/protocols/tests/adders/adder_d1/add_incorrect_implicit.tx +++ b/protocols/tests/adders/adder_d1/add_incorrect_implicit.tx @@ -1,7 +1,6 @@ -trace { // 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); } diff --git a/protocols/tests/adders/adder_d1/add_multitrace.out b/protocols/tests/adders/adder_d1/add_multitrace.out new file mode 100644 index 00000000..efdfbba0 --- /dev/null +++ b/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. diff --git a/protocols/tests/adders/adder_d1/add_multitrace.tx b/protocols/tests/adders/adder_d1/add_multitrace.tx new file mode 100644 index 00000000..07854d8d --- /dev/null +++ b/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); +} diff --git a/protocols/tests/adders/adder_d1/both_threads_fail.out b/protocols/tests/adders/adder_d1/both_threads_fail.out index ced952de..767e7dd9 100644 --- a/protocols/tests/adders/adder_d1/both_threads_fail.out +++ b/protocols/tests/adders/adder_d1/both_threads_fail.out @@ -10,6 +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 failed: Assertion(EqualityFailed { expr1_id: expr5, expr2_id: expr6, value1: ValueOwned(00000000000000000000000000000101), value2: ValueOwned(00000000000000000000000000000011) }) -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr5, expr2_id: expr6, value1: ValueOwned(00000000000000000000000000001010), value2: ValueOwned(00000000000000000000000000001001) }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/both_threads_fail.tx b/protocols/tests/adders/adder_d1/both_threads_fail.tx index 552e6324..0e86e8be 100644 --- a/protocols/tests/adders/adder_d1/both_threads_fail.tx +++ b/protocols/tests/adders/adder_d1/both_threads_fail.tx @@ -1,7 +1,6 @@ -trace { // 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); } diff --git a/protocols/tests/adders/adder_d1/both_threads_pass.tx b/protocols/tests/adders/adder_d1/both_threads_pass.tx index 8ffe5992..640a6616 100644 --- a/protocols/tests/adders/adder_d1/both_threads_pass.tx +++ b/protocols/tests/adders/adder_d1/both_threads_pass.tx @@ -1,5 +1,5 @@ -trace { // 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); } diff --git a/protocols/tests/adders/adder_d1/busy_wait_fail.out b/protocols/tests/adders/adder_d1/busy_wait_fail.out index fbf92b57..a543c5e8 100644 --- a/protocols/tests/adders/adder_d1/busy_wait_fail.out +++ b/protocols/tests/adders/adder_d1/busy_wait_fail.out @@ -4,5 +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 failed: Assertion(EqualityFailed { expr1_id: expr4, expr2_id: expr5, value1: ValueOwned(00000000000000000000001111100111), value2: ValueOwned(00000000000000000000000000000011) }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/busy_wait_fail.tx b/protocols/tests/adders/adder_d1/busy_wait_fail.tx index e45dfe14..3024a150 100644 --- a/protocols/tests/adders/adder_d1/busy_wait_fail.tx +++ b/protocols/tests/adders/adder_d1/busy_wait_fail.tx @@ -1,6 +1,5 @@ -trace { // 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 } diff --git a/protocols/tests/adders/adder_d1/busy_wait_pass.tx b/protocols/tests/adders/adder_d1/busy_wait_pass.tx index 90b5ebea..df87db84 100644 --- a/protocols/tests/adders/adder_d1/busy_wait_pass.tx +++ b/protocols/tests/adders/adder_d1/busy_wait_pass.tx @@ -1,6 +1,5 @@ -trace { // 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 } diff --git a/protocols/tests/adders/adder_d1/didnt_end_in_step.out b/protocols/tests/adders/adder_d1/didnt_end_in_step.out index 7eb2505a..bddc2b05 100644 --- a/protocols/tests/adders/adder_d1/didnt_end_in_step.out +++ b/protocols/tests/adders/adder_d1/didnt_end_in_step.out @@ -4,5 +4,4 @@ error: The last executed statement in Thread 0 (transaction 'add_doesnt_end_in_s 39 │ fork(); │ ^^^^^^^ last statement wasn't `step()` -Trace 0 failed: Thread(DidntEndWithStep { thread_idx: 0, transaction_name: "add_doesnt_end_in_step", last_executed_stmt_id: stmt7 }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/didnt_end_in_step.tx b/protocols/tests/adders/adder_d1/didnt_end_in_step.tx index 671823a3..b20af6a3 100644 --- a/protocols/tests/adders/adder_d1/didnt_end_in_step.tx +++ b/protocols/tests/adders/adder_d1/didnt_end_in_step.tx @@ -1,7 +1,5 @@ -trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 -add_doesnt_end_in_step(1, 2, 3); - - +trace { + add_doesnt_end_in_step(1, 2, 3); } diff --git a/protocols/tests/adders/adder_d1/double_fork_error.out b/protocols/tests/adders/adder_d1/double_fork_error.out index c92cbd4e..67b41ecf 100644 --- a/protocols/tests/adders/adder_d1/double_fork_error.out +++ b/protocols/tests/adders/adder_d1/double_fork_error.out @@ -16,6 +16,4 @@ error: Thread 1 (transaction 'add_double_fork') attempted to fork more than once 15 │ fork(); │ ^^^^^^^ second fork() called here -Trace 0 failed: Thread(DoubleFork { thread_idx: 0, transaction_name: "add_double_fork", first_fork_stmt_id: stmt4, second_fork_stmt_id: stmt7 }) -Trace 0 failed: Thread(DoubleFork { thread_idx: 1, transaction_name: "add_double_fork", first_fork_stmt_id: stmt4, second_fork_stmt_id: stmt7 }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/double_fork_error.tx b/protocols/tests/adders/adder_d1/double_fork_error.tx index b8883aba..aa036892 100644 --- a/protocols/tests/adders/adder_d1/double_fork_error.tx +++ b/protocols/tests/adders/adder_d1/double_fork_error.tx @@ -1,7 +1,6 @@ -trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/double_fork_error.prot // RETURN: 101 -add_double_fork(1, 2, 3); -add_double_fork(4, 5, 9); - +trace { + add_double_fork(1, 2, 3); + add_double_fork(4, 5, 9); } diff --git a/protocols/tests/adders/adder_d1/first_fail_second_norun.out b/protocols/tests/adders/adder_d1/first_fail_second_norun.out index 81103238..9b436ef4 100644 --- a/protocols/tests/adders/adder_d1/first_fail_second_norun.out +++ b/protocols/tests/adders/adder_d1/first_fail_second_norun.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 14 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 4, RHS Value: 3 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr5, expr2_id: expr6, value1: ValueOwned(00000000000000000000000000000100), value2: ValueOwned(00000000000000000000000000000011) }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/first_fail_second_norun.tx b/protocols/tests/adders/adder_d1/first_fail_second_norun.tx index 229a75b6..9adbfe09 100644 --- a/protocols/tests/adders/adder_d1/first_fail_second_norun.tx +++ b/protocols/tests/adders/adder_d1/first_fail_second_norun.tx @@ -1,7 +1,6 @@ -trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 -add(1, 2, 4); -add(4, 5, 10); - +trace { + add(1, 2, 4); + add(4, 5, 10); } diff --git a/protocols/tests/adders/adder_d1/first_thread_fails.out b/protocols/tests/adders/adder_d1/first_thread_fails.out index 81103238..9b436ef4 100644 --- a/protocols/tests/adders/adder_d1/first_thread_fails.out +++ b/protocols/tests/adders/adder_d1/first_thread_fails.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 14 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 4, RHS Value: 3 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr5, expr2_id: expr6, value1: ValueOwned(00000000000000000000000000000100), value2: ValueOwned(00000000000000000000000000000011) }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/first_thread_fails.tx b/protocols/tests/adders/adder_d1/first_thread_fails.tx index d3a2cd8f..bae9521d 100644 --- a/protocols/tests/adders/adder_d1/first_thread_fails.tx +++ b/protocols/tests/adders/adder_d1/first_thread_fails.tx @@ -1,6 +1,6 @@ -trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 -add(1, 2, 4); -add(4, 5, 9); +trace { + add(1, 2, 4); + add(4, 5, 9); } diff --git a/protocols/tests/adders/adder_d1/fork_before_step_error.out b/protocols/tests/adders/adder_d1/fork_before_step_error.out index 068911af..b68ab374 100644 --- a/protocols/tests/adders/adder_d1/fork_before_step_error.out +++ b/protocols/tests/adders/adder_d1/fork_before_step_error.out @@ -4,5 +4,4 @@ error: Thread 0 (transaction 'add_fork_before_step') called `fork()` before call 11 │ fork(); │ ^^^^^^^ Thread 0 (transaction 'add_fork_before_step') called `fork()` before calling `step()` -Trace 0 failed: Thread(ForkBeforeStep { thread_idx: 0, transaction_name: "add_fork_before_step", stmt_id: stmt3 }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/fork_before_step_error.tx b/protocols/tests/adders/adder_d1/fork_before_step_error.tx index 3ba3de97..5bffd4ac 100644 --- a/protocols/tests/adders/adder_d1/fork_before_step_error.tx +++ b/protocols/tests/adders/adder_d1/fork_before_step_error.tx @@ -1,7 +1,6 @@ -trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/fork_before_step_error.prot // RETURN: 101 -add_fork_before_step(1, 2, 3); -add_fork_before_step(4, 5, 9); - +trace { + add_fork_before_step(1, 2, 3); + add_fork_before_step(4, 5, 9); } diff --git a/protocols/tests/adders/adder_d1/loop_with_assigns.tx b/protocols/tests/adders/adder_d1/loop_with_assigns.tx index a811100f..14ec302a 100644 --- a/protocols/tests/adders/adder_d1/loop_with_assigns.tx +++ b/protocols/tests/adders/adder_d1/loop_with_assigns.tx @@ -1,6 +1,5 @@ -trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/loop_with_assigns.prot -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 - +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 } diff --git a/protocols/tests/adders/adder_d1/nested_busy_wait.tx b/protocols/tests/adders/adder_d1/nested_busy_wait.tx index 6cd1b0ed..6315bb9f 100644 --- a/protocols/tests/adders/adder_d1/nested_busy_wait.tx +++ b/protocols/tests/adders/adder_d1/nested_busy_wait.tx @@ -1,6 +1,5 @@ -trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/nested_busy_wait.prot -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 - +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 } diff --git a/protocols/tests/adders/adder_d1/second_thread_fails.out b/protocols/tests/adders/adder_d1/second_thread_fails.out index 627708fc..54efdc9c 100644 --- a/protocols/tests/adders/adder_d1/second_thread_fails.out +++ b/protocols/tests/adders/adder_d1/second_thread_fails.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 14 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 10, RHS Value: 9 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr5, expr2_id: expr6, value1: ValueOwned(00000000000000000000000000001010), value2: ValueOwned(00000000000000000000000000001001) }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/second_thread_fails.tx b/protocols/tests/adders/adder_d1/second_thread_fails.tx index f648fd2a..5409d117 100644 --- a/protocols/tests/adders/adder_d1/second_thread_fails.tx +++ b/protocols/tests/adders/adder_d1/second_thread_fails.tx @@ -1,6 +1,6 @@ -trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 -add(1, 2, 3); -add(4, 5, 10); +trace { + add(1, 2, 3); + add(4, 5, 10); } diff --git a/protocols/tests/adders/adder_d1/wait_and_add_correct.tx b/protocols/tests/adders/adder_d1/wait_and_add_correct.tx index 773a4b58..4f0c3f0b 100644 --- a/protocols/tests/adders/adder_d1/wait_and_add_correct.tx +++ b/protocols/tests/adders/adder_d1/wait_and_add_correct.tx @@ -1,7 +1,6 @@ -trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 0 -wait_and_add(1, 2, 3); -add(4, 5, 9); - +trace { + wait_and_add(1, 2, 3); + add(4, 5, 9); } diff --git a/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.out b/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.out index df6b2059..c03cd41a 100644 --- a/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.out +++ b/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.out @@ -10,6 +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 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000100), new_value: ValueOwned(00000000000000000000000000000001), thread_idx: 0, transaction_name: "wait_and_add", stmt_id: stmt4 }) -Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000001), new_value: ValueOwned(00000000000000000000000000000100), thread_idx: 1, transaction_name: "add_incorrect_implicit", stmt_id: stmt1 }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.tx b/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.tx index 4530d130..d4a44133 100644 --- a/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.tx +++ b/protocols/tests/adders/adder_d1/wait_and_add_incorrect_implicit.tx @@ -1,7 +1,6 @@ -trace { // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 -wait_and_add(1, 2, 3); -add_incorrect_implicit(4, 5, 9); - +trace { + wait_and_add(1, 2, 3); + add_incorrect_implicit(4, 5, 9); } diff --git a/protocols/tests/adders/adder_d2/both_threads_pass.tx b/protocols/tests/adders/adder_d2/both_threads_pass.tx index 3013a8eb..91a2a3d1 100644 --- a/protocols/tests/adders/adder_d2/both_threads_pass.tx +++ b/protocols/tests/adders/adder_d2/both_threads_pass.tx @@ -1,7 +1,6 @@ -trace { // ARGS: --verilog adders/adder_d2/add_d2.v --protocol adders/adder_d2/add_d2.prot --max-steps 4 // RETURN: 0 -add(1, 2, 3); -add(4, 5, 9); - +trace { + add(1, 2, 3); + add(4, 5, 9); } diff --git a/protocols/tests/adders/adder_d2/no_dontcare_conflict.out b/protocols/tests/adders/adder_d2/no_dontcare_conflict.out index e43c2cc0..ef370646 100644 --- a/protocols/tests/adders/adder_d2/no_dontcare_conflict.out +++ b/protocols/tests/adders/adder_d2/no_dontcare_conflict.out @@ -10,6 +10,4 @@ error: Thread 1 (`add`) attempted conflicting assignment to 'a': current=1, new= 12 │ DUT.a := a; │ ^^^^^^^^^^^ Thread 1 (`add`) attempted conflicting assignment to 'a': current=1, new=4 -Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000100), new_value: ValueOwned(00000000000000000000000000000001), thread_idx: 0, transaction_name: "add", stmt_id: stmt1 }) -Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000001), new_value: ValueOwned(00000000000000000000000000000100), thread_idx: 1, transaction_name: "add", stmt_id: stmt1 }) Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d2/no_dontcare_conflict.tx b/protocols/tests/adders/adder_d2/no_dontcare_conflict.tx index 0939aca2..0c5c16c5 100644 --- a/protocols/tests/adders/adder_d2/no_dontcare_conflict.tx +++ b/protocols/tests/adders/adder_d2/no_dontcare_conflict.tx @@ -1,7 +1,6 @@ -trace { // ARGS: --verilog adders/adder_d2/add_d2.v --protocol adders/adder_d2/no_dontcare_conflict.prot // RETURN: 101 -add(1, 2, 3); -add(4, 5, 9); - +trace { + add(1, 2, 3); + add(4, 5, 9); } diff --git a/protocols/tests/alus/alu_d1.tx b/protocols/tests/alus/alu_d1.tx index 6bbfe8a9..20825157 100644 --- a/protocols/tests/alus/alu_d1.tx +++ b/protocols/tests/alus/alu_d1.tx @@ -1,9 +1,8 @@ -trace { // ARGS: --verilog=alus/alu_d1.v --protocol=alus/alu_d1.prot --module alu_d1 -add(1, 2, 3); -add(123, 245, 368); -sub(200, 200, 0); -and(100, 100, 100); -or(0, 230, 230); - +trace { + add(1, 2, 3); + add(123, 245, 368); + sub(200, 200, 0); + and(100, 100, 100); + or(0, 230, 230); } diff --git a/protocols/tests/alus/alu_d2.tx b/protocols/tests/alus/alu_d2.tx index ebc6a596..8bdb53a2 100644 --- a/protocols/tests/alus/alu_d2.tx +++ b/protocols/tests/alus/alu_d2.tx @@ -1,9 +1,8 @@ -trace { // ARGS: --verilog=alus/alu_d2.v --protocol=alus/alu_d2.prot --module alu_d2 -add(1, 2, 3); -add(123, 245, 368); -sub(200, 200, 0); -and(100, 100, 100); -or(0, 230, 230); - +trace { + add(1, 2, 3); + add(123, 245, 368); + sub(200, 200, 0); + and(100, 100, 100); + or(0, 230, 230); } diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.out b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.out index 015c6f2d..1e4bcfe5 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.out +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 10 │ assert_eq(data_out, dut.output_data); │ ^^^^^^^^^^^^^^^^^^^^^^^^^ LHS Value: 2047, RHS Value: 0 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr2, expr2_id: expr3, value1: ValueOwned(11111111111), value2: ValueOwned(00000000000) }) Trace 0 execution failed. diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.tx b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.tx index acf66cde..0d7f172a 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.tx +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.tx @@ -1,5 +1,5 @@ -trace { // ARGS: --verilog=brave_new_world/bit_truncation/bit_truncation_fft_bug.v --protocol=brave_new_world/bit_truncation/bit_truncation_fft.prot --module bit_truncation_fft_bug // RETURN: 101 -bit_truncation_fft(8386560, 2047); +trace { + bit_truncation_fft(8386560, 2047); } diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.tx b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.tx index c2145282..d2d02a2c 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.tx +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_fix.tx @@ -1,4 +1,4 @@ -trace { // ARGS: --verilog=brave_new_world/bit_truncation/bit_truncation_fft_fix.v --protocol=brave_new_world/bit_truncation/bit_truncation_fft.prot --module round11_rne_unsigned_fixed -bit_truncation_fft(8386560, 2047); +trace { + bit_truncation_fft(8386560, 2047); } diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.out b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.out index c06584bc..34967913 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.out +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 9 │ assert_eq(data_out, dut.left); │ ^^^^^^^^^^^^^^^^^^ LHS Value: 68719476736, RHS Value: 0 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr2, expr2_id: expr3, value1: ValueOwned(000001000000000000000000000000000000000000), value2: ValueOwned(000000000000000000000000000000000000000000) }) Trace 0 execution failed. diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.tx b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.tx index ecd45a2c..4507043d 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.tx +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_bug.tx @@ -1,5 +1,5 @@ -trace { // ARGS: --verilog=brave_new_world/bit_truncation/bit_truncation_sha_bug.v --protocol=brave_new_world/bit_truncation/bit_truncation_sha.prot --module bit_truncation_sha_bug // RETURN: 101 -bit_truncation_sha(4398046511104, 68719476736); +trace { + bit_truncation_sha(4398046511104, 68719476736); } diff --git a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.tx b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.tx index bd3a9004..719078ae 100644 --- a/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.tx +++ b/protocols/tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.tx @@ -1,4 +1,4 @@ -trace { // ARGS: --verilog=brave_new_world/bit_truncation/bit_truncation_sha_fix.v --protocol=brave_new_world/bit_truncation/bit_truncation_sha.prot --module bit_truncation_sha_fixed -bit_truncation_sha(4398046511104, 68719476736); +trace { + bit_truncation_sha(4398046511104, 68719476736); } diff --git a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.out b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.out index 7d45fbf6..bfab2905 100644 --- a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.out +++ b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 29 │ assert_eq(dut.valid, 1'b0); │ ^^^^^^^^^^^^^^^ LHS Value: 1, RHS Value: 0 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr9, expr2_id: expr10, value1: ValueOwned(1), value2: ValueOwned(0) }) Trace 0 execution failed. diff --git a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.tx b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.tx index 8c1fd7be..accaf265 100644 --- a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.tx +++ b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_bug.tx @@ -1,5 +1,5 @@ -trace { // ARGS: --verilog=brave_new_world/failure_to_update/ftu_sha_bug.v --protocol=brave_new_world/failure_to_update/ftu_sha.prot --module fsm_update_buggy // RETURN: 101 -failure_to_update_sha(); +trace { + failure_to_update_sha(); } diff --git a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.tx b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.tx index 20c289ad..7604fe20 100644 --- a/protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.tx +++ b/protocols/tests/brave_new_world/failure_to_update/ftu_sha_fix.tx @@ -1,4 +1,4 @@ -trace { // ARGS: --verilog=brave_new_world/failure_to_update/ftu_sha_fix.v --protocol=brave_new_world/failure_to_update/ftu_sha.prot --module fsm_update_fixed_gated -failure_to_update_sha(); +trace { + failure_to_update_sha(); } diff --git a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.out b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.out index ba5a1a89..bb2cd5ee 100644 --- a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.out +++ b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 18 │ assert_eq(data_out, dut.final_resp); │ ^^^^^^^^^^^^^^^^^^^^^^^^ LHS Value: 7, RHS Value: 0 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr6, expr2_id: expr7, value1: ValueOwned(00000000000000000000000000000111), value2: ValueOwned(00000000000000000000000000000000) }) Trace 0 execution failed. diff --git a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.tx b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.tx index 2a792bc0..3340be96 100644 --- a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.tx +++ b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_bug.tx @@ -1,5 +1,5 @@ -trace { // ARGS: --verilog=brave_new_world/signal_asynchrony/signal_async_bug.v --protocol=brave_new_world/signal_asynchrony/signal_async.prot --module signal_async_bug // RETURN: 101 -signal_async(6, 7); +trace { + signal_async(6, 7); } diff --git a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.tx b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.tx index c4fd3abb..0b77dc3d 100644 --- a/protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.tx +++ b/protocols/tests/brave_new_world/signal_asynchrony/signal_async_fix.tx @@ -1,4 +1,4 @@ -trace { // ARGS: --verilog=brave_new_world/signal_asynchrony/signal_async_fix.v --protocol=brave_new_world/signal_asynchrony/signal_async.prot --module signal_async_fix -signal_async(6, 7); +trace { + signal_async(6, 7); } diff --git a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.out b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.out index 6ea5a165..c4167b0c 100644 --- a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.out +++ b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 16 │ assert_eq(data_out, dut.sum); │ ^^^^^^^^^^^^^^^^^ LHS Value: 5, RHS Value: 15 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr4, expr2_id: expr5, value1: ValueOwned(00000000000000000000000000000101), value2: ValueOwned(00000000000000000000000000001111) }) Trace 0 execution failed. diff --git a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.tx b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.tx index d2989a2b..a75a4a80 100644 --- a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.tx +++ b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_bug.tx @@ -1,5 +1,5 @@ -trace { // ARGS: --verilog=brave_new_world/use_without_valid/use_without_valid_bug.v --protocol=brave_new_world/use_without_valid/use_without_valid.prot --module use_without_valid_bug // RETURN: 101 -use_without_valid(5, 5); +trace { + use_without_valid(5, 5); } diff --git a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.tx b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.tx index b674dbf2..dc176950 100644 --- a/protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.tx +++ b/protocols/tests/brave_new_world/use_without_valid/use_without_valid_fix.tx @@ -1,4 +1,4 @@ -trace { // ARGS: --verilog=brave_new_world/use_without_valid/use_without_valid_fix.v --protocol=brave_new_world/use_without_valid/use_without_valid.prot --module use_without_valid_fix -use_without_valid(5, 5); +trace { + use_without_valid(5, 5); } diff --git a/protocols/tests/counters/counter.tx b/protocols/tests/counters/counter.tx index 1fc4a509..68cd16c4 100644 --- a/protocols/tests/counters/counter.tx +++ b/protocols/tests/counters/counter.tx @@ -1,5 +1,4 @@ -trace { // ARGS: --verilog counters/counter.v --protocol counters/counter.prot -count_up(10); - +trace { + count_up(10); } diff --git a/protocols/tests/fifo/fifo.tx b/protocols/tests/fifo/fifo.tx index eabe10ae..aca45d80 100644 --- a/protocols/tests/fifo/fifo.tx +++ b/protocols/tests/fifo/fifo.tx @@ -1,10 +1,9 @@ -trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo.prot --module fifo_wrapper -reset(); -push(3); -push(4); -idle(); -pop(3); -pop(4); - +trace { + reset(); + push(3); + push(4); + idle(); + pop(3); + pop(4); } diff --git a/protocols/tests/fifo/pop_before_push_fail.out b/protocols/tests/fifo/pop_before_push_fail.out index bc91e459..162b5fa2 100644 --- a/protocols/tests/fifo/pop_before_push_fail.out +++ b/protocols/tests/fifo/pop_before_push_fail.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 43 │ assert_eq(DUT.data_o, output); │ ^^^^^^^^^^^^^^^^^^ LHS Value: 0, RHS Value: 3 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr8, expr2_id: expr9, value1: ValueOwned(00000000000000000000000000000000), value2: ValueOwned(00000000000000000000000000000011) }) Trace 0 execution failed. diff --git a/protocols/tests/fifo/pop_before_push_fail.tx b/protocols/tests/fifo/pop_before_push_fail.tx index c6a9fcc0..f873fd42 100644 --- a/protocols/tests/fifo/pop_before_push_fail.tx +++ b/protocols/tests/fifo/pop_before_push_fail.tx @@ -1,11 +1,11 @@ -trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo.prot --module fifo_wrapper // RETURN: 101 +trace { -reset(); -push(4); -pop(4); -idle(); -pop(3); // this line should fail since we're trying to `pop` a non-existent value -push(3); + reset(); + push(4); + pop(4); + idle(); + pop(3); // this line should fail since we're trying to `pop` a non-existent value + push(3); } diff --git a/protocols/tests/fifo/pop_empty_fail.out b/protocols/tests/fifo/pop_empty_fail.out index bc91e459..162b5fa2 100644 --- a/protocols/tests/fifo/pop_empty_fail.out +++ b/protocols/tests/fifo/pop_empty_fail.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 43 │ assert_eq(DUT.data_o, output); │ ^^^^^^^^^^^^^^^^^^ LHS Value: 0, RHS Value: 3 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr8, expr2_id: expr9, value1: ValueOwned(00000000000000000000000000000000), value2: ValueOwned(00000000000000000000000000000011) }) Trace 0 execution failed. diff --git a/protocols/tests/fifo/pop_empty_fail.tx b/protocols/tests/fifo/pop_empty_fail.tx index a2154ec6..72b35041 100644 --- a/protocols/tests/fifo/pop_empty_fail.tx +++ b/protocols/tests/fifo/pop_empty_fail.tx @@ -1,8 +1,8 @@ -trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo.prot --module fifo_wrapper // RETURN: 101 +trace { -reset(); -pop(3); // this line should fail since we're trying to `pop` an empty FIFO -push(3); + reset(); + pop(3); // this line should fail since we're trying to `pop` an empty FIFO + push(3); } diff --git a/protocols/tests/fifo/push_pop_conflict.out b/protocols/tests/fifo/push_pop_conflict.out index 4ef05cb5..c1b37511 100644 --- a/protocols/tests/fifo/push_pop_conflict.out +++ b/protocols/tests/fifo/push_pop_conflict.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 43 │ assert_eq(DUT.data_o, output); │ ^^^^^^^^^^^^^^^^^^ LHS Value: 2, RHS Value: 3 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr8, expr2_id: expr9, value1: ValueOwned(00000000000000000000000000000010), value2: ValueOwned(00000000000000000000000000000011) }) Trace 0 execution failed. diff --git a/protocols/tests/fifo/push_pop_conflict.tx b/protocols/tests/fifo/push_pop_conflict.tx index c790f136..6f817a1b 100644 --- a/protocols/tests/fifo/push_pop_conflict.tx +++ b/protocols/tests/fifo/push_pop_conflict.tx @@ -1,9 +1,8 @@ -trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo.prot --module fifo_wrapper // RETURN: 101 +trace { -reset(); -push(2); -pop(3); // this line should fail, since 3 isn't in the FIFO - + reset(); + push(2); + pop(3); // this line should fail, since 3 isn't in the FIFO } diff --git a/protocols/tests/fifo/push_pop_identity_ok.tx b/protocols/tests/fifo/push_pop_identity_ok.tx index db7e4442..cab2e0bc 100644 --- a/protocols/tests/fifo/push_pop_identity_ok.tx +++ b/protocols/tests/fifo/push_pop_identity_ok.tx @@ -1,10 +1,10 @@ -trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo.prot --module fifo_wrapper +trace { -reset(); -push(2); -pop(2); -idle(); -push(3); -pop(3); + reset(); + push(2); + pop(2); + idle(); + push(3); + pop(3); } diff --git a/protocols/tests/fifo/push_pop_loop_empty.tx b/protocols/tests/fifo/push_pop_loop_empty.tx index a85ae512..e58825b4 100644 --- a/protocols/tests/fifo/push_pop_loop_empty.tx +++ b/protocols/tests/fifo/push_pop_loop_empty.tx @@ -1,8 +1,7 @@ -trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo_bounded_loop.prot --module fifo_wrapper -reset(); -push_n_times(42, 4); // Push 42 four times -pop_n_times(42, 4); // Pop four times -check_empty(); // FIFO should be empty after pushing and popping the same no. of times - +trace { + reset(); + push_n_times(42, 4); // Push 42 four times + pop_n_times(42, 4); // Pop four times + check_empty(); // FIFO should be empty after pushing and popping the same no. of times } diff --git a/protocols/tests/fifo/push_pop_loop_not_empty.tx b/protocols/tests/fifo/push_pop_loop_not_empty.tx index a99b1ea1..91d75f18 100644 --- a/protocols/tests/fifo/push_pop_loop_not_empty.tx +++ b/protocols/tests/fifo/push_pop_loop_not_empty.tx @@ -1,8 +1,7 @@ -trace { // ARGS: --verilog fifo/bsg_mem_1rw_sync.v fifo/bsg_mem_1rw_sync_synth.v fifo/bsg_circular_ptr.v fifo/bsg_fifo_1rw_large.v fifo/fifo_wrapper.v --protocol=fifo/fifo_bounded_loop.prot --module fifo_wrapper -reset(); -push_n_times(7, 3); -pop_n_times(7, 2); -check_not_empty(); // FIFO is non-empty (has one element remaining) - +trace { + reset(); + push_n_times(7, 3); + pop_n_times(7, 2); + check_not_empty(); // FIFO is non-empty (has one element remaining) } diff --git a/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.out b/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.out index 9eb2f39c..73b368a3 100644 --- a/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.out +++ b/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.out @@ -4,5 +4,4 @@ error: Cannot assign to forbidden input 'b' after observing a combinationally de 24 │ dut.b := b; │ ^ Cannot assign to forbidden input 'b' after observing a combinationally dependent output -Trace 0 failed: Evaluation(ForbiddenInputAssignment { input_name: "b", expr_id: expr7 }) Trace 0 execution failed. diff --git a/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.tx b/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.tx index eaf23f90..61a04cf7 100644 --- a/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.tx +++ b/protocols/tests/identities/dual_identity_d0/dual_identity_d0_combdep.tx @@ -1,11 +1,10 @@ -trace { // ARGS: --verilog identities/dual_identity_d0/dual_identity_d0.v --protocol identities/dual_identity_d0/dual_identity_d0.prot // RETURN: 101 -// This test demonstrates how combinational dependency tracking should catch -// observation-assignment conflicts. -// The protocol observes dut.s2 (output) which combinationally depends on dut.b (input). -// Observing s2 should forbid assignments to b, but both branches assign to b. -// With comb dependency tracking: should error with "ASSIGNED FORBIDDEN PORT" -identity(1, 1); - +trace { + // This test demonstrates how combinational dependency tracking should catch + // observation-assignment conflicts. + // The protocol observes dut.s2 (output) which combinationally depends on dut.b (input). + // Observing s2 should forbid assignments to b, but both branches assign to b. + // With comb dependency tracking: should error with "ASSIGNED FORBIDDEN PORT" + identity(1, 1); } diff --git a/protocols/tests/identities/dual_identity_d1/dual_identity_d1.tx b/protocols/tests/identities/dual_identity_d1/dual_identity_d1.tx index 98932f1e..eb09ccfa 100644 --- a/protocols/tests/identities/dual_identity_d1/dual_identity_d1.tx +++ b/protocols/tests/identities/dual_identity_d1/dual_identity_d1.tx @@ -1,7 +1,6 @@ -trace { // ARGS: --verilog identities/dual_identity_d1/dual_identity_d1.v --protocol identities/dual_identity_d1/dual_identity_d1.prot // RETURN: 1 -one(3); -two(2, 3); - +trace { + one(3); + two(2, 3); } diff --git a/protocols/tests/identities/identity_d0/passthrough_combdep.tx b/protocols/tests/identities/identity_d0/passthrough_combdep.tx index e7bebdc7..08d0ac83 100644 --- a/protocols/tests/identities/identity_d0/passthrough_combdep.tx +++ b/protocols/tests/identities/identity_d0/passthrough_combdep.tx @@ -1,6 +1,5 @@ -trace { // ARGS: --verilog identities/identity_d0/identity_d0.v --protocol identities/identity_d0/identity_d0.prot // RETURN: 0 -passthrough(); - +trace { + passthrough(); } diff --git a/protocols/tests/identities/identity_d1/explicit_fork.out b/protocols/tests/identities/identity_d1/explicit_fork.out index 0ab2a325..6f350a86 100644 --- a/protocols/tests/identities/identity_d1/explicit_fork.out +++ b/protocols/tests/identities/identity_d1/explicit_fork.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 12 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 4, RHS Value: 3 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr3, expr2_id: expr4, value1: ValueOwned(00000000000000000000000000000100), value2: ValueOwned(00000000000000000000000000000011) }) Trace 0 execution failed. diff --git a/protocols/tests/identities/identity_d1/explicit_fork.tx b/protocols/tests/identities/identity_d1/explicit_fork.tx index bde62664..db1cf6b0 100644 --- a/protocols/tests/identities/identity_d1/explicit_fork.tx +++ b/protocols/tests/identities/identity_d1/explicit_fork.tx @@ -1,9 +1,8 @@ -trace { // ARGS: --verilog identities/identity_d1/identity_d1.v --protocol identities/identity_d1/identity_d1.prot // RETURN: 101 -explicit_fork(1, 1); -explicit_fork(2, 2); -explicit_fork(3, 4); -explicit_fork(4, 4); - +trace { + explicit_fork(1, 1); + explicit_fork(2, 2); + explicit_fork(3, 4); + explicit_fork(4, 4); } diff --git a/protocols/tests/identities/identity_d1/slicing_err.tx b/protocols/tests/identities/identity_d1/slicing_err.tx index 4d94831c..6e25fc2f 100644 --- a/protocols/tests/identities/identity_d1/slicing_err.tx +++ b/protocols/tests/identities/identity_d1/slicing_err.tx @@ -1,5 +1,5 @@ -trace { // ARGS: --verilog identities/identity_d1/identity_d1.v --protocol identities/identity_d1/slicing_err.prot // RETURN: 1 -slicing_err(1, 1); +trace { + slicing_err(1, 1); } diff --git a/protocols/tests/identities/identity_d1/slicing_invalid.tx b/protocols/tests/identities/identity_d1/slicing_invalid.tx index c72f46bf..2f96388e 100644 --- a/protocols/tests/identities/identity_d1/slicing_invalid.tx +++ b/protocols/tests/identities/identity_d1/slicing_invalid.tx @@ -1,5 +1,5 @@ -trace { // ARGS: --verilog identities/identity_d1/identity_d1.v --protocol identities/identity_d1/slicing_invalid.prot // RETURN: 1 -slicing_invalid(1, 1); +trace { + slicing_invalid(1, 1); } diff --git a/protocols/tests/identities/identity_d1/slicing_ok.tx b/protocols/tests/identities/identity_d1/slicing_ok.tx index 8fb72543..3451b978 100644 --- a/protocols/tests/identities/identity_d1/slicing_ok.tx +++ b/protocols/tests/identities/identity_d1/slicing_ok.tx @@ -1,4 +1,4 @@ -trace { // ARGS: --verilog identities/identity_d1/identity_d1.v --protocol identities/identity_d1/identity_d1.prot -slicing_ok(1, 1); +trace { + slicing_ok(1, 1); } diff --git a/protocols/tests/identities/identity_d2/single_thread_passes.tx b/protocols/tests/identities/identity_d2/single_thread_passes.tx index b7c97043..591658ea 100644 --- a/protocols/tests/identities/identity_d2/single_thread_passes.tx +++ b/protocols/tests/identities/identity_d2/single_thread_passes.tx @@ -1,5 +1,4 @@ -trace { // ARGS: --verilog identities/identity_d2/identity_d2.v --protocol identities/identity_d2/identity_d2.prot -multiple_assign(1, 1); - +trace { + multiple_assign(1, 1); } diff --git a/protocols/tests/identities/identity_d2/two_assignments_same_value.tx b/protocols/tests/identities/identity_d2/two_assignments_same_value.tx index bea1e3ec..16b54177 100644 --- a/protocols/tests/identities/identity_d2/two_assignments_same_value.tx +++ b/protocols/tests/identities/identity_d2/two_assignments_same_value.tx @@ -1,6 +1,5 @@ -trace { // ARGS: --verilog identities/identity_d2/identity_d2.v --protocol identities/identity_d2/identity_d2.prot -multiple_assign(1, 1); -multiple_assign(1, 1); - +trace { + multiple_assign(1, 1); + multiple_assign(1, 1); } diff --git a/protocols/tests/identities/identity_d2/two_different_assignments_error.out b/protocols/tests/identities/identity_d2/two_different_assignments_error.out index e5ce19db..f079f960 100644 --- a/protocols/tests/identities/identity_d2/two_different_assignments_error.out +++ b/protocols/tests/identities/identity_d2/two_different_assignments_error.out @@ -10,6 +10,4 @@ error: Thread 1 (`multiple_assign`) attempted conflicting assignment to 'a': cur 9 │ DUT.a := a; │ ^^^^^^^^^^^ Thread 1 (`multiple_assign`) attempted conflicting assignment to 'a': current=1, new=2 -Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000010), new_value: ValueOwned(00000000000000000000000000000001), thread_idx: 0, transaction_name: "multiple_assign", stmt_id: stmt4 }) -Trace 0 failed: Thread(ConflictingAssignment { symbol_id: symbol1, symbol_name: "a", current_value: ValueOwned(00000000000000000000000000000001), new_value: ValueOwned(00000000000000000000000000000010), thread_idx: 1, transaction_name: "multiple_assign", stmt_id: stmt1 }) Trace 0 execution failed. diff --git a/protocols/tests/identities/identity_d2/two_different_assignments_error.tx b/protocols/tests/identities/identity_d2/two_different_assignments_error.tx index 2c49dc78..88833713 100644 --- a/protocols/tests/identities/identity_d2/two_different_assignments_error.tx +++ b/protocols/tests/identities/identity_d2/two_different_assignments_error.tx @@ -1,7 +1,6 @@ -trace { // ARGS: --verilog identities/identity_d2/identity_d2.v --protocol identities/identity_d2/identity_d2.prot // RETURN: 101 -multiple_assign(1, 1); -multiple_assign(2, 2); - +trace { + multiple_assign(1, 1); + multiple_assign(2, 2); } diff --git a/protocols/tests/identities/identity_d2/two_fork_err.out b/protocols/tests/identities/identity_d2/two_fork_err.out index b7b891f3..29bc0b57 100644 --- a/protocols/tests/identities/identity_d2/two_fork_err.out +++ b/protocols/tests/identities/identity_d2/two_fork_err.out @@ -7,5 +7,4 @@ error: Thread 0 (transaction 'two_fork_err') attempted to fork more than once 25 │ fork(); │ ^^^^^^^ second fork() called here -Trace 0 failed: Thread(DoubleFork { thread_idx: 0, transaction_name: "two_fork_err", first_fork_stmt_id: stmt3, second_fork_stmt_id: stmt6 }) Trace 0 execution failed. diff --git a/protocols/tests/identities/identity_d2/two_fork_err.tx b/protocols/tests/identities/identity_d2/two_fork_err.tx index 2e5bc00b..12fdad2c 100644 --- a/protocols/tests/identities/identity_d2/two_fork_err.tx +++ b/protocols/tests/identities/identity_d2/two_fork_err.tx @@ -1,6 +1,5 @@ -trace { // ARGS: --verilog identities/identity_d2/identity_d2.v --protocol identities/identity_d2/identity_d2.prot // RETURN: 101 -two_fork_err(1, 1); - +trace { + two_fork_err(1, 1); } diff --git a/protocols/tests/identities/identity_d2/two_fork_ill_formed.tx b/protocols/tests/identities/identity_d2/two_fork_ill_formed.tx index 2ae6f28b..2188329c 100644 --- a/protocols/tests/identities/identity_d2/two_fork_ill_formed.tx +++ b/protocols/tests/identities/identity_d2/two_fork_ill_formed.tx @@ -1,6 +1,5 @@ -trace { // ARGS: --verilog identities/identity_d2/identity_d2.v --protocol identities/identity_d2/two_fork_ill_formed.prot // RETURN: 1 -two_fork_ok(1, 1); - +trace { + two_fork_ok(1, 1); } diff --git a/protocols/tests/inverters/inverter_d0.out b/protocols/tests/inverters/inverter_d0.out index 575a48c8..ed742179 100644 --- a/protocols/tests/inverters/inverter_d0.out +++ b/protocols/tests/inverters/inverter_d0.out @@ -4,5 +4,4 @@ error: Output 'DUT.s' depends on input(s) 'DUT.a' which do not have assigned val 7 │ DUT.a := DUT.s; │ ^^^^^ Output 'DUT.s' depends on input(s) 'DUT.a' which do not have assigned values ('DUT.a' initialized to DontCare and were never assigned a concrete value) -Trace 0 failed: Evaluation(ForbiddenPortRead { port_name: "DUT.s", unassigned_inputs: [("DUT.a", None)], expr_id: expr1 }) Trace 0 execution failed. diff --git a/protocols/tests/inverters/inverter_d0.tx b/protocols/tests/inverters/inverter_d0.tx index eb95ba13..8d2c6056 100644 --- a/protocols/tests/inverters/inverter_d0.tx +++ b/protocols/tests/inverters/inverter_d0.tx @@ -1,6 +1,5 @@ -trace { // ARGS: --verilog inverters/inverter_d0.v --protocol inverters/inverter_d0.prot // RETURN: 101 -invert(0, 1); - +trace { + invert(0, 1); } diff --git a/protocols/tests/multi/multi0/multi0.tx b/protocols/tests/multi/multi0/multi0.tx index 0470861b..ddc15528 100644 --- a/protocols/tests/multi/multi0/multi0.tx +++ b/protocols/tests/multi/multi0/multi0.tx @@ -1,5 +1,4 @@ -trace { // ARGS: --verilog multi/multi0/multi0.v --protocol multi/multi0/multi0.prot --module multi0 -multi(10, 10); - +trace { + multi(10, 10); } diff --git a/protocols/tests/multi/multi0keep/multi0keep.tx b/protocols/tests/multi/multi0keep/multi0keep.tx index cfbabb05..1b35821b 100644 --- a/protocols/tests/multi/multi0keep/multi0keep.tx +++ b/protocols/tests/multi/multi0keep/multi0keep.tx @@ -1,5 +1,4 @@ -trace { // ARGS: --verilog multi/multi0keep/multi0keep.v --protocol multi/multi0keep/multi0keep.prot --module multi0keep -multi(10, 10); - +trace { + multi(10, 10); } diff --git a/protocols/tests/multi/multi0keep2const/multi0keep2const.tx b/protocols/tests/multi/multi0keep2const/multi0keep2const.tx index 10aaf230..64f0b412 100644 --- a/protocols/tests/multi/multi0keep2const/multi0keep2const.tx +++ b/protocols/tests/multi/multi0keep2const/multi0keep2const.tx @@ -1,5 +1,4 @@ -trace { // ARGS: --verilog multi/multi0keep2const/multi0keep2const.v multi/multi0keep/multi0keep.v --protocol multi/multi0keep2const/multi0keep2const.prot --module multi0keep2const -multi(10, 10); - +trace { + multi(10, 10); } diff --git a/protocols/tests/multi/multi2const/multi2const.tx b/protocols/tests/multi/multi2const/multi2const.tx index 0f34956f..6b0b7aad 100644 --- a/protocols/tests/multi/multi2const/multi2const.tx +++ b/protocols/tests/multi/multi2const/multi2const.tx @@ -1,5 +1,4 @@ -trace { // ARGS: --verilog multi/multi2const/multi2const.v multi/multi0/multi0.v --protocol multi/multi2const/multi2const.prot --module multi2const -multi(10, 10); - +trace { + multi(10, 10); } diff --git a/protocols/tests/multi/multi2multi/multi2multi.tx b/protocols/tests/multi/multi2multi/multi2multi.tx index f9fe3b70..2790901f 100644 --- a/protocols/tests/multi/multi2multi/multi2multi.tx +++ b/protocols/tests/multi/multi2multi/multi2multi.tx @@ -1,5 +1,4 @@ -trace { // ARGS: --verilog multi/multi2multi/multi2multi.v multi/multi0/multi0.v --protocol multi/multi2multi/multi2multi.prot --module multi2multi -multi(10, 10); - +trace { + multi(10, 10); } diff --git a/protocols/tests/multi/multi_data/multi_data.tx b/protocols/tests/multi/multi_data/multi_data.tx index a13b8e6d..9fac4e40 100644 --- a/protocols/tests/multi/multi_data/multi_data.tx +++ b/protocols/tests/multi/multi_data/multi_data.tx @@ -1,5 +1,4 @@ -trace { // ARGS: --verilog multi/multi_data/multi_data.v --protocol multi/multi_data/multi_data.prot -multi(10, 10); - +trace { + multi(10, 10); } diff --git a/protocols/tests/multipliers/mult_d2/both_threads_fail.out b/protocols/tests/multipliers/mult_d2/both_threads_fail.out index d1f62fcb..274ce0a0 100644 --- a/protocols/tests/multipliers/mult_d2/both_threads_fail.out +++ b/protocols/tests/multipliers/mult_d2/both_threads_fail.out @@ -10,6 +10,4 @@ error: The two expressions did not evaluate to the same value 22 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 47, RHS Value: 48 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr7, expr2_id: expr8, value1: ValueOwned(00000000000000000000000000000011), value2: ValueOwned(00000000000000000000000000000010) }) -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr7, expr2_id: expr8, value1: ValueOwned(00000000000000000000000000101111), value2: ValueOwned(00000000000000000000000000110000) }) Trace 0 execution failed. diff --git a/protocols/tests/multipliers/mult_d2/both_threads_fail.tx b/protocols/tests/multipliers/mult_d2/both_threads_fail.tx index ec23026b..426c83a0 100644 --- a/protocols/tests/multipliers/mult_d2/both_threads_fail.tx +++ b/protocols/tests/multipliers/mult_d2/both_threads_fail.tx @@ -1,9 +1,6 @@ -trace { // ARGS: --verilog multipliers/mult_d2/mult_d2.v --protocol multipliers/mult_d2/mult_d2.prot // RETURN: 101 -mul(1, 2, 3); -mul(6, 8, 47); - - - +trace { + mul(1, 2, 3); + mul(6, 8, 47); } diff --git a/protocols/tests/multipliers/mult_d2/both_threads_pass.tx b/protocols/tests/multipliers/mult_d2/both_threads_pass.tx index 9ab45831..6e5473f4 100644 --- a/protocols/tests/multipliers/mult_d2/both_threads_pass.tx +++ b/protocols/tests/multipliers/mult_d2/both_threads_pass.tx @@ -1,6 +1,5 @@ -trace { // ARGS: --verilog multipliers/mult_d2/mult_d2.v --protocol multipliers/mult_d2/mult_d2.prot -mul(1, 2, 2); -mul(6, 8, 48); - +trace { + mul(1, 2, 2); + mul(6, 8, 48); } diff --git a/protocols/tests/multipliers/mult_d2/first_thread_fails.out b/protocols/tests/multipliers/mult_d2/first_thread_fails.out index 9c5317fa..7303751a 100644 --- a/protocols/tests/multipliers/mult_d2/first_thread_fails.out +++ b/protocols/tests/multipliers/mult_d2/first_thread_fails.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 22 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 3, RHS Value: 2 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr7, expr2_id: expr8, value1: ValueOwned(00000000000000000000000000000011), value2: ValueOwned(00000000000000000000000000000010) }) Trace 0 execution failed. diff --git a/protocols/tests/multipliers/mult_d2/first_thread_fails.tx b/protocols/tests/multipliers/mult_d2/first_thread_fails.tx index b6205f97..127b18f7 100644 --- a/protocols/tests/multipliers/mult_d2/first_thread_fails.tx +++ b/protocols/tests/multipliers/mult_d2/first_thread_fails.tx @@ -1,9 +1,6 @@ -trace { // ARGS: --verilog multipliers/mult_d2/mult_d2.v --protocol multipliers/mult_d2/mult_d2.prot // RETURN: 101 -mul(1, 2, 3); -mul(6, 8, 48); - - - +trace { + mul(1, 2, 3); + mul(6, 8, 48); } diff --git a/protocols/tests/multipliers/mult_d2/second_thread_fails.out b/protocols/tests/multipliers/mult_d2/second_thread_fails.out index 24675e70..b64a0b7c 100644 --- a/protocols/tests/multipliers/mult_d2/second_thread_fails.out +++ b/protocols/tests/multipliers/mult_d2/second_thread_fails.out @@ -4,5 +4,4 @@ error: The two expressions did not evaluate to the same value 22 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 47, RHS Value: 48 -Trace 0 failed: Assertion(EqualityFailed { expr1_id: expr7, expr2_id: expr8, value1: ValueOwned(00000000000000000000000000101111), value2: ValueOwned(00000000000000000000000000110000) }) Trace 0 execution failed. diff --git a/protocols/tests/multipliers/mult_d2/second_thread_fails.tx b/protocols/tests/multipliers/mult_d2/second_thread_fails.tx index 90294af2..6bde8276 100644 --- a/protocols/tests/multipliers/mult_d2/second_thread_fails.tx +++ b/protocols/tests/multipliers/mult_d2/second_thread_fails.tx @@ -1,9 +1,6 @@ -trace { // ARGS: --verilog multipliers/mult_d2/mult_d2.v --protocol multipliers/mult_d2/mult_d2.prot // RETURN: 101 -mul(1, 2, 2); -mul(6, 8, 47); - - - +trace { + mul(1, 2, 2); + mul(6, 8, 47); } diff --git a/protocols/tests/picorv32/unsigned_mul_no_reset.out b/protocols/tests/picorv32/unsigned_mul_no_reset.out index d2b8cd34..688eb263 100644 --- a/protocols/tests/picorv32/unsigned_mul_no_reset.out +++ b/protocols/tests/picorv32/unsigned_mul_no_reset.out @@ -1,5 +1,4 @@ Error error: Reached the maximum number of steps: 200 -Trace 0 failed: MaxStepsReached(200) Trace 0 execution failed. diff --git a/protocols/tests/picorv32/unsigned_mul_no_reset.tx b/protocols/tests/picorv32/unsigned_mul_no_reset.tx index 2bf630c6..ff74c881 100644 --- a/protocols/tests/picorv32/unsigned_mul_no_reset.tx +++ b/protocols/tests/picorv32/unsigned_mul_no_reset.tx @@ -1,9 +1,9 @@ -trace { // ARGS: --verilog ../../examples/picorv32/picorv32.v --protocol picorv32/pcpi_mul_no_reset.prot --module picorv32_pcpi_mul --max-steps 200 // RETURN: 101 -pcpi_mul_reset_normal(); -pcpi_mul(1, 1, 1); -pcpi_mul(1, 100, 100); -pcpi_mul(100, 1, 100); -pcpi_mul(33554483, 200, 2415929304); +trace { + pcpi_mul_reset_normal(); + pcpi_mul(1, 1, 1); + pcpi_mul(1, 100, 100); + pcpi_mul(100, 1, 100); + pcpi_mul(33554483, 200, 2415929304); } diff --git a/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.out b/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.out index d2b8cd34..688eb263 100644 --- a/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.out +++ b/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.out @@ -1,5 +1,4 @@ Error error: Reached the maximum number of steps: 200 -Trace 0 failed: MaxStepsReached(200) Trace 0 execution failed. diff --git a/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.tx b/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.tx index d782f82e..71db18e1 100644 --- a/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.tx +++ b/protocols/tests/picorv32/unsigned_mul_no_reset_thread_assignment_persistence.tx @@ -1,9 +1,9 @@ -trace { // ARGS: --verilog ../../examples/picorv32/picorv32.v --protocol picorv32/pcpi_mul_no_reset.prot --module picorv32_pcpi_mul --max-steps 200 // RETURN: 101 -pcpi_mul_reset_one(); -pcpi_mul(1, 1, 1); -pcpi_mul(1, 100, 100); -pcpi_mul(100, 1, 100); -pcpi_mul(33554483, 200, 2415929304); +trace { + pcpi_mul_reset_one(); + pcpi_mul(1, 1, 1); + pcpi_mul(1, 100, 100); + pcpi_mul(100, 1, 100); + pcpi_mul(33554483, 200, 2415929304); } From dc9d40b838912e91be229237f23bb6a80ceb8820 Mon Sep 17 00:00:00 2001 From: Nikil-Shyamsunder Date: Sat, 14 Feb 2026 21:32:09 -0800 Subject: [PATCH 3/3] fmt --- interp/src/main.rs | 1 - protocols/src/transactions_parser.rs | 13 ++++++++----- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/interp/src/main.rs b/interp/src/main.rs index 7bfa304a..4947d11d 100644 --- a/interp/src/main.rs +++ b/interp/src/main.rs @@ -62,7 +62,6 @@ 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(""); diff --git a/protocols/src/transactions_parser.rs b/protocols/src/transactions_parser.rs index 84a84b27..39a77760 100644 --- a/protocols/src/transactions_parser.rs +++ b/protocols/src/transactions_parser.rs @@ -50,11 +50,14 @@ pub fn parse_transactions_file( // 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 = vec![];