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(()) } 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)) = diff --git a/monitor/tests/adders/add_combinational.fst b/monitor/tests/adders/add_combinational.fst new file mode 100644 index 00000000..4ef73338 Binary files /dev/null and b/monitor/tests/adders/add_combinational.fst differ diff --git a/monitor/tests/adders/add_combinational.out b/monitor/tests/adders/add_combinational.out new file mode 100644 index 00000000..f2558d06 --- /dev/null +++ b/monitor/tests/adders/add_combinational.out @@ -0,0 +1,4 @@ +// trace 0 +trace { + add_combinational(100, 200, 300); +} diff --git a/monitor/tests/adders/add_combinational.prot b/monitor/tests/adders/add_combinational.prot new file mode 100644 index 00000000..1ad36831 --- /dev/null +++ b/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(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