(WIP) [Monitor] Fix failing round-trip tests related to combinational adders

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(&param_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(())
             }

monitor/src/scheduler.rs

@@ -432,28 +432,38 @@ 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 {
                     trace.format_time(finished_thread.start_time_step, ctx.time_unit)
                 } 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::<Vec<_>>()
                 );
-
-                return Err(SchedulerError::NoTransactionsMatch {
-                    struct_name: self.struct_name.clone(),
-                    error_context,
+                let next_thread_ids: Vec<u32> = 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)) =

monitor/tests/adders/add_combinational.out

@@ -0,0 +1,4 @@
+// trace 0
+trace {
+    add_combinational(100, 200, 300);
+}

monitor/tests/adders/add_combinational.prot

@@ -0,0 +1,44 @@
+// ARGS: --wave adders/add_combinational.fst --instances add_d0:Adder 
+struct Adder {
+  in a: u32,
+  in b: u32,
+  out s: u32,
+}
+
+// prot add_combinational_illegal_observation_in_conditional<DUT: Adder>(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<DUT: Adder>(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<DUT: Adder>(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<DUT: Adder>(in a: u32, in b: u32, out s: u32) {
+  DUT.a := a;
+  DUT.b := b;
+  assert_eq(s, DUT.s);
+  step();
+}