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..561ed954 100644 --- a/examples/picorv32/unsigned_mul.tx +++ b/examples/picorv32/unsigned_mul.tx @@ -1,6 +1,8 @@ // ARGS: --verilog picorv32/picorv32.v --protocol picorv32/pcpi_mul.prot --module picorv32_pcpi_mul -pcpi_mul_reset(); -pcpi_mul(1, 1, 1); -pcpi_mul(1, 100, 100); -pcpi_mul(100, 1, 100); -pcpi_mul(33554483, 200, 2415929304); +trace { + pcpi_mul_reset(); + pcpi_mul(1, 1, 1); + pcpi_mul(1, 100, 100); + pcpi_mul(100, 1, 100); + pcpi_mul(33554483, 200, 2415929304); +} 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..cf85cc11 100644 --- a/examples/serv/serv_regfile.tx +++ b/examples/serv/serv_regfile.tx @@ -1,11 +1,13 @@ // ARGS: --verilog serv/rtl/serv_regfile.v --protocol serv/serv_regfile.prot -// Arguments to transaction are: -// rs1_addr: u5 -// rs1_data: u32 (output) -// rs2_data: u32 (output) -// rs2_addr: u5 -// rd_enable: u1 -// rd_addr: u5 -// rd_data: u32 -read_write(0, 0, 0, 0, 1, 5, 0xdeadbeef); -read_write(5, 0xdeadbeef, 0, 0, 0, 0, 0); +trace { + // Arguments to transaction are: + // rs1_addr: u5 + // rs1_data: u32 (output) + // rs2_data: u32 (output) + // rs2_addr: u5 + // rd_enable: u1 + // rd_addr: u5 + // rd_data: u32 + read_write(0, 0, 0, 0, 1, 5, 0xdeadbeef); + read_write(5, 0xdeadbeef, 0, 0, 0, 0, 0); +} 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..ebfeb5b0 100644 --- a/examples/tinyaes128/aes128.tx +++ b/examples/tinyaes128/aes128.tx @@ -1,4 +1,6 @@ // ARGS: --verilog tinyaes128/aes_128.v --protocol tinyaes128/aes128.prot --module aes_128 -// Arguments are key, state, expected output -aes128(0x000102030405060708090a0b0c0d0e0f, 0x00112233445566778899aabbccddeeff, 0x69c4e0d86a7b0430d8cdb78070b4c55a); -aes128(0x00000000000000000000000000000000, 0x00000000000000000000000000000000, 0x66e94bd4ef8a2c3b884cfa59ca342b2e); +trace { + // Arguments are key, state, expected output + aes128(0x000102030405060708090a0b0c0d0e0f, 0x00112233445566778899aabbccddeeff, 0x69c4e0d86a7b0430d8cdb78070b4c55a); + aes128(0x00000000000000000000000000000000, 0x00000000000000000000000000000000, 0x66e94bd4ef8a2c3b884cfa59ca342b2e); +} diff --git a/interp/src/main.rs b/interp/src/main.rs index 2771c579..4947d11d 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,31 @@ struct Cli { /// $ cargo run --package protocols-interp -- --verilog protocols/tests/counters/counter.v -p protocols/tests/counters/counter.prot -t protocols/tests/counters/counter.tx -v /// $ cargo run --package protocols-interp -- --verilog protocols/tests/identities/dual_identity_d1/dual_identity_d1.v -p protocols/tests/identities/dual_identity_d1/dual_identity_d1.prot -t tests/identities/dual_identity_d1/dual_identity_d1.tx /// ``` +fn with_trace_suffix(path: &str, trace_index: usize) -> String { + let path = std::path::Path::new(path); + let stem = path.file_stem().and_then(|s| s.to_str()).unwrap_or(""); + let ext = path.extension().and_then(|e| e.to_str()); + + let file_name = if stem.is_empty() { + if let Some(ext) = ext { + format!("trace_{}.{}", trace_index, ext) + } else { + format!("trace_{}", trace_index) + } + } else if let Some(ext) = ext { + format!("{}_{}.{}", stem, trace_index, ext) + } else { + format!("{}_{}", stem, trace_index) + }; + + match path.parent() { + Some(parent) if !parent.as_os_str().is_empty() => { + parent.join(file_name).to_string_lossy().to_string() + } + _ => file_name, + } +} + fn main() -> anyhow::Result<()> { // Parse CLI args let cli = Cli::parse(); @@ -107,34 +132,48 @@ fn main() -> anyhow::Result<()> { // Create a separate `DiagnosticHandler` when parsing the transactions file let transactions_handler = &mut DiagnosticHandler::new(color_choice, cli.no_error_locations, emit_warnings); - let todos: Vec<(String, Vec)> = 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() { + if trace_index > 0 { + println!("\n---\n"); + } + + // Run each trace in isolation with a fresh interpreter and scheduler. + let interpreter = if let Some(waveform_file) = &cli.fst { + let waveform_file = with_trace_suffix(waveform_file, trace_index); + patronus::sim::Interpreter::new_with_wavedump(&ctx, &sys, waveform_file) + } else { + patronus::sim::Interpreter::new(&ctx, &sys) + }; + + let mut scheduler = Scheduler::new( + transactions_and_symbols.clone(), + todos, + &ctx, + &sys, + interpreter, + protocols_handler, + cli.max_steps.unwrap_or(u32::MAX), + ); + let results = scheduler.execute_todos(); + let trace_failed = results.iter().any(|res| res.is_err()); + + if trace_failed { + any_failed = true; + println!("Trace {} execution failed.", trace_index); + } else { + println!("Trace {} executed successfully!", trace_index); + } + } - // Check whether the protocol was executed successfully - for res in results { - assert_ok(&res) + if any_failed { + panic!("One or more traces failed."); } - println!("Protocol executed successfully!"); Ok(()) } 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..39a77760 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,44 @@ pub fn parse_transactions_file( // Access the `Rule`s contained within the parsed result let inner_rules = parse_result.unwrap().next().unwrap().into_inner(); - let mut todos = vec![]; + let mut traces: Vec> = vec![]; - // 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..d7dcc15a 100644 --- a/protocols/tests/adders/adder_d0/add_combinational.tx +++ b/protocols/tests/adders/adder_d0/add_combinational.tx @@ -1,2 +1,4 @@ // ARGS: --verilog adders/adder_d0/add_d0.v --protocol adders/adder_d0/add_d0.prot -add_combinational(100, 200, 300); +trace { + add_combinational(100, 200, 300); +} diff --git a/protocols/tests/adders/adder_d0/illegal_assignment.out b/protocols/tests/adders/adder_d0/illegal_assignment.out index f991efad..02ca04ca 100644 --- a/protocols/tests/adders/adder_d0/illegal_assignment.out +++ b/protocols/tests/adders/adder_d0/illegal_assignment.out @@ -4,3 +4,4 @@ error: Output 'DUT.s' depends on input(s) 'DUT.b', 'DUT.a' which do not have ass 30 │ if (DUT.s == 32'b0) { │ ^^^^^ Output 'DUT.s' depends on input(s) 'DUT.b', 'DUT.a' which do not have assigned values ('DUT.b', 'DUT.a' initialized to DontCare and were never assigned a concrete value) +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d0/illegal_assignment.tx b/protocols/tests/adders/adder_d0/illegal_assignment.tx index 12c78934..281169ad 100644 --- a/protocols/tests/adders/adder_d0/illegal_assignment.tx +++ b/protocols/tests/adders/adder_d0/illegal_assignment.tx @@ -1,3 +1,5 @@ // ARGS: --verilog adders/adder_d0/add_d0.v --protocol adders/adder_d0/add_d0.prot // RETURN: 101 -add_combinational_legal_observation_illegal_assignment(7, 8, 15); +trace { + add_combinational_legal_observation_illegal_assignment(7, 8, 15); +} diff --git a/protocols/tests/adders/adder_d0/illegal_observation_assertion.out b/protocols/tests/adders/adder_d0/illegal_observation_assertion.out index e9e8457d..b6878884 100644 --- a/protocols/tests/adders/adder_d0/illegal_observation_assertion.out +++ b/protocols/tests/adders/adder_d0/illegal_observation_assertion.out @@ -7,3 +7,4 @@ error: Output 'DUT.s' depends on input(s) 'DUT.b' which do not have assigned val 25 │ assert_eq(DUT.s, s); // this should be illegal │ ^^^^^ Output 'DUT.s' depends on input(s) 'DUT.b' which do not have assigned values +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d0/illegal_observation_assertion.tx b/protocols/tests/adders/adder_d0/illegal_observation_assertion.tx index b72dfd09..d42f3269 100644 --- a/protocols/tests/adders/adder_d0/illegal_observation_assertion.tx +++ b/protocols/tests/adders/adder_d0/illegal_observation_assertion.tx @@ -1,3 +1,5 @@ // ARGS: --verilog adders/adder_d0/add_d0.v --protocol adders/adder_d0/add_d0.prot // RETURN: 101 -add_combinational_illegal_observation_in_assertion(10, 20, 30); +trace { + add_combinational_illegal_observation_in_assertion(10, 20, 30); +} diff --git a/protocols/tests/adders/adder_d0/illegal_observation_conditional.out b/protocols/tests/adders/adder_d0/illegal_observation_conditional.out index af6bb99d..91c0704e 100644 --- a/protocols/tests/adders/adder_d0/illegal_observation_conditional.out +++ b/protocols/tests/adders/adder_d0/illegal_observation_conditional.out @@ -7,3 +7,4 @@ error: Output 'DUT.s' depends on input(s) 'DUT.b' which do not have assigned val 12 │ if (DUT.s == 32'b0) { // this should be illegal │ ^^^^^ Output 'DUT.s' depends on input(s) 'DUT.b' which do not have assigned values +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d0/illegal_observation_conditional.tx b/protocols/tests/adders/adder_d0/illegal_observation_conditional.tx index 78fdd6ea..4c287cda 100644 --- a/protocols/tests/adders/adder_d0/illegal_observation_conditional.tx +++ b/protocols/tests/adders/adder_d0/illegal_observation_conditional.tx @@ -1,3 +1,5 @@ // ARGS: --verilog adders/adder_d0/add_d0.v --protocol adders/adder_d0/add_d0.prot // RETURN: 101 -add_combinational_illegal_observation_in_conditional(5, 3, 8); +trace { + add_combinational_illegal_observation_in_conditional(5, 3, 8); +} diff --git a/protocols/tests/adders/adder_d1/add_incorrect.out b/protocols/tests/adders/adder_d1/add_incorrect.out index 32e962d1..83d34e59 100644 --- a/protocols/tests/adders/adder_d1/add_incorrect.out +++ b/protocols/tests/adders/adder_d1/add_incorrect.out @@ -10,3 +10,4 @@ error: Thread 1 (`add_incorrect`) attempted conflicting assignment to 'a': curre 44 │ DUT.a := a; │ ^^^^^^^^^^^ Thread 1 (`add_incorrect`) attempted conflicting assignment to 'a': current=1, new=4 +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/add_incorrect.tx b/protocols/tests/adders/adder_d1/add_incorrect.tx index f55750fd..fee34936 100644 --- a/protocols/tests/adders/adder_d1/add_incorrect.tx +++ b/protocols/tests/adders/adder_d1/add_incorrect.tx @@ -1,4 +1,6 @@ // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 -add_incorrect(1, 2, 3); -add_incorrect(4, 5, 9); +trace { + add_incorrect(1, 2, 3); + add_incorrect(4, 5, 9); +} diff --git a/protocols/tests/adders/adder_d1/add_incorrect_implicit.out b/protocols/tests/adders/adder_d1/add_incorrect_implicit.out index f5da2d6b..cb716a66 100644 --- a/protocols/tests/adders/adder_d1/add_incorrect_implicit.out +++ b/protocols/tests/adders/adder_d1/add_incorrect_implicit.out @@ -10,3 +10,4 @@ error: Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to ' 55 │ DUT.a := a; │ ^^^^^^^^^^^ Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'a': current=1, new=4 +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/add_incorrect_implicit.tx b/protocols/tests/adders/adder_d1/add_incorrect_implicit.tx index 13966a09..84b4bf5e 100644 --- a/protocols/tests/adders/adder_d1/add_incorrect_implicit.tx +++ b/protocols/tests/adders/adder_d1/add_incorrect_implicit.tx @@ -1,4 +1,6 @@ // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 -add_incorrect_implicit(1, 2, 3); -add_incorrect_implicit(4, 5, 9); +trace { + add_incorrect_implicit(1, 2, 3); + add_incorrect_implicit(4, 5, 9); +} 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 8178f4d7..767e7dd9 100644 --- a/protocols/tests/adders/adder_d1/both_threads_fail.out +++ b/protocols/tests/adders/adder_d1/both_threads_fail.out @@ -10,3 +10,4 @@ error: The two expressions did not evaluate to the same value 26 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 10, RHS Value: 9 +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/both_threads_fail.tx b/protocols/tests/adders/adder_d1/both_threads_fail.tx index 3014f0bb..0e86e8be 100644 --- a/protocols/tests/adders/adder_d1/both_threads_fail.tx +++ b/protocols/tests/adders/adder_d1/both_threads_fail.tx @@ -1,4 +1,6 @@ // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/add_d1.prot // RETURN: 101 -add_fork_early(1, 2, 5); -add_fork_early(4, 5, 10); +trace { + add_fork_early(1, 2, 5); + add_fork_early(4, 5, 10); +} 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..640a6616 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 @@ // 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 +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 761cd89f..a543c5e8 100644 --- a/protocols/tests/adders/adder_d1/busy_wait_fail.out +++ b/protocols/tests/adders/adder_d1/busy_wait_fail.out @@ -4,3 +4,4 @@ error: The two expressions did not evaluate to the same value 21 │ assert_eq(s, DUT.s); │ ^^^^^^^^ LHS Value: 999, RHS Value: 3 +Trace 0 execution failed. diff --git a/protocols/tests/adders/adder_d1/busy_wait_fail.tx b/protocols/tests/adders/adder_d1/busy_wait_fail.tx index bfe7f705..3024a150 100644 --- a/protocols/tests/adders/adder_d1/busy_wait_fail.tx +++ b/protocols/tests/adders/adder_d1/busy_wait_fail.tx @@ -1,3 +1,5 @@ // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/busy_wait.prot // RETURN: 101 -add_busy_wait(1, 2, 2, 999); // Wrong output value, this transaction fails +trace { + add_busy_wait(1, 2, 2, 999); // Wrong output value, this transaction fails +} 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..df87db84 100644 --- a/protocols/tests/adders/adder_d1/busy_wait_pass.tx +++ b/protocols/tests/adders/adder_d1/busy_wait_pass.tx @@ -1,3 +1,5 @@ // ARGS: --verilog adders/adder_d1/add_d1.v --protocol adders/adder_d1/busy_wait.prot -add_busy_wait(1, 2, 1, 3); // Runs busy-waiting loop for 1 iteration -add_busy_wait(4, 5, 3, 9); // Runs busy-waiting loop for 3 iterations +trace { + add_busy_wait(1, 2, 1, 3); // Runs busy-waiting loop for 1 iteration + add_busy_wait(4, 5, 3, 9); // Runs busy-waiting loop for 3 iterations +} 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..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,3 +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 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..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,4 +1,5 @@ // 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 3178405a..67b41ecf 100644 --- a/protocols/tests/adders/adder_d1/double_fork_error.out +++ b/protocols/tests/adders/adder_d1/double_fork_error.out @@ -16,3 +16,4 @@ error: Thread 1 (transaction 'add_double_fork') attempted to fork more than once 15 │ fork(); │ ^^^^^^^ second fork() called here +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..aa036892 100644 --- a/protocols/tests/adders/adder_d1/double_fork_error.tx +++ b/protocols/tests/adders/adder_d1/double_fork_error.tx @@ -1,4 +1,6 @@ // 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 d777153b..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,3 +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 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..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,4 +1,6 @@ // 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 d777153b..9b436ef4 100644 --- a/protocols/tests/adders/adder_d1/first_thread_fails.out +++ b/protocols/tests/adders/adder_d1/first_thread_fails.out @@ -4,3 +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 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..bae9521d 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 @@ // 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 +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 0e0c58c5..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,3 +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 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..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,4 +1,6 @@ // 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.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..14ec302a 100644 --- a/protocols/tests/adders/adder_d1/loop_with_assigns.tx +++ b/protocols/tests/adders/adder_d1/loop_with_assigns.tx @@ -1,3 +1,5 @@ // 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.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..6315bb9f 100644 --- a/protocols/tests/adders/adder_d1/nested_busy_wait.tx +++ b/protocols/tests/adders/adder_d1/nested_busy_wait.tx @@ -1,3 +1,5 @@ // 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 181c1fd3..54efdc9c 100644 --- a/protocols/tests/adders/adder_d1/second_thread_fails.out +++ b/protocols/tests/adders/adder_d1/second_thread_fails.out @@ -4,3 +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 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..5409d117 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 @@ // 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 +trace { + add(1, 2, 3); + 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..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,4 +1,6 @@ // 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 1cf5f891..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,3 +10,4 @@ error: Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to ' 55 │ DUT.a := a; │ ^^^^^^^^^^^ Thread 1 (`add_incorrect_implicit`) attempted conflicting assignment to 'a': current=1, new=4 +Trace 0 execution failed. 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..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,4 +1,6 @@ // 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.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..91a2a3d1 100644 --- a/protocols/tests/adders/adder_d2/both_threads_pass.tx +++ b/protocols/tests/adders/adder_d2/both_threads_pass.tx @@ -1,4 +1,6 @@ // 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 58bc092e..ef370646 100644 --- a/protocols/tests/adders/adder_d2/no_dontcare_conflict.out +++ b/protocols/tests/adders/adder_d2/no_dontcare_conflict.out @@ -10,3 +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 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..0c5c16c5 100644 --- a/protocols/tests/adders/adder_d2/no_dontcare_conflict.tx +++ b/protocols/tests/adders/adder_d2/no_dontcare_conflict.tx @@ -1,4 +1,6 @@ // 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.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..20825157 100644 --- a/protocols/tests/alus/alu_d1.tx +++ b/protocols/tests/alus/alu_d1.tx @@ -1,6 +1,8 @@ // 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.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..8bdb53a2 100644 --- a/protocols/tests/alus/alu_d2.tx +++ b/protocols/tests/alus/alu_d2.tx @@ -1,6 +1,8 @@ // 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 39bc4515..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,3 +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 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..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,3 +1,5 @@ // 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 +trace { + 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..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,2 +1,4 @@ // 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 +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 89ecef55..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,3 +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 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..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,3 +1,5 @@ // 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 +trace { + 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..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,2 +1,4 @@ // 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 +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 24c950e5..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,3 +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 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..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,3 +1,5 @@ // 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 +trace { + 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..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,2 +1,4 @@ // 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 +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 2cf2e4f6..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,3 +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 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..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,3 +1,5 @@ // 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 +trace { + 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..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,2 +1,4 @@ // 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 +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 65fae905..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,3 +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 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..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,3 +1,5 @@ // 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 +trace { + 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..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,2 +1,4 @@ // 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 +trace { + 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..68cd16c4 100644 --- a/protocols/tests/counters/counter.tx +++ b/protocols/tests/counters/counter.tx @@ -1,2 +1,4 @@ // ARGS: --verilog counters/counter.v --protocol counters/counter.prot -count_up(10); +trace { + 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..aca45d80 100644 --- a/protocols/tests/fifo/fifo.tx +++ b/protocols/tests/fifo/fifo.tx @@ -1,7 +1,9 @@ // 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 8b9c925b..162b5fa2 100644 --- a/protocols/tests/fifo/pop_before_push_fail.out +++ b/protocols/tests/fifo/pop_before_push_fail.out @@ -4,3 +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 execution failed. diff --git a/protocols/tests/fifo/pop_before_push_fail.tx b/protocols/tests/fifo/pop_before_push_fail.tx index a88c4af0..f873fd42 100644 --- a/protocols/tests/fifo/pop_before_push_fail.tx +++ b/protocols/tests/fifo/pop_before_push_fail.tx @@ -1,9 +1,11 @@ // 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); \ No newline at end of file + 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 8b9c925b..162b5fa2 100644 --- a/protocols/tests/fifo/pop_empty_fail.out +++ b/protocols/tests/fifo/pop_empty_fail.out @@ -4,3 +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 execution failed. diff --git a/protocols/tests/fifo/pop_empty_fail.tx b/protocols/tests/fifo/pop_empty_fail.tx index d70a215d..72b35041 100644 --- a/protocols/tests/fifo/pop_empty_fail.tx +++ b/protocols/tests/fifo/pop_empty_fail.tx @@ -1,6 +1,8 @@ // 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); \ No newline at end of file + 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 bddcdc3e..c1b37511 100644 --- a/protocols/tests/fifo/push_pop_conflict.out +++ b/protocols/tests/fifo/push_pop_conflict.out @@ -4,3 +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 execution failed. diff --git a/protocols/tests/fifo/push_pop_conflict.tx b/protocols/tests/fifo/push_pop_conflict.tx index a3d69597..6f817a1b 100644 --- a/protocols/tests/fifo/push_pop_conflict.tx +++ b/protocols/tests/fifo/push_pop_conflict.tx @@ -1,6 +1,8 @@ // 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.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..cab2e0bc 100644 --- a/protocols/tests/fifo/push_pop_identity_ok.tx +++ b/protocols/tests/fifo/push_pop_identity_ok.tx @@ -1,8 +1,10 @@ // 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); \ No newline at end of file + reset(); + push(2); + pop(2); + idle(); + push(3); + 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..e58825b4 100644 --- a/protocols/tests/fifo/push_pop_loop_empty.tx +++ b/protocols/tests/fifo/push_pop_loop_empty.tx @@ -1,5 +1,7 @@ // 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.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..91d75f18 100644 --- a/protocols/tests/fifo/push_pop_loop_not_empty.tx +++ b/protocols/tests/fifo/push_pop_loop_not_empty.tx @@ -1,5 +1,7 @@ // 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 b5b23005..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,3 +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 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..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,8 +1,10 @@ // 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 496a95d8..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,4 +1,6 @@ // 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.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..08d0ac83 100644 --- a/protocols/tests/identities/identity_d0/passthrough_combdep.tx +++ b/protocols/tests/identities/identity_d0/passthrough_combdep.tx @@ -1,3 +1,5 @@ // 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 860a4602..6f350a86 100644 --- a/protocols/tests/identities/identity_d1/explicit_fork.out +++ b/protocols/tests/identities/identity_d1/explicit_fork.out @@ -4,3 +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 execution failed. diff --git a/protocols/tests/identities/identity_d1/explicit_fork.tx b/protocols/tests/identities/identity_d1/explicit_fork.tx index 24fc8c77..db1cf6b0 100644 --- a/protocols/tests/identities/identity_d1/explicit_fork.tx +++ b/protocols/tests/identities/identity_d1/explicit_fork.tx @@ -1,6 +1,8 @@ // 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 e2b6b5d5..6e25fc2f 100644 --- a/protocols/tests/identities/identity_d1/slicing_err.tx +++ b/protocols/tests/identities/identity_d1/slicing_err.tx @@ -1,3 +1,5 @@ // 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 +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 06a8ed0c..2f96388e 100644 --- a/protocols/tests/identities/identity_d1/slicing_invalid.tx +++ b/protocols/tests/identities/identity_d1/slicing_invalid.tx @@ -1,3 +1,5 @@ // 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 +trace { + 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..3451b978 100644 --- a/protocols/tests/identities/identity_d1/slicing_ok.tx +++ b/protocols/tests/identities/identity_d1/slicing_ok.tx @@ -1,2 +1,4 @@ // 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 +trace { + 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..591658ea 100644 --- a/protocols/tests/identities/identity_d2/single_thread_passes.tx +++ b/protocols/tests/identities/identity_d2/single_thread_passes.tx @@ -1,2 +1,4 @@ // 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.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..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,3 +1,5 @@ // 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 6281ccf4..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,3 +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 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..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,4 +1,6 @@ // 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 49c327d2..29bc0b57 100644 --- a/protocols/tests/identities/identity_d2/two_fork_err.out +++ b/protocols/tests/identities/identity_d2/two_fork_err.out @@ -7,3 +7,4 @@ error: Thread 0 (transaction 'two_fork_err') attempted to fork more than once 25 │ fork(); │ ^^^^^^^ second fork() called here +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..12fdad2c 100644 --- a/protocols/tests/identities/identity_d2/two_fork_err.tx +++ b/protocols/tests/identities/identity_d2/two_fork_err.tx @@ -1,3 +1,5 @@ // 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 0dfba0d7..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,3 +1,5 @@ // 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 b59ab5dc..ed742179 100644 --- a/protocols/tests/inverters/inverter_d0.out +++ b/protocols/tests/inverters/inverter_d0.out @@ -4,3 +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 execution failed. diff --git a/protocols/tests/inverters/inverter_d0.tx b/protocols/tests/inverters/inverter_d0.tx index 4a527b1b..8d2c6056 100644 --- a/protocols/tests/inverters/inverter_d0.tx +++ b/protocols/tests/inverters/inverter_d0.tx @@ -1,3 +1,5 @@ // 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.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..ddc15528 100644 --- a/protocols/tests/multi/multi0/multi0.tx +++ b/protocols/tests/multi/multi0/multi0.tx @@ -1,2 +1,4 @@ // 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.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..1b35821b 100644 --- a/protocols/tests/multi/multi0keep/multi0keep.tx +++ b/protocols/tests/multi/multi0keep/multi0keep.tx @@ -1,2 +1,4 @@ // 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.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..64f0b412 100644 --- a/protocols/tests/multi/multi0keep2const/multi0keep2const.tx +++ b/protocols/tests/multi/multi0keep2const/multi0keep2const.tx @@ -1,2 +1,4 @@ // 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.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..6b0b7aad 100644 --- a/protocols/tests/multi/multi2const/multi2const.tx +++ b/protocols/tests/multi/multi2const/multi2const.tx @@ -1,2 +1,4 @@ // 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.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..2790901f 100644 --- a/protocols/tests/multi/multi2multi/multi2multi.tx +++ b/protocols/tests/multi/multi2multi/multi2multi.tx @@ -1,2 +1,4 @@ // 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.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..9fac4e40 100644 --- a/protocols/tests/multi/multi_data/multi_data.tx +++ b/protocols/tests/multi/multi_data/multi_data.tx @@ -1,2 +1,4 @@ // 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 b095a57b..274ce0a0 100644 --- a/protocols/tests/multipliers/mult_d2/both_threads_fail.out +++ b/protocols/tests/multipliers/mult_d2/both_threads_fail.out @@ -10,3 +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 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..426c83a0 100644 --- a/protocols/tests/multipliers/mult_d2/both_threads_fail.tx +++ b/protocols/tests/multipliers/mult_d2/both_threads_fail.tx @@ -1,6 +1,6 @@ // 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.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..6e5473f4 100644 --- a/protocols/tests/multipliers/mult_d2/both_threads_pass.tx +++ b/protocols/tests/multipliers/mult_d2/both_threads_pass.tx @@ -1,3 +1,5 @@ // 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 2e83c080..7303751a 100644 --- a/protocols/tests/multipliers/mult_d2/first_thread_fails.out +++ b/protocols/tests/multipliers/mult_d2/first_thread_fails.out @@ -4,3 +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 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..127b18f7 100644 --- a/protocols/tests/multipliers/mult_d2/first_thread_fails.tx +++ b/protocols/tests/multipliers/mult_d2/first_thread_fails.tx @@ -1,6 +1,6 @@ // 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 25010251..b64a0b7c 100644 --- a/protocols/tests/multipliers/mult_d2/second_thread_fails.out +++ b/protocols/tests/multipliers/mult_d2/second_thread_fails.out @@ -4,3 +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 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..6bde8276 100644 --- a/protocols/tests/multipliers/mult_d2/second_thread_fails.tx +++ b/protocols/tests/multipliers/mult_d2/second_thread_fails.tx @@ -1,6 +1,6 @@ // 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 c842c3d8..688eb263 100644 --- a/protocols/tests/picorv32/unsigned_mul_no_reset.out +++ b/protocols/tests/picorv32/unsigned_mul_no_reset.out @@ -1,3 +1,4 @@ Error error: Reached the maximum number of steps: 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..ff74c881 100644 --- a/protocols/tests/picorv32/unsigned_mul_no_reset.tx +++ b/protocols/tests/picorv32/unsigned_mul_no_reset.tx @@ -1,7 +1,9 @@ // 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 +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 c842c3d8..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,3 +1,4 @@ Error error: Reached the maximum number of steps: 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..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,7 +1,9 @@ // 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 +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); +}