diff --git a/.cargo/config.toml b/.cargo/config.toml new file mode 100644 index 00000000..05025a9c --- /dev/null +++ b/.cargo/config.toml @@ -0,0 +1,3 @@ +[alias] +interp = "run --quiet --package protocols-interp --" +monitor = "run --quiet --package protocols-monitor --" diff --git a/.gitignore b/.gitignore index 47672ecb..5cc08d2d 100644 --- a/.gitignore +++ b/.gitignore @@ -4,8 +4,6 @@ Cargo.lock test_run/ *.btor **/.DS_Store -.vscode/* -.surfer/ monitor/target monitor/tests/axi_output.txt *.json @@ -18,6 +16,7 @@ monitor/tests/axi_output.txt # But include the .github directory (CI files) !.github/ !.github/**/* -# And also include .gitignore + .python-version +# And also include .gitignore + .python-version + Cargo config !.gitignore -!.python-version \ No newline at end of file +!.python-version +!.cargo diff --git a/examples/turnt.toml b/examples/turnt.toml index 8c08bf47..68a576a6 100644 --- a/examples/turnt.toml +++ b/examples/turnt.toml @@ -1,2 +1,2 @@ [envs.interp] -command = "cargo run --package protocols-interp -- --color never --transactions {filename} {args}" +command = "cargo interp --color never --transactions {filename} {args}" diff --git a/monitor/src/global_scheduler.rs b/monitor/src/global_scheduler.rs index 7d5a2a6d..8a141a9e 100644 --- a/monitor/src/global_scheduler.rs +++ b/monitor/src/global_scheduler.rs @@ -48,14 +48,16 @@ fn process_group_cycles( match scheduler.process_current_queue(trace, ctx) { Ok(CycleResult::Done) => processed_schedulers.push_back(scheduler), Ok(CycleResult::Fork { parent }) => { - // Iterate over all possible candidate protocols + // When there is an explicit/implicit fork, + // we need to iterate over all possible candidate protocols + // and for each candidate protocol, spawn a scheduler that runs it for (transaction, symbol_table) in &scheduler.possible_transactions { let mut cloned_scheduler = scheduler.clone(); // If there was an explicit fork, we have to add the - // parent thread to the cloned scheduler + // parent thread to the cloned scheduler's `current` queue. if let Some(ref thread) = *parent { - cloned_scheduler.current.push_front(thread.clone()); + cloned_scheduler.current.push_back(thread.clone()); } // Create a new thread for the candidate protocol @@ -75,6 +77,32 @@ fn process_group_cycles( schedulers_to_process.push_back(cloned_scheduler); } } + Ok(CycleResult::RepeatLoopFork { + exited_thread, + speculative_thread, + }) => { + // For forks that arise due to `repeat` loops, + // create 2 schedulers that each execute a different thread: + // - One which executes the `exited_thread`, i.e. the thread + // which exits the loop with the `LoopArg` set to + // `Known(n)` for some `n >= 0` + // - One which executes the `speculative_thread`, i.e. + // the thread which speculatively executes the loop body + // for another iteration, with the `LoopArg` + // set to `Speculative(n + 1)` + + let mut scheduler_with_exited_thread = scheduler.clone(); + scheduler_with_exited_thread + .current + .push_back(*exited_thread); + schedulers_to_process.push_back(scheduler_with_exited_thread); + + let mut scheduler_with_speculative_thread = scheduler.clone(); + scheduler_with_speculative_thread + .current + .push_back(*speculative_thread); + schedulers_to_process.push_back(scheduler_with_speculative_thread); + } Err(SchedulerError::NoTransactionsMatch { struct_name, error_context, diff --git a/monitor/src/interpreter.rs b/monitor/src/interpreter.rs index 9c565251..bf95722a 100644 --- a/monitor/src/interpreter.rs +++ b/monitor/src/interpreter.rs @@ -15,17 +15,25 @@ use crate::{ global_context::GlobalContext, signal_trace::{PortKey, SignalTrace, WaveSignalTrace}, thread::Thread, - types::ProtocolApplication, + types::{LoopArgState, ProtocolApplication}, }; +#[allow(dead_code)] #[derive(Clone)] pub struct Interpreter { pub transaction: Transaction, pub symbol_table: SymbolTable, pub next_stmt_map: NextStmtMap, + + /// Maps protocol arguments (input/output parameters) to their values pub args_mapping: FxHashMap, + + /// Tracks which bits of a `SymbolId` are known pub known_bits: FxHashMap, + /// Tracks the state of arguments for `repeat` loops + pub loop_args: FxHashMap, + /// Constraints on DUT input port values that must hold after stepping. /// These are established by assignments like `D.m_axis_tvalid := 1'b1` /// and verified after each `step()` to ensure the constraint still holds. @@ -43,41 +51,47 @@ pub struct Interpreter { } impl Interpreter { - /// Builds a `ProtocolApplication` from the current interpreter state. + /// Attempts to builds a `ProtocolApplication` from the current interpreter state. /// `struct_name` is left as `None` — the caller (Scheduler) is responsible /// for setting it, since the Interpreter doesn't know the struct name. + /// If this return function returns `None` (e.g. because an argument + /// wasn't present in `args_mapping`), the caller + /// (`Scheduler::run_thread_till_next_step`) treats the corresponding thread + /// as having failed. pub fn to_protocol_application( &self, struct_name: Option, ctx: &GlobalContext, trace: &WaveSignalTrace, - ) -> ProtocolApplication { + ) -> Option { let mut serialized_args = vec![]; for arg in &self.transaction.args { let symbol_id = arg.symbol(); - let name = self.symbol_table[symbol_id].full_name(&self.symbol_table); - let value = self.args_mapping.get(&symbol_id).unwrap_or_else(|| { + if let Some(value) = self.args_mapping.get(&symbol_id) { + serialized_args.push(serialize_bitvec(value, ctx.display_hex)); + } else { + let name = self.symbol_table[symbol_id].full_name(&self.symbol_table); let time_str = if ctx.show_waveform_time { trace.format_time(trace.time_step(), ctx.time_unit) } else { format!("cycle {}", self.trace_cycle_count) }; - panic!( + info!( "Transaction `{}`, {}: Unable to find value for {} ({}) in args_mapping, which is {{ {} }}", self.transaction.name, time_str, name, symbol_id, serialize_args_mapping(&self.args_mapping, &self.symbol_table, ctx.display_hex) - ) - }); - serialized_args.push(serialize_bitvec(value, ctx.display_hex)); + ); + return None; + } } - ProtocolApplication { + Some(ProtocolApplication { struct_name, protocol_name: self.transaction.name.clone(), serialized_args, - } + }) } /// Performs a context switch in the `Interpreter` by setting its @@ -91,6 +105,7 @@ impl Interpreter { self.known_bits = thread.known_bits.clone(); self.constraints = thread.constraints.clone(); self.args_to_pins = thread.args_to_pins.clone(); + self.loop_args = thread.loop_args_state.clone(); } /// Pretty-prints a `Statement` identified by its `StmtId` @@ -157,6 +172,7 @@ impl Interpreter { trace_cycle_count, args_to_pins: FxHashMap::default(), dut_symbol_id, + loop_args: FxHashMap::default(), } } @@ -475,8 +491,10 @@ impl Interpreter { Stmt::While(loop_guard_id, do_block_id) => { self.evaluate_while(loop_guard_id, stmt_id, do_block_id, ctx, trace) } - Stmt::BoundedLoop(_, _) => { - todo!("Bounded loops is not yet implemented in the monitor") + Stmt::RepeatLoop(_, _) => { + // Repeat loops are intercepted in `run_thread_till_next_step` + // in `scheduler.rs`, so this case is unreachable + unreachable!("Repeat loops handled in `scheduler.rs` already") } Stmt::Step | Stmt::Fork => { // The scheduler handles `step`s and `fork`s. diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index 707d3ceb..72822263 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -1,9 +1,9 @@ use anyhow::{Context, anyhow}; -use baa::BitVecOps; +use baa::{BitVecOps, BitVecValue}; use log::info; use protocols::{ errors::{EvaluationError, ExecutionError}, - ir::{Stmt, SymbolId, SymbolTable, Transaction}, + ir::{Expr, Stmt, StmtId, SymbolId, SymbolTable, Transaction}, serialize::serialize_bitvec, }; use rustc_hash::FxHashSet; @@ -15,7 +15,8 @@ use crate::{ signal_trace::{SignalTrace, WaveSignalTrace}, thread::Thread, types::{ - AugmentedProtocolApplication, AugmentedTrace, CycleResult, SchedulerError, ThreadResult, + AugmentedProtocolApplication, AugmentedTrace, CycleResult, LoopArgState, SchedulerError, + ThreadResult, }, }; @@ -143,7 +144,7 @@ impl Scheduler { current_threads.push_back(thread); thread_id += 1; } - // Technically, initializing the `interpreter` here is necessary + // Technically, initializing the `interpreter` here is unnecessary // since when we pop a thread from the `current` queue, we perform // a context switch and run the `interpreter` on the transaction/symbol_table // corresponding to the thread. However, we do this here nonetheless @@ -197,8 +198,8 @@ impl Scheduler { /// (marking all suspended threads as ready for execution), /// then advances the trace to the next step. /// Notes: - /// - This function is used by `GlobalScheduler` to coordinate - /// execution between multiple schedulers. + /// - This function is used by `GlobalScheduler::process_group_cycles` + /// to coordinate execution between multiple schedulers. /// - When a `fork` creates a `Scheduler` clone, call this function /// on the clone pub fn process_current_queue( @@ -211,7 +212,10 @@ impl Scheduler { self.struct_name ); - // Process each thread (this function returns early when a thread `fork`s) + // Process each thread. Note that + // this function returns early when a thread `fork`s, with the + // new forked-off threads propagated to the caller + // (`GlobalScheduler::process_group_cycles`) while let Some(thread) = self.current.pop_front() { match self.run_thread_till_next_step(thread, trace, ctx)? { ThreadResult::Completed => continue, @@ -225,6 +229,15 @@ impl Scheduler { parent: Box::new(None), }); } + ThreadResult::RepeatLoopFork { + exited_thread, + speculative_thread, + } => { + return Ok(CycleResult::RepeatLoopFork { + exited_thread, + speculative_thread, + }); + } } } @@ -650,6 +663,81 @@ impl Scheduler { Err(error_msg) } + /// Helper function which handles `repeat` loops by forking two threads: + /// - One which exits the loop with the `LoopArg` set to `Known(n)` + /// - One which speculatively executes the loop body for another iteration, + /// with the `LoopArg` set to `Speculative(n + 1)` + /// + /// The arguments to this function are: + /// - The `SymbolId` / `StmtId`s of the `LoopArg`, loop body and the + /// entire loop statement itself + /// - The `current_thread` (which will speculatively execute the loop body + /// for another iteration) + /// - The value `n` that has been currently "guessed" for the `LoopArg` + /// + /// This function returns a `ThreadResult::RepeatLoopFork` containing the + /// two threads. + fn handle_repeat_loops( + &mut self, + loop_arg_symbol_id: SymbolId, + loop_body_id: StmtId, + loop_stmt_id: StmtId, + mut current_thread: Thread, + n: u64, + ) -> ThreadResult { + // Create a new thread `exited_thread` that is identical + // to the current thread, but it exits the loop + // with the `LoopArg` set to `Known(n)` + let mut exited_thread = current_thread.clone(); + exited_thread.thread_id = self.num_threads; + self.num_threads += 1; + exited_thread + .loop_args_state + .insert(loop_arg_symbol_id, LoopArgState::Known(n)); + + // Also add the `loop_arg` to the `exited_thread`'s + // `args_mapping` and `known_bits` map. + // (The `loop_arg` is an input + // parameter, so other statements in the protocol + // can still refer to it) + let loop_arg_bitwidth = current_thread.symbol_table[loop_arg_symbol_id] + .tpe() + .bitwidth(); + exited_thread.args_mapping.insert( + loop_arg_symbol_id, + BitVecValue::from_u64(n, loop_arg_bitwidth), + ); + exited_thread + .known_bits + .insert(loop_arg_symbol_id, BitVecValue::ones(loop_arg_bitwidth)); + + // The exited_thread needs to execute the first statement + // that immediately follow the loop + exited_thread.current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + "Repeat loops can't be the last statement in a protocol since protocols always end with `step`" + ); + + // Update the current thread's `loop_args` map so that + // the `LoopArg` is now `Speculative(n + 1)` + current_thread.loop_args_state.insert( + loop_arg_symbol_id, + LoopArgState::Speculative(n + 1, loop_stmt_id), + ); + + // The current thread executes the + // loop body for another iteration speculatively + current_thread.current_stmt_id = loop_body_id; + + // Let the global scheduler deal with both threads + // (The current thread is called the `speculative_thread`, + // since it speculatively executes the loop body again + // with the `LoopArg` set to `Speculative(n + 1)`) + ThreadResult::RepeatLoopFork { + exited_thread: Box::new(exited_thread), + speculative_thread: Box::new(current_thread), + } + } + /// Keeps running a `thread` until: /// - It reaches the next `step()` or `fork()` statement /// - It completes succesfully @@ -673,6 +761,100 @@ impl Scheduler { let mut current_stmt_id = thread.current_stmt_id; loop { + // Intercept repeat loops before evaluating statements + if let Stmt::RepeatLoop(loop_arg_expr_id, loop_body_id) = + thread.transaction[current_stmt_id] + { + let loop_stmt_id = current_stmt_id; + let loop_arg_symbol_id = match thread.transaction[loop_arg_expr_id] { + Expr::Sym(symbol_id) => symbol_id, + Expr::Const(_) => { + todo!("Maybe allow constants to appear as arguments to repeat loops??") + } + _ => { + unreachable!("Arguments to repeat loops are always SymbolIDs") + } + }; + + // Suppose we already know how many iterations a `repeat` loop + // must take. If so, we execute it deterministically. + // This situation occurs if there are multiple `repeat` loops + // in a protocol that use the same `LoopArg`, e.g. + // `repeat n iterations { ... }; ...; repeat n iterations { ... }` + if let Some(num_remaining_iters) = + thread.repeat_loops_remaining_iters.get_mut(&loop_stmt_id) + { + *num_remaining_iters -= 1; + if *num_remaining_iters == 0 { + thread.repeat_loops_remaining_iters.remove(&loop_stmt_id); + current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" + ); + } else { + current_stmt_id = loop_body_id; + } + continue; + } + + // Now we need to handle the case when the value of a `LoopArg` + // is unknown + match thread.loop_args_state.get(&loop_arg_symbol_id).cloned() { + None => { + // First time seeing loop arg, it is `Unknown` + // (i.e. absent from the thread's `loop_args_state` map), + // so pass in `n = 0` to the `handle_repeat_loops` + // helper function + return Ok(self.handle_repeat_loops( + loop_arg_symbol_id, + loop_body_id, + loop_stmt_id, + thread, + 0, + )); + } + Some(LoopArgState::Speculative(n, stored_loop_stmt_id)) => { + // We disallow nested `repeat` loops that use the + // same loop argument, i.e. we forbid + // `repeat n iterations { repeat n iterations { ... } ... }` + if loop_stmt_id != stored_loop_stmt_id { + panic!( + "Nested `repeat` loops that use the same loop argument `{}` are forbidden", + thread.symbol_table[loop_arg_symbol_id].name() + ) + } + + // Fork two threads: + // one with `Known(n)`, one with `Speculative(n + 1)` + return Ok(self.handle_repeat_loops( + loop_arg_symbol_id, + loop_body_id, + loop_stmt_id, + thread, + n, + )); + } + Some(LoopArgState::Known(n)) => { + // Value of `n` has been resolved from a prior loop + // (either with the same `StmtId` or a different `StmtId`) + if n == 0 { + // Exit the loop since the `LoopArg` is already known, + // proceed to the next immediate statement + // (evaluated in the next iteration + // of the outer `loop` in this function) + current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" + ); + } else { + // Insert it into the thread's `repeat_loops_remaining_iters` + // map, which tracks how many iterations need to be executed + // for this loop + thread.repeat_loops_remaining_iters.insert(loop_stmt_id, n); + current_stmt_id = loop_body_id; + } + continue; + } + } + } match self.interpreter.evaluate_stmt(¤t_stmt_id, ctx, trace) { Ok(Some(next_stmt_id)) => { // Update thread-local maps @@ -791,10 +973,22 @@ impl Scheduler { None }; let is_idle = self.interpreter.transaction.is_idle; - let protocol_application = + + let prot_app_opt = self.interpreter .to_protocol_application(struct_name, ctx, trace); + if prot_app_opt.is_none() { + info!( + "Unable to construct protocol application for thread {} (`{}`), marking thread as failed", + thread.global_thread_id(ctx), + self.format_transaction_name(ctx, thread.transaction.name.clone()) + ); + self.failed.push_back(thread.clone()); + self.print_scheduler_state(trace, ctx); + return Ok(ThreadResult::Completed); + } + if is_idle { info!( "Transaction `{}` is marked as idle", @@ -806,7 +1000,8 @@ impl Scheduler { // output buffer self.output_buffer.push(AugmentedProtocolApplication { end_cycle_count: self.cycle_count, - protocol_application, + protocol_application: prot_app_opt + .expect("Expected Some(ProtocolApplication)"), start_time_step: thread.start_time_step, end_time_step, thread_id: thread.global_thread_id(ctx), diff --git a/monitor/src/thread.rs b/monitor/src/thread.rs index 59ddef8e..315b67ba 100644 --- a/monitor/src/thread.rs +++ b/monitor/src/thread.rs @@ -10,7 +10,7 @@ use protocols::{ }; use rustc_hash::FxHashMap; -use crate::global_context::GlobalContext; +use crate::{global_context::GlobalContext, types::LoopArgState}; /// The local context associated with an individual thread, /// storing information such as: @@ -62,6 +62,19 @@ pub struct Thread { /// Maps function parameters to DUT ports pub args_to_pins: FxHashMap, + /// Maps arguments of `repeat` loops to their current "guessed" state + /// (either `Speculative` or `Known` -- see docs for the `LoopArgState` type) + pub loop_args_state: FxHashMap, + + /// Once the state of a `LoopArg` has been determined, we need to track + /// how many iterations remain to be executed -- this is most useful + /// if we have two loops that use the same `LoopArg`, e.g. + /// `repeat n iterations { ... }; ...; repeat n iterations { ...}`. + /// This map is populated lazily when we encounter each `repeat` loop + /// (see `Scheduler::run_thread_till_next_step`). + /// The `StmtId` key is the statement of the `repeat` loop. + pub repeat_loops_remaining_iters: FxHashMap, + /// Determines if the thread has called `fork()` yet. Initialized to `false`. /// Since well-formedness dicates that a protocol can only contain /// at most one `fork()`, once this flag is set to `true`, @@ -117,6 +130,8 @@ impl Thread { start_time_step, args_to_pins: FxHashMap::default(), has_forked: false, + loop_args_state: FxHashMap::default(), + repeat_loops_remaining_iters: FxHashMap::default(), } } diff --git a/monitor/src/types.rs b/monitor/src/types.rs index 11b6ad5d..24ab2284 100644 --- a/monitor/src/types.rs +++ b/monitor/src/types.rs @@ -7,6 +7,8 @@ use std::{collections::VecDeque, fmt}; +use protocols::ir::StmtId; + use crate::{scheduler::Scheduler, thread::Thread}; /// Represents a protocol application like `add(1, 2, 3)` which appears @@ -95,8 +97,11 @@ impl From for SchedulerError { } } -/// The result of an individual `Thread`: either it `Completed`, -/// forked explcitly or forked implicitly. +/// The result of an individual `Thread` is one of four options: +/// - it `Completed` (was moved to one of the `next/finished/failed` queues) +/// - it forked explicitly (by calling `fork()`) (`ExplicitFork`) +/// - it forked implicitly at the end of a protocol (`ImplicitFork`) +/// - it forked after encountering a `repeat` loop (`RepeatLoopFork`) #[derive(Debug)] pub enum ThreadResult { /// Thread completed (moved to next/finished/failed queue) @@ -110,11 +115,22 @@ pub enum ThreadResult { /// constructors of this enum. ExplicitFork { parent: Box }, - /// Thread is laready in the `finished queue and forked implicitly + /// Thread is already in the `finished` queue and forked implicitly /// (e.g. this thread is a protocol which ends with `step` without /// ever calling `fork`). The caller of a function which returns /// this constructor is responsible for spawning new protocol ImplicitFork, + + /// A fork that arises when learning the value of arguments to `repeat` loops + RepeatLoopFork { + /// The thread that exited the loop with the loop argument + /// set to `Known(n)` for some `n >= 0` + exited_thread: Box, + + /// The thread that remains in the loop and executed the loop body again, + /// with the loop argument set to `Speculative(n + 1)` + speculative_thread: Box, + }, } /// The result of the *Scheduler* at the end of a cycle @@ -129,4 +145,33 @@ pub enum CycleResult { /// constructors of this enum. parent: Box>, }, + /// A fork that arises when learning the value of arguments to `repeat` loops + RepeatLoopFork { + /// The thread that exited the loop with the loop argument + /// set to `Known(n)` for some `n >= 0` + exited_thread: Box, + + /// The thread that remains in the loop and executed the loop body again, + /// with the loop argument set to `Speculative(n + 1)` + speculative_thread: Box, + }, +} + +/// The possible states for an argument to a `repeat` loop. +/// We maintain the following invariants: +/// - `Speculative(n, loopID) `only becomes `Known(n)` after the corresponding +/// scheduler has executed the body of the loop at `loopID` exactly `n` +/// times (note that `n` can be 0). +/// - Once a `LoopArg` becomes Known, we proceed to the next statement +/// that immediately follows the loop (we don't enter the loop body). +/// - Moreover, once a `LoopArg` remains `Known`, it remains `Known` thereafter. +#[allow(dead_code)] +#[derive(Debug, Clone)] +pub enum LoopArgState { + /// `Speculative(n, loopID)` means the associated thread has already + /// *speculatively* executed the loop at `loopID` for `n` iterations. + /// (The `StmtId` is there to disambiguate between different loop statements, + /// since different loops can use the same loop argument `n`.) + Speculative(u64, StmtId), + Known(u64), } diff --git a/monitor/tests/adders/busy_wait.err b/monitor/tests/adders/busy_wait.err new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/busy_wait.fst b/monitor/tests/adders/busy_wait.fst new file mode 100644 index 00000000..4349baaf Binary files /dev/null and b/monitor/tests/adders/busy_wait.fst differ diff --git a/monitor/tests/adders/busy_wait.out b/monitor/tests/adders/busy_wait.out new file mode 100644 index 00000000..95a94f09 --- /dev/null +++ b/monitor/tests/adders/busy_wait.out @@ -0,0 +1,5 @@ +// trace 0 +trace { + add_busy_wait(1, 2, 1, 3); + add_busy_wait(4, 5, 3, 9); +} diff --git a/monitor/tests/adders/busy_wait.prof b/monitor/tests/adders/busy_wait.prof new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/busy_wait.prot b/monitor/tests/adders/busy_wait.prot new file mode 100644 index 00000000..289df726 --- /dev/null +++ b/monitor/tests/adders/busy_wait.prot @@ -0,0 +1,29 @@ +// ARGS: --wave adders/busy_wait.fst --instances add_d1:Adder +struct Adder { + in a: u32, + in b: u32, + out s: u32, +} + +// Uses a bounded loop that busy-waits for `num_iters` cycles. +// Since concrete assignments to DUT input ports persist, +// calling `step()` multiple times in the loop with the same inputs +// should still produce the correct result on the adder. (This allows us to +// reuse the same Verilog file as the other `adder_d1` tests.) +prot add_busy_wait(in a: u32, in b: u32, in num_iters: u64, out s: u32) { + DUT.a := a; + DUT.b := b; + // We want `assert_eq(s, DUT.s)` to hold for every iteration of this loop, + // so we cannot put `DUT.a := X; DUT.b := X` in the loop body, since + // that would cause the `assert_eq` to fail on later iterations of the loop + repeat num_iters iterations { + step(); + assert_eq(s, DUT.s); + } + DUT.a := X; + DUT.b := X; + // Ensure `s = a + b` still holds when we exit the loop + assert_eq(s, DUT.s); + fork(); + step(); +} diff --git a/monitor/tests/adders/loop_with_assigns.fst b/monitor/tests/adders/loop_with_assigns.fst new file mode 100644 index 00000000..b3babd9d Binary files /dev/null and b/monitor/tests/adders/loop_with_assigns.fst differ diff --git a/monitor/tests/adders/loop_with_assigns.out b/monitor/tests/adders/loop_with_assigns.out new file mode 100644 index 00000000..21c26b8a --- /dev/null +++ b/monitor/tests/adders/loop_with_assigns.out @@ -0,0 +1,5 @@ +// trace 0 +trace { + loop_add(1, 2, 3, 3); + loop_add(10, 20, 1, 30); +} \ No newline at end of file diff --git a/monitor/tests/adders/loop_with_assigns.prof b/monitor/tests/adders/loop_with_assigns.prof new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/loop_with_assigns.prot b/monitor/tests/adders/loop_with_assigns.prot new file mode 100644 index 00000000..c933237f --- /dev/null +++ b/monitor/tests/adders/loop_with_assigns.prot @@ -0,0 +1,23 @@ +// ARGS: --wave adders/loop_with_assigns.fst --instances add_d1:Adder +struct Adder { + in a: u32, + in b: u32, + out s: u32, +} + +// Each iteration of the loop performs the full add protocol: +// assign inputs -> step -> release inputs -> assert output +// This tests that assignments, DontCare releases, and assertions +// all work correctly inside a bounded loop body. +prot loop_add(in a: u32, in b: u32, in num_iters: u64, out s: u32) { + repeat num_iters iterations { + 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/nested_busy_wait.fst b/monitor/tests/adders/nested_busy_wait.fst new file mode 100644 index 00000000..4c711db4 Binary files /dev/null and b/monitor/tests/adders/nested_busy_wait.fst differ diff --git a/monitor/tests/adders/nested_busy_wait.out b/monitor/tests/adders/nested_busy_wait.out new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/nested_busy_wait.prof b/monitor/tests/adders/nested_busy_wait.prof new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/nested_busy_wait.prot b/monitor/tests/adders/nested_busy_wait.prot new file mode 100644 index 00000000..2c0e4a15 --- /dev/null +++ b/monitor/tests/adders/nested_busy_wait.prot @@ -0,0 +1,29 @@ +// ARGS: --wave adders/nested_busy_wait.fst --instances add_d1:Adder +struct Adder { + in a: u32, + in b: u32, + out s: u32, +} + +// Nested bounded loops: the outer loop runs `outer_iters` times, +// and the inner loop runs `inner_iters` times per outer iteration, +// for a total of `outer_iters * inner_iters` steps. +// Since inputs are sticky on the adder, the final result is +// the same regardless of how many steps we take. +prot nested_busy_wait(in a: u32, in b: u32, in outer_iters: u64, in inner_iters: u64, out s: u32) { + DUT.a := a; + DUT.b := b; + repeat outer_iters iterations { + repeat inner_iters iterations { + step(); + assert_eq(s, DUT.s); + } + step(); + assert_eq(s, DUT.s); + } + DUT.a := X; + DUT.b := X; + assert_eq(s, DUT.s); + fork(); + step(); +} diff --git a/monitor/tests/turnt.toml b/monitor/tests/turnt.toml index 6b85ef21..ebe5dde3 100644 --- a/monitor/tests/turnt.toml +++ b/monitor/tests/turnt.toml @@ -1,7 +1,7 @@ # We run Cargo in quiet mode to prevent build messages from # appearing in the output for Turnt tests [envs.monitor] -command = "cargo run --quiet --package protocols-monitor -- -p {filename} {args}" +command = "cargo monitor -p {filename} {args}" output.out = "-" output.err = "2" diff --git a/protocols/src/interpreter.rs b/protocols/src/interpreter.rs index 8203db7f..abd5eb33 100644 --- a/protocols/src/interpreter.rs +++ b/protocols/src/interpreter.rs @@ -744,7 +744,7 @@ impl<'a> Evaluator<'a> { Stmt::While(loop_guard_id, do_block_id) => { self.evaluate_while(loop_guard_id, stmt_id, do_block_id) } - Stmt::BoundedLoop(num_iters_id, loop_body_id) => { + Stmt::RepeatLoop(num_iters_id, loop_body_id) => { self.evaluate_bounded_loop(num_iters_id, stmt_id, loop_body_id) } Stmt::Step => { diff --git a/protocols/src/ir.rs b/protocols/src/ir.rs index 2cf720a3..f6f7527e 100644 --- a/protocols/src/ir.rs +++ b/protocols/src/ir.rs @@ -148,7 +148,7 @@ impl Transaction { } // Add a back-edge from the loop body to the current `stmt_id` // (same as how while-loops are represented in the current AST) - Stmt::BoundedLoop(_, body_id) => { + Stmt::RepeatLoop(_, body_id) => { map.extend(self.next_stmt_mapping_helper(*body_id, Some(stmt_id))); } _ => {} @@ -325,8 +325,9 @@ pub enum Stmt { Step, Fork, While(ExprId, StmtId), - // Bounded loop with fixed no. of iterations - BoundedLoop(ExprId, StmtId), + /// Bounded loop with fixed no. of iterations + /// (`ExprId` is the no. of iterations, `StmtId` is the loop body) + RepeatLoop(ExprId, StmtId), IfElse(ExprId, StmtId, StmtId), AssertEq(ExprId, ExprId), } diff --git a/protocols/src/parser.rs b/protocols/src/parser.rs index c12398fb..43289f7e 100644 --- a/protocols/src/parser.rs +++ b/protocols/src/parser.rs @@ -443,7 +443,7 @@ impl ParserContext<'_> { )?; let num_iterations = self.parse_expr(expr_rule.into_inner())?; let body = self.parse_stmt_block(inner_rules)?; - Ok(Stmt::BoundedLoop(num_iterations, body)) + Ok(Stmt::RepeatLoop(num_iterations, body)) } fn parse_assert_eq(&mut self, pair: pest::iterators::Pair) -> Result { diff --git a/protocols/src/serialize.rs b/protocols/src/serialize.rs index 4dfc470b..c5c30842 100644 --- a/protocols/src/serialize.rs +++ b/protocols/src/serialize.rs @@ -176,7 +176,7 @@ pub fn serialize_stmt(tr: &Transaction, st: &SymbolTable, stmt_id: &StmtId) -> S serialize_stmt(tr, st, stmt_id) ) } - Stmt::BoundedLoop(expr_id, stmt_id) => { + Stmt::RepeatLoop(expr_id, stmt_id) => { format!( "repeat {} iterations {{ {} }}", serialize_expr(tr, st, expr_id), @@ -236,7 +236,7 @@ pub fn build_statements( build_statements(out, tr, st, bodyid, index + 1)?; writeln!(out, "{}}}", " ".repeat(index))?; } - Stmt::BoundedLoop(count, bodyid) => { + Stmt::RepeatLoop(count, bodyid) => { writeln!( out, "{}repeat {} iterations {{", diff --git a/protocols/src/typecheck.rs b/protocols/src/typecheck.rs index 67d08adf..aec8da1c 100644 --- a/protocols/src/typecheck.rs +++ b/protocols/src/typecheck.rs @@ -203,7 +203,7 @@ fn check_stmt_types( Err(anyhow!(error_msg)) } } - Stmt::BoundedLoop(count_expr, bodyid) => { + Stmt::RepeatLoop(count_expr, bodyid) => { // Typecheck the no. of iterations (which must be a BitVec type of any width) let num_iterations_type = check_expr_types(tr, st, handler, count_expr)?; if let Type::BitVec(_) = num_iterations_type { diff --git a/protocols/tests/turnt.toml b/protocols/tests/turnt.toml index 8c08bf47..68a576a6 100644 --- a/protocols/tests/turnt.toml +++ b/protocols/tests/turnt.toml @@ -1,2 +1,2 @@ [envs.interp] -command = "cargo run --package protocols-interp -- --color never --transactions {filename} {args}" +command = "cargo interp --color never --transactions {filename} {args}" diff --git a/turnt.toml b/turnt.toml index 70a5c157..895f5f9c 100644 --- a/turnt.toml +++ b/turnt.toml @@ -1 +1 @@ -command = "cargo run --package protocols-interp -- --color never --transactions {filename} {args}" +command = "cargo interp --color never --transactions {filename} {args}"