From a81fcb9cf99993554ced284f38626068ef183a18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 30 Apr 2026 14:32:34 -0400 Subject: [PATCH 1/3] wishbone: add stb non-determinism allowed by spec --- examples/wishbone/wishbone.prot | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/examples/wishbone/wishbone.prot b/examples/wishbone/wishbone.prot index 66808969..25d317c2 100644 --- a/examples/wishbone/wishbone.prot +++ b/examples/wishbone/wishbone.prot @@ -130,13 +130,12 @@ prot read(mask: u4, addr: u32, data: u32) { prot write_burst_const(mask: u4, addr: u32, data: [u32]+) { // no RST self.RST := 1'b0; + // constant burst cycle (in which case bte is don't care) self.CTI := 3'b001; self.BTE := X; - // in our simple version, we always drive cyc and stb together self.CYC := 1'b1; - self.STB := 1'b1; // we are writing self.WE := 1'b1; @@ -146,6 +145,8 @@ prot write_burst_const(mask: u4, addr: u32, data: [u32]+) { self.SEL := mask; for d in data { + // set STB for at least one cycle + self.STB := 1'b1; self.DAT_O := d; // indicate end of cycle for last item @@ -156,6 +157,12 @@ prot write_burst_const(mask: u4, addr: u32, data: [u32]+) { // wait for ack while self.ACK == 1'b0 { step(); + // after the first cycle, STB does not have to remain at one + // OBSERVATION 4.00: + // "[The server] can use the [CTI_I()] signals to determine the response for the next cycle. + // But it cannot determine the state of [STB_I] for the next cycle, + // therefore it must generate the response independent of [STB_I]." + self.STB := X; } // acknowledge is now true for one cycle From f45cbdf92bcb37891555549837beae103b5c335b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 30 Apr 2026 14:36:29 -0400 Subject: [PATCH 2/3] errors: remove duplicated code for error message --- protocols/src/errors.rs | 27 ++------------------------- 1 file changed, 2 insertions(+), 25 deletions(-) diff --git a/protocols/src/errors.rs b/protocols/src/errors.rs index 0d0af07b..5699d628 100644 --- a/protocols/src/errors.rs +++ b/protocols/src/errors.rs @@ -736,34 +736,11 @@ impl DiagnosticEmitter { ); } EvaluationError::ForbiddenPortRead { - port_name, unassigned_inputs, expr_id, + .. } => { - let input_names: Vec<_> = unassigned_inputs - .iter() - .map(|(name, _)| format!("'{}'", name)) - .collect(); - // Inputs with no stmt_id were never explicitly assigned (implicit DontCare at initialization) - let implicit_names: Vec<_> = unassigned_inputs - .iter() - .filter(|(_, stmt_id)| stmt_id.is_none()) - .map(|(name, _)| format!("'{}'", name)) - .collect(); - let implicit_note = if implicit_names.is_empty() { - String::new() - } else { - format!( - " ({} initialized to DontCare and were never assigned a concrete value)", - implicit_names.join(", ") - ) - }; - let main_message = format!( - "Output '{}' depends on input(s) {} which do not have assigned values{}", - port_name, - input_names.join(", "), - implicit_note - ); + let main_message = format!("{error}"); let stmt_labels: Vec<_> = unassigned_inputs .iter() .filter_map(|(name, stmt_id)| { From cabac217e6ce98c37ddebe815bd7ddd2fa2db1a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 30 Apr 2026 16:13:59 -0400 Subject: [PATCH 3/3] interp: add option to simplify RTL before simulation and analysis --- interp/src/main.rs | 6 ++++++ protocols/src/setup.rs | 7 ++++++- 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/interp/src/main.rs b/interp/src/main.rs index 4067827b..57f7a12d 100644 --- a/interp/src/main.rs +++ b/interp/src/main.rs @@ -61,6 +61,11 @@ struct Cli { /// Skips the static checks for step/fork errors. #[arg(long)] skip_static_step_fork_checks: bool, + + /// Optimize the underlying transition system before simulation. + /// This might change the combinational dependencies. + #[arg(long)] + simplify_rtl: bool, } /// Examples (enables all tracing logs): @@ -123,6 +128,7 @@ fn main() -> anyhow::Result<()> { cli.module, protocols_handler, cli.skip_static_step_fork_checks, + cli.simplify_rtl, )?; // Nikil says we have to do this step in order to convert diff --git a/protocols/src/setup.rs b/protocols/src/setup.rs index 766d9faf..1ae56886 100644 --- a/protocols/src/setup.rs +++ b/protocols/src/setup.rs @@ -63,8 +63,13 @@ pub fn setup_test_environment( top_module: Option, handler: &mut DiagnosticHandler, skip_static_step_fork_checks: bool, + simplify_rtl: bool, ) -> anyhow::Result { - let (ctx, sys) = create_sim_context(verilog_paths, top_module); + let (mut ctx, mut sys) = create_sim_context(verilog_paths, top_module); + if simplify_rtl { + patronus::system::transform::replace_anonymous_inputs_with_zero(&mut ctx, &mut sys); + patronus::system::transform::simplify_expressions(&mut ctx, &mut sys); + } let parsed = frontend(transaction_filename, handler, skip_static_step_fork_checks)?; Ok((parsed, ctx, sys)) }