[Interp] Assignment Handling Overhaul and Implicit Input Reapplication

[Nikil-Shyamsunder]

This PR makes two major changes to how input assignments work in the Protocols interpreter: first, I overhauled the assignment semantics to allow threads to "change their mind" about input values while still detecting inter-thread conflicts; second, I implemented implicit input reapplication that persists values across cycles using the same assignment machinery.

Part 1: Overhauled Assignment Semantics

The previous system used an InputValue enum with three states (OldValue, NewValue, and DontCare) that formed a lattice for conflict detection. Once any thread set an input to a value (even DontCare), any subsequent change by any thread (including the same thread) would trigger a conflict error. This was overly restrictive: if a thread assigned a := 5 in one statement and later wanted to assign a := 10, this would fail even though there was no inter-thread conflict.

The new system relaxes this restriction. A thread can now "change its mind" about an input value. that is, it can assign a := 5, then later assign a := 10 or a := X, and this is perfectly valid. The conflict detection now only triggers when different threads disagree on concrete values. If Thread 0 assigns a := 5 and Thread 1 assigns a := 10, this is an error. But if Thread 0 assigns a := 5 and later Thread 0 itself assigns a := 10, this is allowed (assuming no conflicts with other threads).

Implementing this requires tracking the most recent input value on a per-thread basis. I introduced a new data structure per_thread_input_vals: FxHashMap<SymbolId, FxHashMap<usize, ThreadInputValue>> that maps each input pin to a map of thread IDs to their values. The ThreadInputValue enum is much simpler than before, with just two variants: Concrete(BitVecValue) or DontCare.

When a thread executes an assignment, we check if any other thread (not including the current thread) has assigned a different concrete value to that pin. If so, we raise a conflict error. Otherwise, we update the current thread's entry in the map and immediately apply the value to the simulator. DontCare assignments implement a consensus mechanism. When a thread assigns a := X, we check if any other thread currently has a concrete value for a. If another thread has a := 5, we do nothing i.e. their concrete value remains in the simulator. But if all other threads also have DontCare for a, we randomize a in the simulator. This ensures that inputs are only randomized when all active threads agree they should be DontCare.

Part 2: Implicit Input Reapplication

Since we now track the most recent assignment per thread in per_thread_input_vals, implementing implicit input reapplication becomes natural: at the start of each cycle, we simply reapply each thread's most recent assignments using the exact same assignment machinery as explicit assignments, so the semantics are identical. Threads can then change their mind about implicitly reapplied values by applying an explicit assignment as allowed by the work in part 1.

Thread lifecycle is straightforward. When a thread starts (either as an initial transaction or via implicit fork), we call init_new_thread(thread_id) to initialize all input pins to DontCare for that thread. This ensures every thread has an entry for every pin—there's no "no opinion" state. When a thread completes, we call clear_thread_inputs(thread_id) to remove all its entries from the maps, ensuring it no longer influences the DontCare consensus for ongoing threads.

For combinational dependency tracking, we use reference counting to handle the fact that assignments can be overwritten within a thread. Since a thread can assign a concrete value to an input and then change it to DontCare within the same cycle, we need to track how many inputs affecting each output are currently DontCare. The forbidden_output_counts map maintains a count for each output pin. When a thread assigns an input from Concrete to DontCare, we increment the count for all outputs combinationally dependent on that input. When a thread assigns from DontCare to Concrete, we decrement those counts. This reference counting is necessary because multiple input pins can affect the same output pin combinationally; after setting one input to Concrete, we cannot simply clear the forbidden status of the output; we must decrement its count by one. An output is forbidden to observe if its count is greater than zero, meaning at least one input in its combinational cone is currently assigned to DontCare.

Test Changes

Several test outputs changed due to the new execution model. For conflict error tests (adder_d1/add_incorrect.tx, adder_d2/no_dontcare_conflict.tx, and identity_d2/two_different_assignments_error.tx), the error messages now report "Thread 1" instead of "Thread 0" as the source of the conflict. This is simply due to different execution ordering (that is more straight forward now, threads are just number from 0 to n in order they appear in the transaction file, and they are executed deterministically in the order in which they appear in the transaction file just to make the .out files stay the same). it just reports the specific thread making the conflicting assignment.

The identity_d0/passthrough_combdep.tx test previously failed but now passes. The protocol assigns a := 0, steps, observes output b (which combinationally depends on a), and steps again. With cycle-start implicit reapplication, the sticky value a := 0 is reapplied at the beginning of cycle 2 before any dependency checking occurs. In the old system, dependency checking happened first and would mark a as forbidden, causing the implicit reapplication to error. Now the reapplication happens cleanly before the protocol observes anything, so no error is raised.

We had a bug in brave_new_world/use_without_valid/use_without_valid.prot where the protocol never explicitly initialized data_val to 0, relying on it being randomly initialized to 0. With the new randomization timing, data_val could be randomized to 1 in cycle 2, causing extra accumulation. We fixed this by adding an explicit dut.data_val := 1'b0; initialization.

Deleted examples/picorv32/unsigned_mul_no_reset.tx and pcpi_mul_no_reset.prot. This test was fundamentally incorrect and had an unexpected behavior before. Now the behavior is as expected (program hangs), so the test has been deleted. This might take some time to fix, so I will address it in a new PR and it's already issue #94.

We added four new tests in adders/adder_d0/ to verify that combinational dependency tracking with reference counting works correctly. The adder has two inputs (a and b) that both combinationally affect output s, making it an ideal test case for reference counting. The test illegal_observation_conditional.tx verifies that observing s in a conditional after setting a := X (with b implicitly initialized to DontCare) correctly triggers a forbidden port error; even though a was subsequently assigned a concrete value, b remains DontCare so the count stays at 1 (greater than 0). Similarly, illegal_observation_assertion.tx checks the same semantics but in an assertion context. The test illegal_assignment.tx verifies the reverse direction: observing s first (when both inputs are DontCare) marks both a and b as forbidden, and attempting to assign to a afterward correctly errors. Finally, add_combinational.tx is the valid case where both inputs are assigned concrete values before observing the output, demonstrating that when all dependent inputs are concrete (count = 0), observation is allowed. These tests ensure that the reference counting properly tracks multiple DontCare inputs affecting the same output and correctly forbids observations when any dependent input remains DontCare.

[ngernest]

This all looks good to me, great job! I like the idea of using referencing counting to track combinational dependents & viewing DontCare assignment between threads as a consensus mechanism (both are conceptually elegant)!

I just pushed a few commits that:

1. merge with main
2. Use the serialize_bitvec function in serialize.rs to pretty-print bit-vector values so that error messages look nicer (i.e. they print out decimal values, e.g. "5" instead of a long binary-string)

Hopefully this is OK!

I'll defer to @ekiwi to see if he has any other comments!

[ngernest]

I was planning on also pretty-printing BitVecValues for the "these two expressions did not evaluate to the same value" error message (i.e. render them in decimal instead of binary), but I realized that would involve changing too many .out Turnt files to pass CI, and make the PR harder for Kevin to review. (I'll create an issue for it since its not germane to this PR)

[Nikil-Shyamsunder]

I'm going to merge this because for the sake of WIP PRs that are branched off of this. If things need to change, they can be addressed in a future PR.