From 5500515c2dc47ac766a4ec99fdc2c46578d7453a Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 22 Feb 2026 21:11:17 -0500 Subject: [PATCH 1/3] Proceed to next stmt when encountering empty block instead of terminating thread --- monitor/src/interpreter.rs | 37 ++++++++++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/monitor/src/interpreter.rs b/monitor/src/interpreter.rs index 9c565251..c14a7a0a 100644 --- a/monitor/src/interpreter.rs +++ b/monitor/src/interpreter.rs @@ -488,7 +488,9 @@ impl Interpreter { } Stmt::Block(stmt_ids) => { if stmt_ids.is_empty() { - Ok(None) + // If we have an empty statement block, + // proceed directly to the next statement + Ok(self.next_stmt_map[stmt_id]) } else { Ok(Some(stmt_ids[0])) } @@ -958,6 +960,39 @@ impl Interpreter { "Cleared bindings for {} in `constraints` and `args_to_pins` due to DontCare assignment", self.symbol_table[*lhs_symbol_id].full_name(&self.symbol_table) ); + + // Even though the protocol says "don't care about this pin's value", + // the trace still has a concrete value for it. If there's an input + // parameter whose name matches the pin name and which hasn't been + // inferred yet, read the trace value and add the mapping. + // (e.g. `DUT.b := X` → still learn `b |-> trace_value(DUT.b)`) + // This ensures `to_protocol_application` can find all parameter values. + let pin_name = self.symbol_table[*lhs_symbol_id].name().to_string(); + if let Ok(trace_value) = trace.get(ctx.instance_id, *lhs_symbol_id) { + let transaction = self.transaction.clone(); + for arg in &transaction.args { + if let Dir::In = arg.dir() { + let param_symbol = arg.symbol(); + let param_name = self.symbol_table[param_symbol].name(); + if param_name == pin_name + && !self.args_mapping.contains_key(¶m_symbol) + { + let width = trace_value.width(); + self.args_mapping.insert(param_symbol, trace_value.clone()); + self.known_bits + .insert(param_symbol, BitVecValue::ones(width)); + self.args_to_pins.insert(param_symbol, *lhs_symbol_id); + info!( + "Inferred input parameter {} |-> {} from DontCare assignment to {}", + param_name, + serialize_bitvec(&trace_value, ctx.display_hex), + pin_name + ); + break; + } + } + } + } } Ok(()) } From 5ce1dc4ec48093cb31d2c71a72a8f08a5c10d6c5 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 22 Feb 2026 22:25:02 -0500 Subject: [PATCH 2/3] Add waveform file for combinational adder for monitor --- monitor/tests/adders/add_combinational.fst | Bin 0 -> 575 bytes monitor/tests/adders/add_combinational.out | 4 ++ monitor/tests/adders/add_combinational.prot | 44 ++++++++++++++++++++ 3 files changed, 48 insertions(+) create mode 100644 monitor/tests/adders/add_combinational.fst create mode 100644 monitor/tests/adders/add_combinational.out create mode 100644 monitor/tests/adders/add_combinational.prot diff --git a/monitor/tests/adders/add_combinational.fst b/monitor/tests/adders/add_combinational.fst new file mode 100644 index 0000000000000000000000000000000000000000..4ef73338c017587bf09e06124b21c029df297dfb GIT binary patch literal 575 zcmZQz00Tx(2n{D0Gs8u?x%RUdjb>yBNGvJJ&nqofD6T9nNzGNr%qvMP zDkw??l4xcOPc9qOTLw^Cx#b^2VoFMUiUB*r2NnT_LR%m%oCp`n2R5a9xZq(PcNYM4!6USfn(in a: u32, in b: u32, out s: u32) { +// DUT.a := X; +// DUT.b := X; +// DUT.a := a; + +// if (DUT.s == 32'b0) { // this should be illegal +// // pass +// } else { +// // pass +// } +// step(); +// } + +// prot add_combinational_illegal_observation_in_assertion(in a: u32, in b: u32, out s: u32) { +// DUT.a := X; +// DUT.b := X; +// DUT.a := a; + +// assert_eq(DUT.s, s); // this should be illegal +// step(); +// } + +prot add_combinational_legal_observation_illegal_assignment(in a: u32, in b: u32, out s: u32) { + if (DUT.s == 32'b0) { + DUT.a := a; // this should be illegal + } else { + + } + step(); +} + +prot add_combinational(in a: u32, in b: u32, out s: u32) { + DUT.a := a; + DUT.b := b; + assert_eq(s, DUT.s); + step(); +} \ No newline at end of file From 5e126f6fad43b097aefae20c2cabeffef5d9f65f Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 22 Feb 2026 22:27:13 -0500 Subject: [PATCH 3/3] Add ad-hoc fix to handle protocols that erroneously end with fork (ill-formed) --- monitor/src/scheduler.rs | 43 +++++++++++++++++++++++++++++++++------- 1 file changed, 36 insertions(+), 7 deletions(-) diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index 707d3ceb..e622bda7 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -432,7 +432,8 @@ impl Scheduler { } let finished_thread = &finished[0]; - // ...and there shouldn't be any other threads in `next` + // ...if there are other threads from the same start cycle still in `next`, + // eliminate them — only one protocol can win per start cycle. let next = threads_with_start_time(&self.next, start_cycle); if !next.is_empty() { let start_time_str = if ctx.show_waveform_time { @@ -440,20 +441,29 @@ impl Scheduler { } else { format!("cycle {}", finished_thread.start_cycle) }; - let error_context = anyhow!( - "Thread {} (`{}`) finished but there are other threads with the same start time ({}) in the `next` queue, namely {:?}", + info!( + "Thread {} (`{}`) finished at {}; failing {} competing thread(s) from the same start time: {:?}", finished_thread.global_thread_id(ctx), finished_thread.transaction.name, start_time_str, + next.len(), next.iter() .map(|t| t.transaction.name.clone()) .collect::>() ); - - return Err(SchedulerError::NoTransactionsMatch { - struct_name: self.struct_name.clone(), - error_context, + let next_thread_ids: Vec = next.iter().map(|t| t.thread_id).collect(); + let mut threads_to_fail = Vec::new(); + self.next.retain(|t| { + if next_thread_ids.contains(&t.thread_id) { + threads_to_fail.push(t.clone()); + false + } else { + true + } }); + for t in threads_to_fail { + self.failed.push_back(t); + } } } @@ -748,6 +758,25 @@ impl Scheduler { } } Ok(None) => { + // If `current_stmt_id` is a `Fork` statement and there is no + // `next_stmt_id`, it means the protocol ended with `fork()` + // as its last statement -- this is an ill-formed protocol. + // In this case, we treat this thread as having failed. + // (if we treated this thread as having finished + // successfully, it would incorrectly terminate other threads + // from the same start cycle that are still in `next`.) + // TODO: this is an ad-hoc fix for now (see Slack discussion) + if matches!(thread.transaction[current_stmt_id], Stmt::Fork) { + info!( + "Thread {} (`{}`) reached end of function after skipping `fork()`. Marking as failed.", + thread.global_thread_id(ctx), + self.format_transaction_name(ctx, thread.transaction.name.clone()) + ); + self.failed.push_back(thread); + self.print_scheduler_state(trace, ctx); + return Ok(ThreadResult::Completed); + } + // Check if another thread has already finished in this cycle. // Invariant: Only one thread per struct can finish per cycle if let Some((first_start_cycle, first_thread_id, first_transaction_name)) =