From 3793e713ca2a241bac35cd3e52fbad2990776f45 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 22 Feb 2026 19:53:49 -0500 Subject: [PATCH 1/6] Add adder_d1 files that trigger monitor bugs --- monitor/tests/adders/add_combinational.fst | Bin 0 -> 574 bytes monitor/tests/adders/add_combinational.out | 4 + monitor/tests/adders/add_combinational.prot | 44 +++++++++++ monitor/tests/adders/both_threads_pass.err | 0 monitor/tests/adders/both_threads_pass.fst | Bin 0 -> 604 bytes monitor/tests/adders/both_threads_pass.out | 5 ++ monitor/tests/adders/both_threads_pass.prot | 19 +++++ monitor/tests/adders/loop_with_assigns.err | 0 monitor/tests/adders/wait_and_add.fst | Bin 0 -> 620 bytes monitor/tests/adders/wait_and_add.prot | 81 ++++++++++++++++++++ 10 files changed, 153 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 create mode 100644 monitor/tests/adders/both_threads_pass.err create mode 100644 monitor/tests/adders/both_threads_pass.fst create mode 100644 monitor/tests/adders/both_threads_pass.out create mode 100644 monitor/tests/adders/both_threads_pass.prot create mode 100644 monitor/tests/adders/loop_with_assigns.err create mode 100644 monitor/tests/adders/wait_and_add.fst create mode 100644 monitor/tests/adders/wait_and_add.prot diff --git a/monitor/tests/adders/add_combinational.fst b/monitor/tests/adders/add_combinational.fst new file mode 100644 index 0000000000000000000000000000000000000000..83e5421ff6161418267612cb348bf9db030e1193 GIT binary patch literal 574 zcmZQz00Tx(2#p{!!$rEe_Om)5M8GUYD4!XPW@HFREGf#*D=k(it}HG|%~i0W&0mf%m dP*C82iY*n1ppbtM4tcv literal 0 HcmV?d00001 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..543bdb20 --- /dev/null +++ b/monitor/tests/adders/add_combinational.prot @@ -0,0 +1,44 @@ +// ARGS: --wave adders/add_combinational.fst --instances adder_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 diff --git a/monitor/tests/adders/both_threads_pass.err b/monitor/tests/adders/both_threads_pass.err new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/both_threads_pass.fst b/monitor/tests/adders/both_threads_pass.fst new file mode 100644 index 0000000000000000000000000000000000000000..bdd7aea26db401fd6a72beb663844a2df7802a27 GIT binary patch literal 604 zcmZQz00Tx(2n{EhGQ&l>x%RUJjb>yBNGvJJ&nqofD6T9nNzGNr%qvMP zDkw??l4xcOPc9qOTc%K2yX7B4VoFMUiXl70L;;3G1_cHIh9owI3&}az42(c_F;L_` zGgP$(in a: u32, in b: u32, out s: u32) { + DUT.a := a; + DUT.b := b; + step(); + DUT.a := X; + DUT.b := X; + assert_eq(s, DUT.s); + + fork(); + step(); +} diff --git a/monitor/tests/adders/loop_with_assigns.err b/monitor/tests/adders/loop_with_assigns.err new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/wait_and_add.fst b/monitor/tests/adders/wait_and_add.fst new file mode 100644 index 0000000000000000000000000000000000000000..1c4ef41152fcc6359bbb5de0bbda1c7f92002011 GIT binary patch literal 620 zcmZQz00Tx(2n{EhGs8u?x%RUJjb>yBNGvJJ&nqofD6T9nNzGNr%qvMP zDkw??l4xcOPc9qOTc%K2yX7B4VoFMUiXl70L;;3G1_cHIh9owI3&}az42(c_F;L_` zGgP$&8eEQW>#28KWYA`O595CaJq1!93AR0&uqPym8J uY6$`s6R@=`Oh5_}`>Y@)5Lb&cJOeQ~nZ=pJ!HO6dSQr^$Nd)FfI1K=Z(=D+8 literal 0 HcmV?d00001 diff --git a/monitor/tests/adders/wait_and_add.prot b/monitor/tests/adders/wait_and_add.prot new file mode 100644 index 00000000..fde08e6a --- /dev/null +++ b/monitor/tests/adders/wait_and_add.prot @@ -0,0 +1,81 @@ +// ARGS: --wave adders/wait_and_add.fst --instances add_d1:Adder +struct Adder { + in a: u32, + in b: u32, + out s: u32, +} + +// Adder with 1-cycle delay (i.e. `DUT.s` is only assigned after one cycle)s +prot add(in a: u32, in b: u32, out s: u32) { + DUT.a := a; + DUT.b := b; + step(); + DUT.a := X; + DUT.b := X; + assert_eq(s, DUT.s); + fork(); + step(); +} + +prot add_fork_early(in a: u32, in b: u32, out s: u32) { + DUT.a := a; + DUT.b := b; + step(); + fork(); + DUT.a := X; + DUT.b := X; + assert_eq(s, DUT.s); + step(); +} + +// Like `add` above, but this protocol doesn't end in `step`, +// so this function is ill-formed +prot add_doesnt_end_in_step(in a: u32, in b: u32, out s: u32) { + DUT.a := a; + DUT.b := b; + step(); + DUT.a := X; + DUT.b := X; + assert_eq(s, DUT.s); + fork(); +} + + +prot add_incorrect(in a: u32, in b: u32, out s: u32) { + DUT.a := a; + DUT.b := b; + step(); + DUT.a := a; + DUT.b := b; + assert_eq(s, DUT.s); + fork(); + step(); +} + +prot add_incorrect_implicit(in a: u32, in b: u32, out s: u32) { + DUT.a := a; + DUT.b := b; + step(); + + // missing DontCare assignments to DUT.a and DUT.b + + assert_eq(s, DUT.s); + fork(); + step(); +} + +prot wait_and_add(in a: u32, in b: u32, out s: u32) { + step(); + + fork(); + + step(); + + DUT.a := a; + DUT.b := b; + + step(); + + assert_eq(s, DUT.s); + step(); +} \ No newline at end of file From f7fbeea3beaad28ef8b0936ad596270c322564b4 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 22 Feb 2026 20:12:41 -0500 Subject: [PATCH 2/6] Fix waveform file for wait_and_add --- monitor/tests/adders/loop_with_assigns.err | 0 monitor/tests/adders/wait_and_add.fst | Bin 620 -> 626 bytes 2 files changed, 0 insertions(+), 0 deletions(-) delete mode 100644 monitor/tests/adders/loop_with_assigns.err diff --git a/monitor/tests/adders/loop_with_assigns.err b/monitor/tests/adders/loop_with_assigns.err deleted file mode 100644 index e69de29b..00000000 diff --git a/monitor/tests/adders/wait_and_add.fst b/monitor/tests/adders/wait_and_add.fst index 1c4ef41152fcc6359bbb5de0bbda1c7f92002011..5ecf8ea2fb70e7fbd1d70a5cc16ab3b85b183035 100644 GIT binary patch delta 68 zcmaFE@`+`F1S88v$sR_@D-5WB1hl;W=GBQpy0O|z*aOemL delta 82 wcmeyw@`h!C1S9iC$sR_@a}20}8OoKLypOS6omreo94f%V$jAs~!qmWN0MZ}_H2?qr From 09200d60c06f058343a7ef96bc398f71a0fb3102 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 22 Feb 2026 20:32:50 -0500 Subject: [PATCH 3/6] Ensure that interpreter calls simulator.step even when next_threads queue is empty --- protocols/src/scheduler.rs | 25 ++++++++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) diff --git a/protocols/src/scheduler.rs b/protocols/src/scheduler.rs index bb87d0c0..340c79fb 100644 --- a/protocols/src/scheduler.rs +++ b/protocols/src/scheduler.rs @@ -167,6 +167,13 @@ pub struct Scheduler<'a> { results: Vec>, /// Handler for error diagnostics handler: &'a mut DiagnosticHandler, + /// Flag that tracks whether any thread executed a `step()` statement + /// in the current scheduling cycle. This is used to ensure + /// that the simulator's `sim_step()` method is called even when all + /// threads have completed and the `next_threads` queue is empty + /// (this is necessary to produce accurate waveforms for combinational + /// DUTs that only have one single `step()` in their protocol). + step_happened_this_cycle: bool, } impl<'a> Scheduler<'a> { @@ -264,6 +271,7 @@ impl<'a> Scheduler<'a> { results: vec![Ok(()); results_size], handler, max_steps, + step_happened_this_cycle: false, } } @@ -376,12 +384,22 @@ impl<'a> Scheduler<'a> { self.next_todo_idx += 1; } - // setup the threads for the next cycle - if !self.next_threads.is_empty() { - // advance simulation for next step + // Advance the simulator whenever a `step()` statement was + // encountered this cycle. + // This must happen even when all threads have completed and + // the `next_threads`` queue is empty, so that the waveform + // records a timestep for every `step()` statement in the protocol. + // (Example: combinational adders which only contain one `step()`. + // Without the following if-statement, the waveform would contain + // 0 timesteps.) + if self.step_happened_this_cycle { info!("Stepping..."); self.evaluator.sim_step(); + self.step_happened_this_cycle = false; + } + // setup the threads for the next cycle + if !self.next_threads.is_empty() { info!( "Moving {} threads from next_threads to active_threads for next cycle", self.next_threads.len() @@ -551,6 +569,7 @@ impl<'a> Scheduler<'a> { if !thread.has_stepped { thread.has_stepped = true; } + self.step_happened_this_cycle = true; info!(" `Step()` reached at {:?}, pausing.", next_id); // Check if this is the final step (no statement after it) From 919b79aa7f31f139f8eb73caae5962fd3636d2d8 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 22 Feb 2026 20:33:09 -0500 Subject: [PATCH 4/6] Update waveform file for combinational adder in monitor/tests --- monitor/tests/adders/add_combinational.fst | Bin 574 -> 575 bytes monitor/tests/adders/add_combinational.prot | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/monitor/tests/adders/add_combinational.fst b/monitor/tests/adders/add_combinational.fst index 83e5421ff6161418267612cb348bf9db030e1193..4ef73338c017587bf09e06124b21c029df297dfb 100644 GIT binary patch literal 575 zcmZQz00Tx(2n{D0Gs8u?x%RUdjb>yBNGvJJ&nqofD6T9nNzGNr%qvMP zDkw??l4xcOPc9qOTLw^Cx#b^2VoFMUiUB*r2NnT_LR%m%oCp`n2R5a9xZq(PcNYM4!6USfn0W&0mf%m dP*C82iY*n1ppbtM4tcv diff --git a/monitor/tests/adders/add_combinational.prot b/monitor/tests/adders/add_combinational.prot index 543bdb20..e43f940a 100644 --- a/monitor/tests/adders/add_combinational.prot +++ b/monitor/tests/adders/add_combinational.prot @@ -1,4 +1,4 @@ -// ARGS: --wave adders/add_combinational.fst --instances adder_d0:Adder +// ARGS: --wave adders/add_combinational.fst --instances add_d0:Adder struct Adder { in a: u32, in b: u32, From 23ad90fe059b472b8b17b740a4fe3462f7234b1c Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 22 Feb 2026 20:36:22 -0500 Subject: [PATCH 5/6] Move monitor adder tests to another branch --- monitor/tests/adders/add_combinational.fst | Bin 575 -> 0 bytes monitor/tests/adders/add_combinational.out | 4 - monitor/tests/adders/add_combinational.prot | 44 ----------- monitor/tests/adders/both_threads_pass.err | 0 monitor/tests/adders/both_threads_pass.fst | Bin 604 -> 0 bytes monitor/tests/adders/both_threads_pass.out | 5 -- monitor/tests/adders/both_threads_pass.prot | 19 ----- monitor/tests/adders/wait_and_add.fst | Bin 626 -> 0 bytes monitor/tests/adders/wait_and_add.prot | 81 -------------------- 9 files changed, 153 deletions(-) delete mode 100644 monitor/tests/adders/add_combinational.fst delete mode 100644 monitor/tests/adders/add_combinational.out delete mode 100644 monitor/tests/adders/add_combinational.prot delete mode 100644 monitor/tests/adders/both_threads_pass.err delete mode 100644 monitor/tests/adders/both_threads_pass.fst delete mode 100644 monitor/tests/adders/both_threads_pass.out delete mode 100644 monitor/tests/adders/both_threads_pass.prot delete mode 100644 monitor/tests/adders/wait_and_add.fst delete mode 100644 monitor/tests/adders/wait_and_add.prot diff --git a/monitor/tests/adders/add_combinational.fst b/monitor/tests/adders/add_combinational.fst deleted file mode 100644 index 4ef73338c017587bf09e06124b21c029df297dfb..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 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 diff --git a/monitor/tests/adders/both_threads_pass.err b/monitor/tests/adders/both_threads_pass.err deleted file mode 100644 index e69de29b..00000000 diff --git a/monitor/tests/adders/both_threads_pass.fst b/monitor/tests/adders/both_threads_pass.fst deleted file mode 100644 index bdd7aea26db401fd6a72beb663844a2df7802a27..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 604 zcmZQz00Tx(2n{EhGQ&l>x%RUJjb>yBNGvJJ&nqofD6T9nNzGNr%qvMP zDkw??l4xcOPc9qOTc%K2yX7B4VoFMUiXl70L;;3G1_cHIh9owI3&}az42(c_F;L_` zGgP$(in a: u32, in b: u32, out s: u32) { - DUT.a := a; - DUT.b := b; - step(); - DUT.a := X; - DUT.b := X; - assert_eq(s, DUT.s); - - fork(); - step(); -} diff --git a/monitor/tests/adders/wait_and_add.fst b/monitor/tests/adders/wait_and_add.fst deleted file mode 100644 index 5ecf8ea2fb70e7fbd1d70a5cc16ab3b85b183035..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 626 zcmZQz00Tx(2n{D$GQ&l>x%RUJjb>yBNGvJJ&nqofD6T9nNzGNr%qvMP zDkw??l4xcOPc9qOTc%K2yX7B4VoFMUiXl70L;;3G1_cHIh9owI3&}az42(c_F;L_` zGgP$#28KWYA`O595CaJq1!93AR0&uqPym8J wY6$`s6R@=`Oh5_}`>Y@)5Lb&cJOeQ~K?F0iIFmS#1_2gEAb>C#U~Yxe0H!A`#{d8T diff --git a/monitor/tests/adders/wait_and_add.prot b/monitor/tests/adders/wait_and_add.prot deleted file mode 100644 index fde08e6a..00000000 --- a/monitor/tests/adders/wait_and_add.prot +++ /dev/null @@ -1,81 +0,0 @@ -// ARGS: --wave adders/wait_and_add.fst --instances add_d1:Adder -struct Adder { - in a: u32, - in b: u32, - out s: u32, -} - -// Adder with 1-cycle delay (i.e. `DUT.s` is only assigned after one cycle)s -prot add(in a: u32, in b: u32, out s: u32) { - DUT.a := a; - DUT.b := b; - step(); - DUT.a := X; - DUT.b := X; - assert_eq(s, DUT.s); - fork(); - step(); -} - -prot add_fork_early(in a: u32, in b: u32, out s: u32) { - DUT.a := a; - DUT.b := b; - step(); - fork(); - DUT.a := X; - DUT.b := X; - assert_eq(s, DUT.s); - step(); -} - -// Like `add` above, but this protocol doesn't end in `step`, -// so this function is ill-formed -prot add_doesnt_end_in_step(in a: u32, in b: u32, out s: u32) { - DUT.a := a; - DUT.b := b; - step(); - DUT.a := X; - DUT.b := X; - assert_eq(s, DUT.s); - fork(); -} - - -prot add_incorrect(in a: u32, in b: u32, out s: u32) { - DUT.a := a; - DUT.b := b; - step(); - DUT.a := a; - DUT.b := b; - assert_eq(s, DUT.s); - fork(); - step(); -} - -prot add_incorrect_implicit(in a: u32, in b: u32, out s: u32) { - DUT.a := a; - DUT.b := b; - step(); - - // missing DontCare assignments to DUT.a and DUT.b - - assert_eq(s, DUT.s); - fork(); - step(); -} - -prot wait_and_add(in a: u32, in b: u32, out s: u32) { - step(); - - fork(); - - step(); - - DUT.a := a; - DUT.b := b; - - step(); - - assert_eq(s, DUT.s); - step(); -} \ No newline at end of file From 4ea396177b9a7fab7852e90e035dc8541fbc2123 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sun, 22 Feb 2026 20:39:01 -0500 Subject: [PATCH 6/6] Comments --- protocols/src/scheduler.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/protocols/src/scheduler.rs b/protocols/src/scheduler.rs index 340c79fb..054f51b2 100644 --- a/protocols/src/scheduler.rs +++ b/protocols/src/scheduler.rs @@ -387,7 +387,7 @@ impl<'a> Scheduler<'a> { // Advance the simulator whenever a `step()` statement was // encountered this cycle. // This must happen even when all threads have completed and - // the `next_threads`` queue is empty, so that the waveform + // the `next_threads` queue is empty, so that the waveform // records a timestep for every `step()` statement in the protocol. // (Example: combinational adders which only contain one `step()`. // Without the following if-statement, the waveform would contain @@ -395,6 +395,8 @@ impl<'a> Scheduler<'a> { if self.step_happened_this_cycle { info!("Stepping..."); self.evaluator.sim_step(); + // Reset flag to ensure that simulator is stepped exactly + // once during each cycle self.step_happened_this_cycle = false; }