From 54c704d78ab49ff23cc00da809832c66f08f2687 Mon Sep 17 00:00:00 2001 From: Nikil Shyamsunder Date: Fri, 31 Jul 2026 15:18:18 -0400 Subject: [PATCH 1/7] implement steady state automata for special case of protocols without forks --- graph-interp/src/main.rs | 42 ++++++++++ protocols/src/ir/bounded_lowering.rs | 4 +- protocols/src/ir/mod.rs | 1 + protocols/src/ir/steady_state_lowering.rs | 93 +++++++++++++++++++++++ 4 files changed, 138 insertions(+), 2 deletions(-) create mode 100644 protocols/src/ir/steady_state_lowering.rs diff --git a/graph-interp/src/main.rs b/graph-interp/src/main.rs index 9ab03366..0ef4f926 100644 --- a/graph-interp/src/main.rs +++ b/graph-interp/src/main.rs @@ -20,6 +20,7 @@ use protocols::ir::lowering::lower_ast_to_ir; use protocols::ir::propagate_assigns::propagate_assignments; use protocols::ir::proto_graph::ProtoGraph; use protocols::ir::reaching_defs::{format_reaching_defs, reaching_definitions}; +use protocols::ir::steady_state_lowering::lower_steady_state; use protocols::ir::trace_lowering::lower_trace_to_ir; use protocols::{PatronusSim, PortId, Value, frontend, transaction_frontend}; use rustc_hash::FxHashMap; @@ -84,6 +85,9 @@ struct Cli { #[arg(long, default_value_t)] bound: usize, + + #[arg(long)] + steady_state: bool, } fn load_protocols(cli: &Cli) -> (SymbolTable, Vec) { @@ -503,6 +507,41 @@ fn run_bmc(cli: &Cli, st: &SymbolTable, module: &Module, traces: &[Vec<(String, } } +fn run_steady_state( + cli: &Cli, + st: &SymbolTable, + module: &Module, + traces: &[Vec<(String, Vec)>], +) { + let protos_by_name: FxHashMap = + module.protos.iter().map(|p| (p.name.clone(), p)).collect(); + + for (trace_index, trace) in traces.iter().enumerate() { + print_trace_separator(trace_index); + let mut used_protocol_names = Vec::new(); + for (name, _) in trace { + if !used_protocol_names.contains(&name.as_str()) { + used_protocol_names.push(name.as_str()); + } + } + let used_protocols: Vec = used_protocol_names + .iter() + .map(|name| (*protos_by_name.get(*name).unwrap()).clone()) + .collect(); + + let sim = PatronusSim::new(&cli.verilog, cli.module.as_deref(), module, None).unwrap(); + // The graph and DUT transition system must share an expression + // context, including port expressions such as DUT.o_ack. + let (mut pg, _proto_choice) = lower_steady_state(used_protocols, st, sim.ctx.clone()); + pg.garbage_collect_unreachable(); + pg = determinized(pg, st); + + if cli.graphout { + println!("{}", to_dot_string(&pg, st)); + } + } +} + fn main() { let cli = Cli::parse(); let (st, modules) = load_protocols(&cli); @@ -512,6 +551,9 @@ fn main() { // let old_hook = std::panic::take_hook(); // std::panic::set_hook(Box::new(|_| {})); let _result = catch_unwind(AssertUnwindSafe(|| { + if cli.steady_state { + run_steady_state(&cli, &st, &module, &traces); + } if cli.bound > 0 { run_bmc(&cli, &st, &module, &traces); } else if cli.transition_system { diff --git a/protocols/src/ir/bounded_lowering.rs b/protocols/src/ir/bounded_lowering.rs index 7a538a41..20905922 100644 --- a/protocols/src/ir/bounded_lowering.rs +++ b/protocols/src/ir/bounded_lowering.rs @@ -5,7 +5,7 @@ use crate::ir::proto_graph::{Action, NodeId, Op, ProtoGraph}; use patronus::expr::{Context as ExprContext, ExprRef, TypeCheck}; use rustc_hash::FxHashMap; -fn mark_graft_point_ready(lowerer: &mut Lowerer<'_>, node: NodeId, guard: ExprRef) { +pub fn mark_graft_point_ready(lowerer: &mut Lowerer<'_>, node: NodeId, guard: ExprRef) { let already_ready = lowerer.ir[node] .actions .iter() @@ -16,7 +16,7 @@ fn mark_graft_point_ready(lowerer: &mut Lowerer<'_>, node: NodeId, guard: ExprRe } } -fn graft_choice_entries_into( +pub fn graft_choice_entries_into( lowerer: &mut Lowerer<'_>, parent: NodeId, choices: Vec<(NodeId, ExprRef)>, diff --git a/protocols/src/ir/mod.rs b/protocols/src/ir/mod.rs index b500f2d5..bf58d4c0 100644 --- a/protocols/src/ir/mod.rs +++ b/protocols/src/ir/mod.rs @@ -8,6 +8,7 @@ pub mod lowering; pub mod propagate_assigns; pub mod proto_graph; pub mod reaching_defs; +pub mod steady_state_lowering; pub mod trace_lowering; // TODO: add a function to transform AST to IR // pub fn frontend( diff --git a/protocols/src/ir/steady_state_lowering.rs b/protocols/src/ir/steady_state_lowering.rs new file mode 100644 index 00000000..825f03c6 --- /dev/null +++ b/protocols/src/ir/steady_state_lowering.rs @@ -0,0 +1,93 @@ +use crate::frontend::ast::Protocol; +use crate::frontend::symbol::{SymbolId, SymbolKind, SymbolTable}; +use crate::ir::bounded_lowering::{graft_choice_entries_into, mark_graft_point_ready}; +use crate::ir::edge_contract::contract_edges; +use crate::ir::lowering::{LoweredFragmentInfo, Lowerer}; +use crate::ir::proto_graph::{Action, NodeId, Op, ProtoGraph, Transition}; +use patronus::expr::{Context as ExprContext, ExprRef, TypeCheck}; +use rustc_hash::FxHashMap; + +/// Lower a set of protocols to a joint IR that represents traces of any length +/// Precondition: every `p \in protos` must fork in its exit node (there is no possibility of +/// overlapping protcols) +pub fn lower_steady_state( + protos: Vec, + symbols: &SymbolTable, + mut expr_ctx: ExprContext, +) -> (ProtoGraph, ExprRef) { + assert!(!protos.is_empty()); + let num_protos = protos.len(); + let width = if num_protos <= 1 { + 1 + } else { + usize::BITS - (num_protos - 1).leading_zeros() + }; + let proto_choice: ExprRef = expr_ctx.bv_symbol(&"proto_choice".to_string(), width); + + let first_ast = protos.first().unwrap(); + let mut graft_points: Vec<(NodeId, ExprRef)> = vec![]; + + // set up the lowerer and lower all the protocols + let mut lowerer = Lowerer::with_expr_ctx(first_ast.ctx.clone(), symbols, expr_ctx); + // TODO: Handle done vs not done + let mut lowered_protocols: Vec = vec![]; + for protocol in protos { + let mut pg = lowerer.lower_protocol_fragment(&protocol, false, true); + // lowerer.postprocess_trace_fragment(&pg); + pg.graft_points = lowerer.graft_points(&pg); + lowered_protocols.push(pg); + } + + let arg_symbols: Vec = lowerer + .symbols + .get_args() + .into_iter() + .filter(|symbol_id| { + matches!(lowerer.symbols[*symbol_id].kind(), SymbolKind::Arg(_)) + && lowerer.ir.symbol_expr(*symbol_id).is_some() + }) + .collect(); + + // TODO: kinda janky way to make an identity instance substitution + let instance_substitutions: FxHashMap = arg_symbols + .iter() + .filter_map(|symbol_id| lowerer.ir.symbol_expr(*symbol_id).map(|expr| (expr, expr))) + .collect(); + + let entry_node = lowerer.ir.entry; + + let mut initial_choices = Vec::with_capacity(num_protos); + for (idx, prototype) in lowered_protocols.iter().enumerate().take(num_protos) { + let proto_idx_expr = lowerer.ir.expr_ctx.bit_vec_val(idx, width); + let node_equals = if idx + 1 == num_protos { + lowerer + .ir + .expr_ctx + .greater_or_equal(proto_choice, proto_idx_expr) + } else { + lowerer.ir.expr_ctx.equal(proto_choice, proto_idx_expr) + }; + let new_frag = lowerer.copy_protocol_fragment(prototype.clone(), &instance_substitutions); + + // TODO: all exits have the done action. If these were interpreter, the graph interpreter would actually get mad at this, + // but it shouldn't. Done doesn't really have meaning for driver automata, just for monitors. + let done_op = lowerer.ir.o(Op::Done); + let true_id = lowerer.ir.true_id(); + lowerer + .ir + .push_action(new_frag.exit, Action::new(true_id, done_op)); + + for &(node, guard) in &new_frag.graft_points { + mark_graft_point_ready(&mut lowerer, node, guard); + } + graft_points.extend(new_frag.graft_points.clone()); + initial_choices.push((new_frag.entry, node_equals)); + } + graft_choice_entries_into(&mut lowerer, entry_node, initial_choices); + + // contract_edges(&mut lowerer.ir, lowerer.symbols); + + // pass in the initial IR with and its graft points, and append_trace_transactions will lower the rest of the trace from here. + lowerer.ir.simplify_all_exprs(); + (lowerer.ir, proto_choice) +} From f57e8561403cfd1b94335309d40a3217dd443bb0 Mon Sep 17 00:00:00 2001 From: Nikil Shyamsunder Date: Fri, 31 Jul 2026 16:24:27 -0400 Subject: [PATCH 2/7] implement looping in steady state --- protocols/src/ir/steady_state_lowering.rs | 41 ++++++++++++++--------- 1 file changed, 26 insertions(+), 15 deletions(-) diff --git a/protocols/src/ir/steady_state_lowering.rs b/protocols/src/ir/steady_state_lowering.rs index 825f03c6..d96fd43a 100644 --- a/protocols/src/ir/steady_state_lowering.rs +++ b/protocols/src/ir/steady_state_lowering.rs @@ -1,12 +1,26 @@ use crate::frontend::ast::Protocol; use crate::frontend::symbol::{SymbolId, SymbolKind, SymbolTable}; use crate::ir::bounded_lowering::{graft_choice_entries_into, mark_graft_point_ready}; -use crate::ir::edge_contract::contract_edges; use crate::ir::lowering::{LoweredFragmentInfo, Lowerer}; -use crate::ir::proto_graph::{Action, NodeId, Op, ProtoGraph, Transition}; -use patronus::expr::{Context as ExprContext, ExprRef, TypeCheck}; +use crate::ir::proto_graph::{Action, NodeId, Op, ProtoGraph}; +use patronus::expr::{Context as ExprContext, ExprRef}; use rustc_hash::FxHashMap; +fn loop_exit_to_entry(lowerer: &mut Lowerer<'_>, fragment: &LoweredFragmentInfo, entry: NodeId) { + for node in fragment.nodes.iter().copied() { + if node == fragment.exit { + continue; + } + + for transition in &mut lowerer.ir.node_mut(node).transitions { + if transition.target == fragment.exit { + transition.target = entry; + transition.consumes_step = true; + } + } + } +} + /// Lower a set of protocols to a joint IR that represents traces of any length /// Precondition: every `p \in protos` must fork in its exit node (there is no possibility of /// overlapping protcols) @@ -55,6 +69,9 @@ pub fn lower_steady_state( .collect(); let entry_node = lowerer.ir.entry; + // the entry node is a fork point (where we start new transactions) + let fork_op = lowerer.ir.o(Op::Fork); + lowerer.ir.push_action(entry_node, Action::new(lowerer.ir.true_id(), fork_op)); let mut initial_choices = Vec::with_capacity(num_protos); for (idx, prototype) in lowered_protocols.iter().enumerate().take(num_protos) { @@ -69,19 +86,13 @@ pub fn lower_steady_state( }; let new_frag = lowerer.copy_protocol_fragment(prototype.clone(), &instance_substitutions); - // TODO: all exits have the done action. If these were interpreter, the graph interpreter would actually get mad at this, - // but it shouldn't. Done doesn't really have meaning for driver automata, just for monitors. - let done_op = lowerer.ir.o(Op::Done); - let true_id = lowerer.ir.true_id(); - lowerer - .ir - .push_action(new_frag.exit, Action::new(true_id, done_op)); - - for &(node, guard) in &new_frag.graft_points { - mark_graft_point_ready(&mut lowerer, node, guard); - } - graft_points.extend(new_frag.graft_points.clone()); + // for &(node, guard) in &new_frag.graft_points { + // mark_graft_point_ready(&mut lowerer, node, guard); + // } + // graft_points.extend(new_frag.graft_points.clone()); initial_choices.push((new_frag.entry, node_equals)); + + loop_exit_to_entry(&mut lowerer, &new_frag, entry_node); } graft_choice_entries_into(&mut lowerer, entry_node, initial_choices); From 8ee1e96efa159b67c82c54b4c853f4127f8f5583 Mon Sep 17 00:00:00 2001 From: Nikil Shyamsunder Date: Fri, 31 Jul 2026 16:58:19 -0400 Subject: [PATCH 3/7] implement lowering to transition system that holds values --- examples/wishbone/read_write.tx | 8 +- graph-interp/src/main.rs | 106 +++++++++++++++++++++- protocols/src/ir/steady_state_lowering.rs | 27 +++--- 3 files changed, 125 insertions(+), 16 deletions(-) diff --git a/examples/wishbone/read_write.tx b/examples/wishbone/read_write.tx index 3eaac591..5c067be3 100644 --- a/examples/wishbone/read_write.tx +++ b/examples/wishbone/read_write.tx @@ -1,7 +1,11 @@ trace { reset(); write(0b1111, 0x4000000, 0x1111); - // reset(); + reset(); read(0b1111, 0x4000000, 0x1111); - //idle_no_cycle(); + idle_no_cycle(); + write(0b1111, 0x4000000, 0x1111); + reset(); + read(0b1111, 0x4000000, 0x1112); + idle_no_cycle(); } diff --git a/graph-interp/src/main.rs b/graph-interp/src/main.rs index 0ef4f926..246bb20d 100644 --- a/graph-interp/src/main.rs +++ b/graph-interp/src/main.rs @@ -528,17 +528,118 @@ fn run_steady_state( .iter() .map(|name| (*protos_by_name.get(*name).unwrap()).clone()) .collect(); + let protocol_arg_symbols: Vec<_> = used_protocols + .iter() + .flat_map(|protocol| protocol.args.iter().map(|arg| arg.symbol())) + .collect(); + let protocol_choice_indices: FxHashMap<&str, u64> = used_protocol_names + .iter() + .enumerate() + .map(|(index, name)| (*name, index as u64)) + .collect(); let sim = PatronusSim::new(&cli.verilog, cli.module.as_deref(), module, None).unwrap(); // The graph and DUT transition system must share an expression // context, including port expressions such as DUT.o_ack. - let (mut pg, _proto_choice) = lower_steady_state(used_protocols, st, sim.ctx.clone()); + let (mut pg, proto_choice) = lower_steady_state(used_protocols, st, sim.ctx.clone()); pg.garbage_collect_unreachable(); pg = determinized(pg, st); if cli.graphout { println!("{}", to_dot_string(&pg, st)); } + + let port_expr_refs: FxHashMap = FxHashMap::from_iter( + sim.ios() + .filter_map(|port| sim.get_port_expr(port).map(|expr| (port, expr))), + ); + let res = into_bmc_transition_system( + pg, + sim.sys.clone(), + vec![proto_choice], + sim.port_map.clone(), + port_expr_refs, + &protocol_arg_symbols, + st, + ); + + let proto_choice_width = if used_protocol_names.len() <= 1 { + 1 + } else { + usize::BITS - (used_protocol_names.len() - 1).leading_zeros() + }; + let mut transition_sim = Interpreter::new(&res.ctx, &res.ts); + transition_sim.init(InitKind::Zero); + let mut waveform = FxHashMap::default(); + let mut transaction_idx = 0; + + loop { + let at_fork = transition_sim + .get(res.fork_ready) + .try_into_u64() + .expect("fork ready failed") + == 1; + if at_fork { + if transaction_idx == trace.len() { + print_trace_success(trace_index); + break; + } + + let (proto_name, values) = &trace[transaction_idx]; + let proto = *protos_by_name.get(proto_name).unwrap(); + for (arg_expr, value) in proto + .args + .iter() + .map(|arg| res.protocol_inputs[&(0, arg.symbol())]) + .zip(values) + { + let value: BitVecValue = value.clone().try_into().expect("value not in bitvec"); + transition_sim.set(arg_expr, &value); + } + transition_sim.set( + res.protocol_choices[0], + &BitVecValue::from_u64( + protocol_choice_indices[proto_name.as_str()], + proto_choice_width, + ), + ); + transaction_idx += 1; + } + + record_transition_waveform( + &mut waveform, + &transition_sim, + &sim, + &res.port_to_expr, + &res.is_dont_care, + ); + transition_sim.step(); + + let state = transition_sim.get(res.node_symbol); + if state == transition_sim.get(res.external_assert_state) { + println!( + "Assertion failure while executing transaction {}.", + transaction_idx - 1 + ); + break; + } + if state == transition_sim.get(res.internal_assert_state) { + println!( + "Internal assertion failure while executing transaction {}.", + transaction_idx - 1 + ); + break; + } + } + + if cli.ascii_waveform { + print_ascii_waveform( + waveform, + |port| sim.port_name(port).to_string(), + |port| sim.port_width(port), + false, + ); + } } } @@ -553,8 +654,7 @@ fn main() { let _result = catch_unwind(AssertUnwindSafe(|| { if cli.steady_state { run_steady_state(&cli, &st, &module, &traces); - } - if cli.bound > 0 { + } else if cli.bound > 0 { run_bmc(&cli, &st, &module, &traces); } else if cli.transition_system { run_transition_system(&cli, &st, &module, &traces); diff --git a/protocols/src/ir/steady_state_lowering.rs b/protocols/src/ir/steady_state_lowering.rs index d96fd43a..89665ec7 100644 --- a/protocols/src/ir/steady_state_lowering.rs +++ b/protocols/src/ir/steady_state_lowering.rs @@ -1,9 +1,9 @@ use crate::frontend::ast::Protocol; use crate::frontend::symbol::{SymbolId, SymbolKind, SymbolTable}; -use crate::ir::bounded_lowering::{graft_choice_entries_into, mark_graft_point_ready}; +use crate::ir::bounded_lowering::graft_choice_entries_into; use crate::ir::lowering::{LoweredFragmentInfo, Lowerer}; use crate::ir::proto_graph::{Action, NodeId, Op, ProtoGraph}; -use patronus::expr::{Context as ExprContext, ExprRef}; +use patronus::expr::{Context as ExprContext, ExprRef, TypeCheck}; use rustc_hash::FxHashMap; fn loop_exit_to_entry(lowerer: &mut Lowerer<'_>, fragment: &LoweredFragmentInfo, entry: NodeId) { @@ -39,7 +39,6 @@ pub fn lower_steady_state( let proto_choice: ExprRef = expr_ctx.bv_symbol(&"proto_choice".to_string(), width); let first_ast = protos.first().unwrap(); - let mut graft_points: Vec<(NodeId, ExprRef)> = vec![]; // set up the lowerer and lower all the protocols let mut lowerer = Lowerer::with_expr_ctx(first_ast.ctx.clone(), symbols, expr_ctx); @@ -62,16 +61,26 @@ pub fn lower_steady_state( }) .collect(); - // TODO: kinda janky way to make an identity instance substitution + // The steady-state automaton has one reusable transaction slot. Use the + // same #0 argument names that `into_bmc_transition_system` creates for its + // first slot so the copied graph reads those transition-system inputs. let instance_substitutions: FxHashMap = arg_symbols .iter() - .filter_map(|symbol_id| lowerer.ir.symbol_expr(*symbol_id).map(|expr| (expr, expr))) + .filter_map(|symbol_id| { + let old_expr = lowerer.ir.symbol_expr(*symbol_id)?; + let width = old_expr.get_bv_type(&lowerer.ir.expr_ctx)?; + let name = lowerer.symbols.full_name_from_symbol_id(symbol_id); + let slot_expr = lowerer.ir.expr_ctx.bv_symbol(&format!("{name}#0"), width); + Some((old_expr, slot_expr)) + }) .collect(); let entry_node = lowerer.ir.entry; // the entry node is a fork point (where we start new transactions) let fork_op = lowerer.ir.o(Op::Fork); - lowerer.ir.push_action(entry_node, Action::new(lowerer.ir.true_id(), fork_op)); + lowerer + .ir + .push_action(entry_node, Action::new(lowerer.ir.true_id(), fork_op)); let mut initial_choices = Vec::with_capacity(num_protos); for (idx, prototype) in lowered_protocols.iter().enumerate().take(num_protos) { @@ -86,12 +95,8 @@ pub fn lower_steady_state( }; let new_frag = lowerer.copy_protocol_fragment(prototype.clone(), &instance_substitutions); - // for &(node, guard) in &new_frag.graft_points { - // mark_graft_point_ready(&mut lowerer, node, guard); - // } - // graft_points.extend(new_frag.graft_points.clone()); initial_choices.push((new_frag.entry, node_equals)); - + loop_exit_to_entry(&mut lowerer, &new_frag, entry_node); } graft_choice_entries_into(&mut lowerer, entry_node, initial_choices); From ac7aa56811e217da6018486e4cb112691974a5fd Mon Sep 17 00:00:00 2001 From: Nikil Shyamsunder Date: Mon, 3 Aug 2026 11:41:40 -0400 Subject: [PATCH 4/7] to monitor --- protocols/src/frontend/remap.rs | 3 + protocols/src/frontend/symbol.rs | 7 + protocols/src/interpreter.rs | 6 + protocols/src/ir/mod.rs | 1 + protocols/src/ir/proto_graph.rs | 10 + protocols/src/ir/to_monitor.rs | 493 +++++++++++++++++++++++++++++++ 6 files changed, 520 insertions(+) create mode 100644 protocols/src/ir/to_monitor.rs diff --git a/protocols/src/frontend/remap.rs b/protocols/src/frontend/remap.rs index 3fa67235..248537d2 100644 --- a/protocols/src/frontend/remap.rs +++ b/protocols/src/frontend/remap.rs @@ -361,6 +361,9 @@ impl Remapper<'_> { .unwrap_or_else(|| unreachable!("{name} should have been declared!")); self.out.e(Expr::Sym(out_sym)) } + SymbolKind::MonitorState => { + unreachable!("monitor state is not part of frontend remapping") + } } } Expr::DontCare => self.out.dont_care_id(), diff --git a/protocols/src/frontend/symbol.rs b/protocols/src/frontend/symbol.rs index 0ff97fe1..a3336b8b 100644 --- a/protocols/src/frontend/symbol.rs +++ b/protocols/src/frontend/symbol.rs @@ -53,6 +53,9 @@ pub enum SymbolKind { OutPort, Arg(u16), LoopVar, + /// State introduced by an IR-to-IR transformation, such as protocol + /// argument knownness in a generated monitor. + MonitorState, } #[derive(Clone, Copy, Hash, PartialEq, Eq, Default)] @@ -596,4 +599,8 @@ impl SymbolTableEntry { pub fn is_loop_var(&self) -> bool { matches!(self.kind, SymbolKind::LoopVar) } + + pub fn is_monitor_state(&self) -> bool { + matches!(self.kind, SymbolKind::MonitorState) + } } diff --git a/protocols/src/interpreter.rs b/protocols/src/interpreter.rs index 3c8658f1..15664e42 100644 --- a/protocols/src/interpreter.rs +++ b/protocols/src/interpreter.rs @@ -523,6 +523,9 @@ impl<'a> Evaluator<'a> { .unwrap(); Ok(ExprValue::Concrete(value.clone())) } + SymbolKind::MonitorState => { + unreachable!("monitor state is not part of AST interpretation") + } } } Expr::DontCare => Ok(ExprValue::DontCare), @@ -741,6 +744,9 @@ impl<'a> Evaluator<'a> { "loop_var".to_string(), stmt_id, )), + SymbolKind::MonitorState => { + unreachable!("monitor state is not part of AST interpretation") + } } } diff --git a/protocols/src/ir/mod.rs b/protocols/src/ir/mod.rs index bf58d4c0..f1909f64 100644 --- a/protocols/src/ir/mod.rs +++ b/protocols/src/ir/mod.rs @@ -9,6 +9,7 @@ pub mod propagate_assigns; pub mod proto_graph; pub mod reaching_defs; pub mod steady_state_lowering; +pub mod to_monitor; pub mod trace_lowering; // TODO: add a function to transform AST to IR // pub fn frontend( diff --git a/protocols/src/ir/proto_graph.rs b/protocols/src/ir/proto_graph.rs index a2b23a92..026ae8ef 100644 --- a/protocols/src/ir/proto_graph.rs +++ b/protocols/src/ir/proto_graph.rs @@ -145,6 +145,14 @@ pub struct ProtoGraph { /// symbol expressions representing DontCare pub dont_cares: FxHashSet, + /// Symbols that are state in this graph and their initial values. + /// + /// This is populated by IR-to-IR transformations such as `to_monitor`. + /// Keeping the declaration on the graph lets `Op::Assign` represent both + /// DUT driving assignments in a driver graph and state updates in a + /// monitor graph without adding another operation kind. + pub state_init: FxHashMap, + nodes: PrimaryMap, ops: PrimaryMap, @@ -163,6 +171,7 @@ impl Clone for ProtoGraph { simplifier: Simplifier::new(SparseExprMap::default()), symbol_expr: self.symbol_expr.clone(), dont_cares: self.dont_cares.clone(), + state_init: self.state_init.clone(), nodes: self.nodes.clone(), ops: self.ops.clone(), op_loc: self.op_loc.clone(), @@ -190,6 +199,7 @@ impl ProtoGraph { simplifier: Simplifier::new(SparseExprMap::default()), symbol_expr: FxHashMap::default(), dont_cares: FxHashSet::default(), + state_init: FxHashMap::default(), nodes, ops, op_loc, diff --git a/protocols/src/ir/to_monitor.rs b/protocols/src/ir/to_monitor.rs new file mode 100644 index 00000000..b5d4ac35 --- /dev/null +++ b/protocols/src/ir/to_monitor.rs @@ -0,0 +1,493 @@ +use crate::frontend::symbol::{SymbolId, SymbolKind, SymbolTable, Type}; +use crate::ir::proto_graph::{Action, Assignment, Op, ProtoGraph}; +use patronus::expr::{ExprRef, TypeCheck, simple_transform_expr}; +use rustc_hash::{FxHashMap, FxHashSet}; +use thiserror::Error; + +#[derive(Debug, Error, PartialEq, Eq)] +pub enum ToMonitorError { + #[error("monitor parameters must be bit-vectors: {0}")] + NonBitVectorParameter(String), + #[error("assignment target has no expression in the ProtoGraph: {0:?}")] + MissingAssignmentTarget(SymbolId), + #[error("fork actions are only supported on the steady-state entry node")] + UnsupportedFork, +} + +#[derive(Clone, Copy)] +struct ParameterState { + symbol: SymbolId, + expr: ExprRef, + known_symbol: SymbolId, + known_expr: ExprRef, +} + +fn expression_roots(pg: &ProtoGraph) -> Vec { + let mut roots = Vec::new(); + for (_, node) in pg.nodes() { + for transition in &node.transitions { + roots.push(transition.guard); + } + for action in &node.actions { + roots.push(action.guard); + match &pg[action.op] { + Op::Assign(_, assignment) => { + roots.push(assignment.dont_care); + for (guard, rhs) in &assignment.concretes { + roots.push(*guard); + roots.push(*rhs); + } + } + Op::AssertEq(lhs, rhs) => { + roots.push(*lhs); + roots.push(*rhs); + } + Op::Fork | Op::InternalAssertFalse | Op::Done => {} + } + } + } + roots +} + +fn referenced_symbols(pg: &mut ProtoGraph) -> FxHashMap { + let mut symbols = FxHashMap::default(); + for root in expression_roots(pg) { + simple_transform_expr(&mut pg.expr_ctx, root, |ctx, candidate, _children| { + if let Some(name) = ctx.get_symbol_name(candidate) { + symbols.insert(name.to_string(), candidate); + } + None + }); + } + symbols +} + +fn create_parameter_states( + pg: &mut ProtoGraph, + symbols: &mut SymbolTable, +) -> Result, ToMonitorError> { + let referenced = referenced_symbols(pg); + let cached_args: Vec<(SymbolId, ExprRef)> = pg + .symbol_expr + .iter() + .filter_map(|(symbol, expr)| { + matches!(symbols[*symbol].kind(), SymbolKind::Arg(_)).then_some((*symbol, *expr)) + }) + .collect(); + + // Steady-state lowering renames the one reusable argument bank with `#0`. + // Multiple protocol scopes may contain the same argument name; those map to + // the same monitor register, which is precisely the one-bank assumption. + let mut by_expr: FxHashMap = FxHashMap::default(); + for (symbol, cached_expr) in cached_args { + let name = symbols.full_name_from_symbol_id(&symbol); + let parameter_expr = referenced + .get(&format!("{name}#0")) + .or_else(|| referenced.get(&name)) + .copied() + .unwrap_or(cached_expr); + by_expr.entry(parameter_expr).or_insert(symbol); + } + + let mut parameters = Vec::with_capacity(by_expr.len()); + for (expr, symbol) in by_expr { + let width = expr.get_bv_type(&pg.expr_ctx).ok_or_else(|| { + ToMonitorError::NonBitVectorParameter(symbols.full_name_from_symbol_id(&symbol)) + })?; + let known_name = format!("__monitor_arg{}_known", symbol.as_u32()); + let known_symbol = + if let Some(existing) = symbols.symbol_id_from_name_in_active_scope(&known_name) { + existing + } else { + symbols.add_without_parent( + known_name.clone(), + Type::BitVec(1), + SymbolKind::MonitorState, + ) + }; + let known_expr = pg.expr_ctx.bv_symbol(&known_name, 1); + + // Assigning the original argument SymbolId now updates its monitor + // register. Cache the expression actually used by the steady-state PG. + pg.cache_symbol_expr(symbol, expr); + pg.cache_symbol_expr(known_symbol, known_expr); + pg.state_init + .insert(symbol, pg.expr_ctx.bit_vec_val(0, width)); + pg.state_init.insert(known_symbol, pg.false_id()); + parameters.push(ParameterState { + symbol, + expr, + known_symbol, + known_expr, + }); + } + Ok(parameters) +} + +fn symbol_expr( + pg: &mut ProtoGraph, + symbols: &SymbolTable, + symbol: SymbolId, +) -> Result { + if let Some(expr) = pg.symbol_expr(symbol) { + return Ok(expr); + } + let Type::BitVec(width) = symbols[symbol].tpe() else { + return Err(ToMonitorError::MissingAssignmentTarget(symbol)); + }; + let name = symbols.full_name_from_symbol_id(&symbol); + let expr = pg.expr_ctx.bv_symbol(&name, width); + pg.cache_symbol_expr(symbol, expr); + Ok(expr) +} + +fn parameters_in_expr( + pg: &mut ProtoGraph, + expr: ExprRef, + by_expr: &FxHashMap, +) -> Vec { + let mut found = FxHashSet::default(); + simple_transform_expr(&mut pg.expr_ctx, expr, |_ctx, candidate, _children| { + if by_expr.contains_key(&candidate) { + found.insert(candidate); + } + None + }); + found + .into_iter() + .map(|candidate| by_expr[&candidate]) + .collect() +} + +fn and_all(pg: &mut ProtoGraph, terms: impl IntoIterator) -> ExprRef { + terms + .into_iter() + .fold(pg.true_id(), |acc, term| pg.and_guard(acc, term)) +} + +fn push_assign( + pg: &mut ProtoGraph, + actions: &mut Vec, + guard: ExprRef, + lhs: SymbolId, + rhs: ExprRef, +) { + let assignment = Assignment::concrete(pg.false_id(), pg.true_id(), rhs); + let op = pg.o(Op::Assign(lhs, assignment)); + actions.push(Action::new(guard, op)); +} + +fn push_assert( + pg: &mut ProtoGraph, + actions: &mut Vec, + guard: ExprRef, + lhs: ExprRef, + rhs: ExprRef, +) { + let op = pg.o(Op::AssertEq(lhs, rhs)); + actions.push(Action::new(guard, op)); +} + +fn push_internal_assert_false(pg: &mut ProtoGraph, actions: &mut Vec, guard: ExprRef) { + let op = pg.o(Op::InternalAssertFalse); + actions.push(Action::new(guard, op)); +} + +/// Turn one equality into explicit learn/check actions. +/// +/// A whole unknown parameter may be assigned from the other, fully-known side. +/// Once every referenced parameter is known, the equality is checked normally. +/// Any active case requiring partial or relational inference becomes an explicit +/// internal assertion failure in the monitor graph. +fn lower_equality( + pg: &mut ProtoGraph, + actions: &mut Vec, + active: ExprRef, + lhs: ExprRef, + rhs: ExprRef, + parameters: &FxHashMap, +) { + let lhs_parameters = parameters_in_expr(pg, lhs, parameters); + let rhs_parameters = parameters_in_expr(pg, rhs, parameters); + let mut all_parameters = lhs_parameters.clone(); + for parameter in &rhs_parameters { + if !all_parameters + .iter() + .any(|other| other.expr == parameter.expr) + { + all_parameters.push(*parameter); + } + } + + if all_parameters.is_empty() { + push_assert(pg, actions, active, lhs, rhs); + return; + } + + let all_known = and_all( + pg, + all_parameters.iter().map(|parameter| parameter.known_expr), + ); + let check_guard = pg.and_guard(active, all_known); + push_assert(pg, actions, check_guard, lhs, rhs); + + let mut handled = all_known; + if let Some(parameter) = parameters.get(&lhs).copied() { + let rhs_known = and_all(pg, rhs_parameters.iter().map(|other| other.known_expr)); + let lhs_unknown = pg.not_guard(parameter.known_expr); + let can_bind = pg.and_guard(lhs_unknown, rhs_known); + let bind_guard = pg.and_guard(active, can_bind); + push_assign(pg, actions, bind_guard, parameter.symbol, rhs); + push_assign( + pg, + actions, + bind_guard, + parameter.known_symbol, + pg.true_id(), + ); + handled = pg.or_guard(handled, can_bind); + } + if let Some(parameter) = parameters.get(&rhs).copied() { + let lhs_known = and_all(pg, lhs_parameters.iter().map(|other| other.known_expr)); + let rhs_unknown = pg.not_guard(parameter.known_expr); + let can_bind = pg.and_guard(rhs_unknown, lhs_known); + let bind_guard = pg.and_guard(active, can_bind); + push_assign(pg, actions, bind_guard, parameter.symbol, lhs); + push_assign( + pg, + actions, + bind_guard, + parameter.known_symbol, + pg.true_id(), + ); + handled = pg.or_guard(handled, can_bind); + } + + let unhandled = pg.not_guard(handled); + let unsupported_guard = pg.and_guard(active, unhandled); + push_internal_assert_false(pg, actions, unsupported_guard); +} + +/// Convert a steady-state driver `ProtoGraph` into an explicit monitor graph. +/// +/// DUT assignments become equalities against observed DUT ports. Whole unknown +/// arguments are learned with guarded `Op::Assign` actions; later observations +/// are checked with guarded `Op::AssertEq` actions. The one-bank assumption is +/// reflected by sharing a monitor register for each argument expression. +pub fn to_monitor( + mut pg: ProtoGraph, + symbols: &mut SymbolTable, +) -> Result { + let parameter_states = create_parameter_states(&mut pg, symbols)?; + let parameters: FxHashMap = parameter_states + .iter() + .map(|parameter| (parameter.expr, *parameter)) + .collect(); + let node_ids: Vec<_> = pg.nodes().map(|(node, _)| node).collect(); + + for node_id in node_ids { + let old_actions = pg[node_id].actions.clone(); + let transitions = pg[node_id].transitions.clone(); + let mut new_actions = Vec::new(); + + for action in old_actions { + match pg[action.op].clone() { + Op::Assign(port, assignment) => { + let port_expr = symbol_expr(&mut pg, symbols, port)?; + for (assignment_guard, rhs) in assignment.concretes { + let active = pg.and_guard(action.guard, assignment_guard); + lower_equality( + &mut pg, + &mut new_actions, + active, + port_expr, + rhs, + ¶meters, + ); + } + // DontCare branches intentionally impose no monitor constraint. + } + Op::AssertEq(lhs, rhs) => lower_equality( + &mut pg, + &mut new_actions, + action.guard, + lhs, + rhs, + ¶meters, + ), + Op::Fork if node_id == pg.entry => {} + Op::Fork => return Err(ToMonitorError::UnsupportedFork), + Op::InternalAssertFalse | Op::Done => new_actions.push(action), + } + } + + // A steady-state back-edge starts a fresh transaction. Clear all + // knownness registers on the same edge that returns to the entry. + let entry = pg.entry; + let false_id = pg.false_id(); + for transition in transitions + .iter() + .filter(|transition| transition.target == entry) + { + for parameter in ¶meter_states { + push_assign( + &mut pg, + &mut new_actions, + transition.guard, + parameter.known_symbol, + false_id, + ); + } + } + + pg.node_mut(node_id).actions = new_actions; + } + + pg.simplify_all_exprs(); + Ok(pg) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::frontend; + use crate::frontend::diagnostic::DiagnosticHandler; + use crate::frontend::require_single_module; + use crate::ir::graphviz::to_dot_string; + use crate::ir::steady_state_lowering::lower_steady_state; + use patronus::expr::Context as ExprContext; + use std::fs; + use tempfile::NamedTempFile; + + fn lower_monitor(source: &str) -> (ProtoGraph, SymbolTable) { + let file = NamedTempFile::new().unwrap(); + fs::write(file.path(), source).unwrap(); + let mut diagnostics = DiagnosticHandler::default(); + let (mut symbols, modules) = frontend(&[file.path()], &mut diagnostics, true).unwrap(); + let module = require_single_module(modules, &[file.path()]).unwrap(); + let (driver, _) = lower_steady_state(module.protos, &symbols, ExprContext::default()); + let monitor = to_monitor(driver, &mut symbols).unwrap(); + (monitor, symbols) + } + + #[test] + fn steady_state_driver_actions_become_explicit_monitor_state_updates() { + let (monitor, symbols) = lower_monitor( + r#" + struct Device { + in x: u32, + out z: u32, + } + + prot transaction(a: u32) { + dut.x := a; + step(); + assert_eq(dut.z, a); + step(); + } + "#, + ); + + let mut saw_argument_update = false; + let mut saw_knownness_update = false; + let mut saw_monitor_assertion = false; + + for (_, node) in monitor.nodes() { + for action in &node.actions { + match &monitor[action.op] { + Op::Assign(symbol, _) => match symbols[*symbol].kind() { + SymbolKind::Arg(_) => saw_argument_update = true, + SymbolKind::MonitorState => saw_knownness_update = true, + SymbolKind::InPort | SymbolKind::OutPort => { + panic!("monitor graph still drives a DUT port") + } + SymbolKind::Dut | SymbolKind::LoopVar => { + panic!("unexpected monitor assignment target") + } + }, + Op::AssertEq(_, _) => saw_monitor_assertion = true, + Op::Fork => panic!("synthetic steady-state fork was not removed"), + Op::InternalAssertFalse | Op::Done => {} + } + } + } + + assert!(saw_argument_update); + assert!(saw_knownness_update); + assert!(saw_monitor_assertion); + assert_eq!( + monitor + .state_init + .keys() + .filter(|symbol| symbols[**symbol].is_arg()) + .count(), + 1 + ); + assert_eq!( + monitor + .state_init + .keys() + .filter(|symbol| symbols[**symbol].is_monitor_state()) + .count(), + 1 + ); + } + + #[test] + fn serializes_normal_swapped_monitor() { + let (monitor, symbols) = lower_monitor( + r#" + struct Device { + in x: u32, + in y: u32, + out z: u32, + } + + prot normal(a: u32, b: u32) { + dut.x := a; + dut.y := b; + step(); + assert_eq(dut.z, a); + step(); + } + + prot swapped(a: u32, b: u32) { + dut.x := b; + dut.y := a; + step(); + assert_eq(dut.z, a); + step(); + } + "#, + ); + + let serialized = to_dot_string(&monitor, &symbols); + println!("{serialized}"); + assert!(serialized.contains("__monitor_arg")); + assert!(serialized.contains("assert_eq")); + } + + #[test] + fn serializes_add_d0_monitor() { + let (monitor, symbols) = lower_monitor( + r#" + struct Device { + in a: u32, + in b: u32, + out s: u32, + } + + prot add(a: u32, b: u32, s: u32) { + dut.a := a; + dut.b := b; + step(); + assert_eq(dut.s, s); + step(); + } + "#, + ); + + let serialized = to_dot_string(&monitor, &symbols); + println!("{serialized}"); + } +} From fb712fcd4d9ee422eb74cbee469c50359a6e4fb3 Mon Sep 17 00:00:00 2001 From: Nikil Shyamsunder Date: Mon, 3 Aug 2026 12:02:38 -0400 Subject: [PATCH 5/7] eliminate registers via a static analysis of known bits --- protocols/src/ir/determinize.rs | 47 +- protocols/src/ir/to_monitor.rs | 872 ++++++++++++++++++------ scripts/wishbone_read_write_monitor.dot | 52 ++ 3 files changed, 767 insertions(+), 204 deletions(-) create mode 100644 scripts/wishbone_read_write_monitor.dot diff --git a/protocols/src/ir/determinize.rs b/protocols/src/ir/determinize.rs index bde4775e..2e30cb30 100644 --- a/protocols/src/ir/determinize.rs +++ b/protocols/src/ir/determinize.rs @@ -93,6 +93,44 @@ pub fn determinized(protocol: ProtoGraph, symbols: &SymbolTable) -> ProtoGraph { )); } + // The DFA successor only records which NFA target nodes are active, + // not which of several parallel edges activated each target. Collapse + // those parallel edges before enumerating subsets. Otherwise every + // equivalent edge selection becomes a separate minterm which is later + // ORed back together into a very large expression. + let mut grouped: Vec = Vec::new(); + for transition in transitions { + if let Some(existing) = grouped + .iter_mut() + .find(|existing| existing.target == transition.target) + { + existing.guard = protocol.or_guard(existing.guard, transition.guard); + } else { + grouped.push(transition); + } + } + let transitions = grouped; + + if let Some(first) = transitions.first() + && transitions + .iter() + .all(|transition| transition.target == first.target) + { + let guard = transitions + .iter() + .fold(protocol.false_id(), |guard, transition| { + protocol.or_guard(guard, transition.guard) + }); + let target = BTreeSet::from([first.target]); + let target_id = + get_or_create_state(target, &mut state_ids, &mut worklist, &mut new_nodes); + new_nodes[this_id] = NFANode { + actions, + transitions: vec![Transition::new(guard, target_id, true)], + }; + continue; + } + let mut new_trans: Vec = Vec::new(); let n = transitions.len(); let transition_guards: Vec<_> = transitions.iter().map(|t| t.guard).collect(); @@ -136,9 +174,14 @@ pub fn determinized(protocol: ProtoGraph, symbols: &SymbolTable) -> ProtoGraph { SatResult::MaybeSat => guard, }; + let target_id = + get_or_create_state(targets, &mut state_ids, &mut worklist, &mut new_nodes); + if let Some(existing) = new_trans + .iter_mut() + .find(|transition| transition.target == target_id && transition.consumes_step) { - let target_id = - get_or_create_state(targets, &mut state_ids, &mut worklist, &mut new_nodes); + existing.guard = protocol.or_guard(existing.guard, guard); + } else { new_trans.push(Transition::new(guard, target_id, true)); } } diff --git a/protocols/src/ir/to_monitor.rs b/protocols/src/ir/to_monitor.rs index b5d4ac35..7bdfc252 100644 --- a/protocols/src/ir/to_monitor.rs +++ b/protocols/src/ir/to_monitor.rs @@ -1,127 +1,61 @@ +use crate::frontend::ast::Protocol; use crate::frontend::symbol::{SymbolId, SymbolKind, SymbolTable, Type}; -use crate::ir::proto_graph::{Action, Assignment, Op, ProtoGraph}; -use patronus::expr::{ExprRef, TypeCheck, simple_transform_expr}; +use crate::ir::determinize::{SatResult, check_sat, determinized}; +use crate::ir::lowering::{LoweredFragmentInfo, Lowerer}; +use crate::ir::proto_graph::{Action, Assignment, NodeId, Op, ProtoGraph}; +use patronus::expr::{Context as ExprContext, ExprRef, simple_transform_expr}; use rustc_hash::{FxHashMap, FxHashSet}; +use std::collections::VecDeque; use thiserror::Error; #[derive(Debug, Error, PartialEq, Eq)] pub enum ToMonitorError { + #[error("cannot construct a monitor from an empty protocol set")] + EmptyProtocolSet, #[error("monitor parameters must be bit-vectors: {0}")] NonBitVectorParameter(String), #[error("assignment target has no expression in the ProtoGraph: {0:?}")] MissingAssignmentTarget(SymbolId), - #[error("fork actions are only supported on the steady-state entry node")] + #[error("monitor lowering does not support fork actions")] UnsupportedFork, } -#[derive(Clone, Copy)] -struct ParameterState { +#[derive(Clone)] +struct ParameterSeed { + original: SymbolId, symbol: SymbolId, - expr: ExprRef, known_symbol: SymbolId, - known_expr: ExprRef, + name: String, + known_name: String, + width: u32, } -fn expression_roots(pg: &ProtoGraph) -> Vec { - let mut roots = Vec::new(); - for (_, node) in pg.nodes() { - for transition in &node.transitions { - roots.push(transition.guard); - } - for action in &node.actions { - roots.push(action.guard); - match &pg[action.op] { - Op::Assign(_, assignment) => { - roots.push(assignment.dont_care); - for (guard, rhs) in &assignment.concretes { - roots.push(*guard); - roots.push(*rhs); - } - } - Op::AssertEq(lhs, rhs) => { - roots.push(*lhs); - roots.push(*rhs); - } - Op::Fork | Op::InternalAssertFalse | Op::Done => {} - } - } - } - roots +#[derive(Clone)] +struct ProtocolSeed { + live_symbol: SymbolId, + live_name: String, + parameters: Vec, } -fn referenced_symbols(pg: &mut ProtoGraph) -> FxHashMap { - let mut symbols = FxHashMap::default(); - for root in expression_roots(pg) { - simple_transform_expr(&mut pg.expr_ctx, root, |ctx, candidate, _children| { - if let Some(name) = ctx.get_symbol_name(candidate) { - symbols.insert(name.to_string(), candidate); - } - None - }); - } - symbols +struct CandidateState { + live_symbol: SymbolId, + live_expr: ExprRef, + parameters: Vec, } -fn create_parameter_states( - pg: &mut ProtoGraph, - symbols: &mut SymbolTable, -) -> Result, ToMonitorError> { - let referenced = referenced_symbols(pg); - let cached_args: Vec<(SymbolId, ExprRef)> = pg - .symbol_expr - .iter() - .filter_map(|(symbol, expr)| { - matches!(symbols[*symbol].kind(), SymbolKind::Arg(_)).then_some((*symbol, *expr)) - }) - .collect(); - - // Steady-state lowering renames the one reusable argument bank with `#0`. - // Multiple protocol scopes may contain the same argument name; those map to - // the same monitor register, which is precisely the one-bank assumption. - let mut by_expr: FxHashMap = FxHashMap::default(); - for (symbol, cached_expr) in cached_args { - let name = symbols.full_name_from_symbol_id(&symbol); - let parameter_expr = referenced - .get(&format!("{name}#0")) - .or_else(|| referenced.get(&name)) - .copied() - .unwrap_or(cached_expr); - by_expr.entry(parameter_expr).or_insert(symbol); - } - - let mut parameters = Vec::with_capacity(by_expr.len()); - for (expr, symbol) in by_expr { - let width = expr.get_bv_type(&pg.expr_ctx).ok_or_else(|| { - ToMonitorError::NonBitVectorParameter(symbols.full_name_from_symbol_id(&symbol)) - })?; - let known_name = format!("__monitor_arg{}_known", symbol.as_u32()); - let known_symbol = - if let Some(existing) = symbols.symbol_id_from_name_in_active_scope(&known_name) { - existing - } else { - symbols.add_without_parent( - known_name.clone(), - Type::BitVec(1), - SymbolKind::MonitorState, - ) - }; - let known_expr = pg.expr_ctx.bv_symbol(&known_name, 1); +#[derive(Clone, Copy)] +struct ParameterState { + symbol: SymbolId, + expr: ExprRef, + known_symbol: Option, + known_expr: Option, +} - // Assigning the original argument SymbolId now updates its monitor - // register. Cache the expression actually used by the steady-state PG. - pg.cache_symbol_expr(symbol, expr); - pg.cache_symbol_expr(known_symbol, known_expr); - pg.state_init - .insert(symbol, pg.expr_ctx.bit_vec_val(0, width)); - pg.state_init.insert(known_symbol, pg.false_id()); - parameters.push(ParameterState { - symbol, - expr, - known_symbol, - known_expr, - }); - } - Ok(parameters) +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum Knownness { + Unknown, + Known, + Maybe, } fn symbol_expr( @@ -159,6 +93,132 @@ fn parameters_in_expr( .collect() } +fn join_knownness(lhs: Knownness, rhs: Knownness) -> Knownness { + if lhs == rhs { lhs } else { Knownness::Maybe } +} + +fn or_all(pg: &mut ProtoGraph, guards: impl IntoIterator) -> ExprRef { + guards + .into_iter() + .fold(pg.false_id(), |acc, guard| pg.or_guard(acc, guard)) +} + +fn node_equalities(pg: &mut ProtoGraph, node: NodeId) -> Vec<(ExprRef, ExprRef, ExprRef)> { + let actions = pg[node].actions.clone(); + let mut equalities = Vec::new(); + for action in actions { + match pg[action.op].clone() { + Op::Assign(symbol, assignment) => { + let lhs = pg.symbol_expr(symbol).unwrap(); + for (guard, rhs) in assignment.concretes { + let guard = pg.and_guard(action.guard, guard); + equalities.push((guard, lhs, rhs)); + } + } + Op::AssertEq(lhs, rhs) => equalities.push((action.guard, lhs, rhs)), + Op::Fork | Op::InternalAssertFalse | Op::Done => {} + } + } + equalities +} + +fn transfer_knownness( + pg: &mut ProtoGraph, + node: NodeId, + input: &FxHashMap, + parameters: &FxHashMap, +) -> FxHashMap { + let equalities = node_equalities(pg, node); + let mut output = input.clone(); + + let mut definite: FxHashMap> = FxHashMap::default(); + let mut possible: FxHashMap> = FxHashMap::default(); + + for (guard, lhs, rhs) in &equalities { + for (candidate, other) in [(*lhs, *rhs), (*rhs, *lhs)] { + if !parameters.contains_key(&candidate) { + continue; + } + let dependencies = parameters_in_expr(pg, other, parameters); + if dependencies + .iter() + .all(|dependency| input[&dependency.expr] == Knownness::Known) + { + definite.entry(candidate).or_default().push(*guard); + } + if dependencies + .iter() + .all(|dependency| input[&dependency.expr] != Knownness::Unknown) + { + possible.entry(candidate).or_default().push(*guard); + } + } + } + + for parameter in parameters.values() { + let definitely_learned = definite + .remove(¶meter.expr) + .map(|guards| or_all(pg, guards)) + .is_some_and(|guard| matches!(check_sat(pg, guard), SatResult::AlwaysSat)); + let possibly_learned = possible + .remove(¶meter.expr) + .map(|guards| or_all(pg, guards)) + .is_some_and(|guard| !matches!(check_sat(pg, guard), SatResult::DefinitelyUnsat)); + + output.insert( + parameter.expr, + match (input[¶meter.expr], definitely_learned, possibly_learned) { + (Knownness::Known, _, _) | (_, true, _) => Knownness::Known, + (Knownness::Unknown, false, true) => Knownness::Maybe, + (knownness, false, false) => knownness, + (Knownness::Maybe, false, true) => Knownness::Maybe, + }, + ); + } + + output +} + +fn analyze_knownness( + pg: &mut ProtoGraph, + entry: NodeId, + parameters: &FxHashMap, +) -> FxHashMap> { + let unknown: FxHashMap = parameters + .keys() + .map(|expr| (*expr, Knownness::Unknown)) + .collect(); + let mut input_facts = FxHashMap::default(); + input_facts.insert(entry, unknown.clone()); + let mut worklist = VecDeque::from([entry]); + + while let Some(node) = worklist.pop_front() { + let output = transfer_knownness(pg, node, &input_facts[&node], parameters); + let transitions = pg[node].transitions.clone(); + for transition in transitions { + let incoming = output.clone(); + let changed = if let Some(existing) = input_facts.get_mut(&transition.target) { + let old = existing.clone(); + for (expr, knownness) in incoming { + existing + .entry(expr) + .and_modify(|current| *current = join_knownness(*current, knownness)) + .or_insert(knownness); + } + *existing != old + } else { + input_facts.insert(transition.target, incoming); + true + }; + if changed { + worklist.push_back(transition.target); + } + } + } + + input_facts +} + fn and_all(pg: &mut ProtoGraph, terms: impl IntoIterator) -> ExprRef { terms .into_iter() @@ -172,41 +232,62 @@ fn push_assign( lhs: SymbolId, rhs: ExprRef, ) { - let assignment = Assignment::concrete(pg.false_id(), pg.true_id(), rhs); + let assignment = Assignment::concrete(pg.false_id(), guard, rhs); let op = pg.o(Op::Assign(lhs, assignment)); - actions.push(Action::new(guard, op)); + actions.push(Action::new(pg.true_id(), op)); +} + +fn known_expr( + pg: &ProtoGraph, + parameter: ParameterState, + facts: &FxHashMap, +) -> ExprRef { + match facts[¶meter.expr] { + Knownness::Unknown => pg.false_id(), + Knownness::Known => pg.true_id(), + Knownness::Maybe => parameter.known_expr.unwrap(), + } } -fn push_assert( +fn push_known_update( pg: &mut ProtoGraph, actions: &mut Vec, guard: ExprRef, - lhs: ExprRef, - rhs: ExprRef, + parameter: ParameterState, ) { - let op = pg.o(Op::AssertEq(lhs, rhs)); - actions.push(Action::new(guard, op)); + if let Some(symbol) = parameter.known_symbol { + push_assign(pg, actions, guard, symbol, pg.true_id()); + } } -fn push_internal_assert_false(pg: &mut ProtoGraph, actions: &mut Vec, guard: ExprRef) { - let op = pg.o(Op::InternalAssertFalse); - actions.push(Action::new(guard, op)); +fn push_candidate_failure( + pg: &mut ProtoGraph, + actions: &mut Vec, + active: ExprRef, + live_symbol: SymbolId, + lhs: ExprRef, + rhs: ExprRef, +) { + let equal = pg.expr_ctx.equal(lhs, rhs); + let mismatch = pg.not_guard(equal); + let guard = pg.and_guard(active, mismatch); + push_assign(pg, actions, guard, live_symbol, pg.false_id()); } -/// Turn one equality into explicit learn/check actions. -/// -/// A whole unknown parameter may be assigned from the other, fully-known side. -/// Once every referenced parameter is known, the equality is checked normally. -/// Any active case requiring partial or relational inference becomes an explicit -/// internal assertion failure in the monitor graph. -fn lower_equality( +fn lower_candidate_equality( pg: &mut ProtoGraph, actions: &mut Vec, active: ExprRef, lhs: ExprRef, rhs: ExprRef, + live_symbol: SymbolId, parameters: &FxHashMap, + facts: &FxHashMap, ) { + if matches!(check_sat(pg, active), SatResult::DefinitelyUnsat) { + return; + } + let lhs_parameters = parameters_in_expr(pg, lhs, parameters); let rhs_parameters = parameters_in_expr(pg, rhs, parameters); let mut all_parameters = lhs_parameters.clone(); @@ -219,132 +300,469 @@ fn lower_equality( } } - if all_parameters.is_empty() { - push_assert(pg, actions, active, lhs, rhs); + if all_parameters.is_empty() + || all_parameters + .iter() + .all(|parameter| facts[¶meter.expr] == Knownness::Known) + { + push_candidate_failure(pg, actions, active, live_symbol, lhs, rhs); + return; + } + + if let Some(parameter) = parameters.get(&lhs).copied() + && facts[¶meter.expr] == Knownness::Unknown + && rhs_parameters + .iter() + .all(|other| facts[&other.expr] == Knownness::Known) + { + push_assign(pg, actions, active, parameter.symbol, rhs); + push_known_update(pg, actions, active, parameter); + return; + } + if let Some(parameter) = parameters.get(&rhs).copied() + && facts[¶meter.expr] == Knownness::Unknown + && lhs_parameters + .iter() + .all(|other| facts[&other.expr] == Knownness::Known) + { + push_assign(pg, actions, active, parameter.symbol, lhs); + push_known_update(pg, actions, active, parameter); return; } let all_known = and_all( pg, - all_parameters.iter().map(|parameter| parameter.known_expr), + all_parameters + .iter() + .map(|parameter| known_expr(pg, *parameter, facts)) + .collect::>(), ); let check_guard = pg.and_guard(active, all_known); - push_assert(pg, actions, check_guard, lhs, rhs); + push_candidate_failure(pg, actions, check_guard, live_symbol, lhs, rhs); let mut handled = all_known; if let Some(parameter) = parameters.get(&lhs).copied() { - let rhs_known = and_all(pg, rhs_parameters.iter().map(|other| other.known_expr)); - let lhs_unknown = pg.not_guard(parameter.known_expr); + let rhs_known = and_all( + pg, + rhs_parameters + .iter() + .map(|other| known_expr(pg, *other, facts)) + .collect::>(), + ); + let lhs_unknown = pg.not_guard(known_expr(pg, parameter, facts)); let can_bind = pg.and_guard(lhs_unknown, rhs_known); let bind_guard = pg.and_guard(active, can_bind); push_assign(pg, actions, bind_guard, parameter.symbol, rhs); - push_assign( - pg, - actions, - bind_guard, - parameter.known_symbol, - pg.true_id(), - ); + push_known_update(pg, actions, bind_guard, parameter); handled = pg.or_guard(handled, can_bind); } if let Some(parameter) = parameters.get(&rhs).copied() { - let lhs_known = and_all(pg, lhs_parameters.iter().map(|other| other.known_expr)); - let rhs_unknown = pg.not_guard(parameter.known_expr); + let lhs_known = and_all( + pg, + lhs_parameters + .iter() + .map(|other| known_expr(pg, *other, facts)) + .collect::>(), + ); + let rhs_unknown = pg.not_guard(known_expr(pg, parameter, facts)); let can_bind = pg.and_guard(rhs_unknown, lhs_known); let bind_guard = pg.and_guard(active, can_bind); push_assign(pg, actions, bind_guard, parameter.symbol, lhs); - push_assign( - pg, - actions, - bind_guard, - parameter.known_symbol, - pg.true_id(), - ); + push_known_update(pg, actions, bind_guard, parameter); handled = pg.or_guard(handled, can_bind); } - let unhandled = pg.not_guard(handled); - let unsupported_guard = pg.and_guard(active, unhandled); - push_internal_assert_false(pg, actions, unsupported_guard); + let unsupported = pg.not_guard(handled); + let unsupported = pg.and_guard(active, unsupported); + push_assign(pg, actions, unsupported, live_symbol, pg.false_id()); } -/// Convert a steady-state driver `ProtoGraph` into an explicit monitor graph. -/// -/// DUT assignments become equalities against observed DUT ports. Whole unknown -/// arguments are learned with guarded `Op::Assign` actions; later observations -/// are checked with guarded `Op::AssertEq` actions. The one-bank assumption is -/// reflected by sharing a monitor register for each argument expression. -pub fn to_monitor( - mut pg: ProtoGraph, +fn learn_equality_knownness( + pg: &mut ProtoGraph, + active: ExprRef, + lhs: ExprRef, + rhs: ExprRef, + parameters: &FxHashMap, + facts: &mut FxHashMap, +) { + let active_sat = check_sat(pg, active); + if matches!(active_sat, SatResult::DefinitelyUnsat) { + return; + } + + for (candidate, other) in [(lhs, rhs), (rhs, lhs)] { + if !parameters.contains_key(&candidate) { + continue; + } + let dependencies = parameters_in_expr(pg, other, parameters); + if dependencies + .iter() + .all(|dependency| facts[&dependency.expr] == Knownness::Known) + { + let learned = if matches!(active_sat, SatResult::AlwaysSat) { + Knownness::Known + } else { + Knownness::Maybe + }; + facts + .entry(candidate) + .and_modify(|knownness| { + if *knownness == Knownness::Unknown { + *knownness = learned; + } + }); + } + } +} + +fn allocate_protocol_seeds( + protos: &[Protocol], symbols: &mut SymbolTable, -) -> Result { - let parameter_states = create_parameter_states(&mut pg, symbols)?; - let parameters: FxHashMap = parameter_states +) -> Result, ToMonitorError> { + let mut seeds = Vec::with_capacity(protos.len()); + for protocol in protos { + let prefix = protocol.name.clone(); + let live_name = format!("{prefix}_live"); + let live_symbol = symbols.add_without_parent( + live_name.clone(), + Type::BitVec(1), + SymbolKind::MonitorState, + ); + let mut parameters = Vec::with_capacity(protocol.args.len()); + for argument in &protocol.args { + let original = argument.symbol(); + let Type::BitVec(width) = symbols[original].tpe() else { + return Err(ToMonitorError::NonBitVectorParameter( + symbols.full_name_from_symbol_id(&original), + )); + }; + let argument_name = symbols[original].name(); + let name = format!("{prefix}_{argument_name}"); + let known_name = format!("{name}_known"); + let symbol = symbols.add_without_parent( + name.clone(), + Type::BitVec(width), + SymbolKind::MonitorState, + ); + let known_symbol = symbols.add_without_parent( + known_name.clone(), + Type::BitVec(1), + SymbolKind::MonitorState, + ); + parameters.push(ParameterSeed { + original, + symbol, + known_symbol, + name, + known_name, + width, + }); + } + seeds.push(ProtocolSeed { + live_symbol, + live_name, + parameters, + }); + } + Ok(seeds) +} + +fn instantiate_candidate( + lowerer: &mut Lowerer<'_>, + protocol: &Protocol, + seed: &ProtocolSeed, +) -> (LoweredFragmentInfo, CandidateState) { + let prototype = lowerer.lower_protocol_fragment(protocol, false, true); + let mut substitutions = FxHashMap::default(); + let mut parameters = Vec::with_capacity(seed.parameters.len()); + + for parameter in &seed.parameters { + let expr = lowerer + .ir + .expr_ctx + .bv_symbol(¶meter.name, parameter.width); + lowerer.ir.cache_symbol_expr(parameter.symbol, expr); + lowerer.ir.state_init.insert( + parameter.symbol, + lowerer.ir.expr_ctx.bit_vec_val(0, parameter.width), + ); + if let Some(original_expr) = lowerer.ir.symbol_expr(parameter.original) { + substitutions.insert(original_expr, expr); + } + parameters.push(ParameterState { + symbol: parameter.symbol, + expr, + known_symbol: None, + known_expr: None, + }); + } + + let live_expr = lowerer.ir.expr_ctx.bv_symbol(&seed.live_name, 1); + lowerer.ir.cache_symbol_expr(seed.live_symbol, live_expr); + lowerer + .ir + .state_init + .insert(seed.live_symbol, lowerer.ir.true_id()); + let fragment = lowerer.copy_protocol_fragment(prototype, &substitutions); + ( + fragment, + CandidateState { + live_symbol: seed.live_symbol, + live_expr, + parameters, + }, + ) +} + +fn transform_candidate_fragment( + pg: &mut ProtoGraph, + symbols: &SymbolTable, + fragment: &LoweredFragmentInfo, + seed: &ProtocolSeed, + candidate: &mut CandidateState, +) -> Result<(), ToMonitorError> { + for node_id in &fragment.nodes { + for action in pg[*node_id].actions.clone() { + if let Op::Assign(symbol, _) = pg[action.op] { + symbol_expr(pg, symbols, symbol)?; + } + } + } + + let mut parameters: FxHashMap = candidate + .parameters .iter() .map(|parameter| (parameter.expr, *parameter)) .collect(); - let node_ids: Vec<_> = pg.nodes().map(|(node, _)| node).collect(); + let facts = analyze_knownness(pg, fragment.entry, ¶meters); - for node_id in node_ids { - let old_actions = pg[node_id].actions.clone(); - let transitions = pg[node_id].transitions.clone(); - let mut new_actions = Vec::new(); + for (parameter, parameter_seed) in candidate.parameters.iter_mut().zip(&seed.parameters) { + if !facts + .values() + .any(|fact| fact.get(¶meter.expr) == Some(&Knownness::Maybe)) + { + continue; + } + let known_expr = pg.expr_ctx.bv_symbol(¶meter_seed.known_name, 1); + pg.cache_symbol_expr(parameter_seed.known_symbol, known_expr); + pg.state_init + .insert(parameter_seed.known_symbol, pg.false_id()); + parameter.known_symbol = Some(parameter_seed.known_symbol); + parameter.known_expr = Some(known_expr); + } + parameters = candidate + .parameters + .iter() + .map(|parameter| (parameter.expr, *parameter)) + .collect(); + for node_id in facts.keys().copied().collect::>() { + let node_active = if node_id == fragment.entry { + pg.true_id() + } else { + candidate.live_expr + }; + let old_actions = pg[node_id].actions.clone(); + let mut actions = Vec::new(); + let mut local_facts = facts[&node_id].clone(); for action in old_actions { match pg[action.op].clone() { Op::Assign(port, assignment) => { - let port_expr = symbol_expr(&mut pg, symbols, port)?; + let port_expr = symbol_expr(pg, symbols, port)?; for (assignment_guard, rhs) in assignment.concretes { let active = pg.and_guard(action.guard, assignment_guard); - lower_equality( - &mut pg, - &mut new_actions, + let active = pg.and_guard(node_active, active); + lower_candidate_equality( + pg, + &mut actions, + active, + port_expr, + rhs, + candidate.live_symbol, + ¶meters, + &local_facts, + ); + learn_equality_knownness( + pg, active, port_expr, rhs, ¶meters, + &mut local_facts, ); } - // DontCare branches intentionally impose no monitor constraint. } - Op::AssertEq(lhs, rhs) => lower_equality( - &mut pg, - &mut new_actions, - action.guard, - lhs, - rhs, - ¶meters, - ), - Op::Fork if node_id == pg.entry => {} + Op::AssertEq(lhs, rhs) => { + let active = pg.and_guard(node_active, action.guard); + lower_candidate_equality( + pg, + &mut actions, + active, + lhs, + rhs, + candidate.live_symbol, + ¶meters, + &local_facts, + ); + learn_equality_knownness( + pg, + active, + lhs, + rhs, + ¶meters, + &mut local_facts, + ); + } Op::Fork => return Err(ToMonitorError::UnsupportedFork), - Op::InternalAssertFalse | Op::Done => new_actions.push(action), + Op::InternalAssertFalse | Op::Done => { + let guard = pg.and_guard(node_active, action.guard); + actions.push(action.with_guard(guard)); + } } } - // A steady-state back-edge starts a fresh transaction. Clear all - // knownness registers on the same edge that returns to the entry. - let entry = pg.entry; - let false_id = pg.false_id(); - for transition in transitions + let transitions = pg[node_id].transitions.clone(); + let transition_guards: Vec<_> = transitions .iter() - .filter(|transition| transition.target == entry) + .map(|transition| pg.expr_ctx.and(candidate.live_expr, transition.guard)) + .collect(); + pg.node_mut(node_id).actions = actions; + for (transition, guard) in pg + .node_mut(node_id) + .transitions + .iter_mut() + .zip(transition_guards) { - for parameter in ¶meter_states { - push_assign( - &mut pg, - &mut new_actions, - transition.guard, - parameter.known_symbol, - false_id, - ); + transition.guard = guard; + } + } + initialize_candidate_entry(pg, fragment.entry, candidate); + Ok(()) +} + +fn initialize_candidate_entry(pg: &mut ProtoGraph, entry: NodeId, candidate: &CandidateState) { + let old_actions = pg[entry].actions.clone(); + let mut actions = Vec::new(); + let mut live_kills = Vec::new(); + let known_symbols: FxHashSet<_> = candidate + .parameters + .iter() + .filter_map(|parameter| parameter.known_symbol) + .collect(); + let mut known_sets: FxHashMap> = FxHashMap::default(); + + for action in old_actions { + let Op::Assign(symbol, assignment) = pg[action.op].clone() else { + actions.push(action); + continue; + }; + if symbol != candidate.live_symbol && !known_symbols.contains(&symbol) { + actions.push(action); + continue; + } + for (branch_guard, rhs) in assignment.concretes { + let guard = pg.and_guard(action.guard, branch_guard); + if symbol == candidate.live_symbol && rhs == pg.false_id() { + live_kills.push(guard); + } else if known_symbols.contains(&symbol) && rhs == pg.true_id() { + known_sets.entry(symbol).or_default().push(guard); } } + } - pg.node_mut(node_id).actions = new_actions; + let kill = or_all(pg, live_kills); + let survives = pg.not_guard(kill); + let live_assignment = Assignment { + dont_care: pg.false_id(), + concretes: vec![(kill, pg.false_id()), (survives, pg.true_id())], + }; + let live_op = pg.o(Op::Assign(candidate.live_symbol, live_assignment)); + actions.push(Action::new(pg.true_id(), live_op)); + + for parameter in &candidate.parameters { + let Some(known_symbol) = parameter.known_symbol else { + continue; + }; + let set = or_all(pg, known_sets.remove(&known_symbol).unwrap_or_default()); + let clear = pg.not_guard(set); + let assignment = Assignment { + dont_care: pg.false_id(), + concretes: vec![(set, pg.true_id()), (clear, pg.false_id())], + }; + let op = pg.o(Op::Assign(known_symbol, assignment)); + actions.push(Action::new(pg.true_id(), op)); } + pg.node_mut(entry).actions = actions; +} - pg.simplify_all_exprs(); - Ok(pg) +fn loop_fragment_exit_to_entry( + pg: &mut ProtoGraph, + fragment: &LoweredFragmentInfo, + entry: NodeId, + live_expr: ExprRef, +) { + for node in fragment + .nodes + .iter() + .copied() + .filter(|node| *node != fragment.exit) + { + for transition in &mut pg.node_mut(node).transitions { + if transition.target == fragment.exit { + transition.target = entry; + transition.consumes_step = true; + } + } + if pg[node] + .transitions + .iter() + .any(|transition| transition.target == entry) + { + let done = pg.o(Op::Done); + pg.push_action(node, Action::new(live_expr, done)); + } + } +} + +/// Lower protocols directly into a deterministic steady-state monitor. +/// +/// Each protocol receives its own parameter bank and live bit. Observations +/// bind unknown parameters and eliminate only that protocol on a known-value +/// mismatch. The live protocol fragments are grafted together and subset +/// construction makes every surviving combination explicit. +pub fn to_monitor( + protos: Vec, + symbols: &mut SymbolTable, + expr_ctx: ExprContext, +) -> Result { + let Some(first) = protos.first() else { + return Err(ToMonitorError::EmptyProtocolSet); + }; + let seeds = allocate_protocol_seeds(&protos, symbols)?; + let mut lowerer = Lowerer::with_expr_ctx(first.ctx.clone(), symbols, expr_ctx); + let mut fragments = Vec::with_capacity(protos.len()); + let mut candidates = Vec::with_capacity(protos.len()); + + for (protocol, seed) in protos.iter().zip(&seeds) { + let (fragment, candidate) = instantiate_candidate(&mut lowerer, protocol, seed); + fragments.push(fragment); + candidates.push(candidate); + } + + for ((fragment, seed), candidate) in fragments.iter().zip(&seeds).zip(&mut candidates) { + transform_candidate_fragment(&mut lowerer.ir, lowerer.symbols, fragment, seed, candidate)?; + } + + let entry = lowerer.ir.entry; + for (fragment, candidate) in fragments.iter().zip(&candidates) { + loop_fragment_exit_to_entry(&mut lowerer.ir, fragment, entry, candidate.live_expr); + lowerer.graft_contracted_entry(entry, fragment.entry, lowerer.ir.true_id()); + } + + lowerer.ir.simplify_all_exprs(); + let mut monitor = determinized(lowerer.ir, symbols); + monitor.garbage_collect_unreachable(); + Ok(monitor) } #[cfg(test)] @@ -354,7 +772,6 @@ mod tests { use crate::frontend::diagnostic::DiagnosticHandler; use crate::frontend::require_single_module; use crate::ir::graphviz::to_dot_string; - use crate::ir::steady_state_lowering::lower_steady_state; use patronus::expr::Context as ExprContext; use std::fs; use tempfile::NamedTempFile; @@ -365,8 +782,7 @@ mod tests { let mut diagnostics = DiagnosticHandler::default(); let (mut symbols, modules) = frontend(&[file.path()], &mut diagnostics, true).unwrap(); let module = require_single_module(modules, &[file.path()]).unwrap(); - let (driver, _) = lower_steady_state(module.protos, &symbols, ExprContext::default()); - let monitor = to_monitor(driver, &mut symbols).unwrap(); + let monitor = to_monitor(module.protos, &mut symbols, ExprContext::default()).unwrap(); (monitor, symbols) } @@ -412,16 +828,16 @@ mod tests { } } - assert!(saw_argument_update); + assert!(!saw_argument_update); assert!(saw_knownness_update); - assert!(saw_monitor_assertion); + assert!(!saw_monitor_assertion); assert_eq!( monitor .state_init .keys() .filter(|symbol| symbols[**symbol].is_arg()) .count(), - 1 + 0 ); assert_eq!( monitor @@ -429,7 +845,7 @@ mod tests { .keys() .filter(|symbol| symbols[**symbol].is_monitor_state()) .count(), - 1 + 2 ); } @@ -462,9 +878,9 @@ mod tests { ); let serialized = to_dot_string(&monitor, &symbols); - println!("{serialized}"); - assert!(serialized.contains("__monitor_arg")); - assert!(serialized.contains("assert_eq")); + println!("{}", serialized); + assert!(!serialized.contains("proto_choice")); + assert!(serialized.contains("_live")); } #[test] @@ -474,13 +890,28 @@ mod tests { struct Device { in a: u32, in b: u32, + in op: u1, out s: u32, } prot add(a: u32, b: u32, s: u32) { dut.a := a; dut.b := b; + dut.op := 1'b0; + step(); + dut.a := X; + dut.b := X; + assert_eq(dut.s, s); + step(); + } + + prot sub(a: u32, b: u32, s: u32) { + dut.a := a; + dut.b := b; + dut.op := 1'b1; step(); + dut.a := X; + dut.b := X; assert_eq(dut.s, s); step(); } @@ -490,4 +921,41 @@ mod tests { let serialized = to_dot_string(&monitor, &symbols); println!("{serialized}"); } + + #[test] + fn serializes_wishbone_read_write_monitor() { + use crate::transaction_frontend; + use std::collections::HashSet; + + let protocol_file = "../examples/wishbone/wishbone.prot"; + let trace_file = "../examples/wishbone/read_write.tx"; + let mut diagnostics = DiagnosticHandler::default(); + let (mut symbols, modules) = + frontend(&[protocol_file], &mut diagnostics, true).unwrap(); + let module = require_single_module(modules, &[protocol_file]).unwrap(); + let traces = transaction_frontend( + trace_file, + &symbols, + &module.protos, + &mut diagnostics, + ) + .unwrap(); + let selected_names: HashSet<_> = traces[0] + .iter() + .map(|(name, _)| name.as_str()) + .collect(); + let selected = module + .protos + .into_iter() + .filter(|protocol| selected_names.contains(protocol.name.as_str())) + .collect(); + + let monitor = to_monitor(selected, &mut symbols, ExprContext::default()).unwrap(); + let serialized = to_dot_string(&monitor, &symbols); + let output = std::path::Path::new(env!("CARGO_MANIFEST_DIR")) + .join("../scripts/wishbone_read_write_monitor.dot"); + fs::write(output, &serialized).unwrap(); + // assert!(!serialized.contains("internal_assert_false")); + println!("{serialized}"); + } } diff --git a/scripts/wishbone_read_write_monitor.dot b/scripts/wishbone_read_write_monitor.dot new file mode 100644 index 00000000..e4704ac8 --- /dev/null +++ b/scripts/wishbone_read_write_monitor.dot @@ -0,0 +1,52 @@ +digraph "reset" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label="[1] reset_live := 0 if or(or(not(self.RST), self.CYC), self.STB); 1 if not(or(or(not(self.RST), self.CYC), self.STB))\n[or(or(or(reset_live, idle_no_cycle_live), write_live), read_live)] done\n[1] idle_no_cycle_live := 0 if or(self.RST, self.CYC); 1 if not(or(self.RST, self.CYC))\n[1] write_mask := 15 if 1\n[1] write_addr := self.ADR if 1\n[1] write_data := self.DAT_O if 1\n[1] write_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))))\n[1] read_mask := 15 if 1\n[1] read_data := self.DAT_I if self.ACK\n[1] read_addr := self.ADR if 1\n[1] read_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))))\n[1] read_data_known := 1 if self.ACK; 0 if not(self.ACK)"]; + node0 -> node0 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), not(and(read_live, not(self.ACK)))) / step"]; + node0 -> node1 [label="and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; + node0 -> node2 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; + node0 -> node3 [label="and(not(or(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; + node0 -> node4 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; + node0 -> node5 [label="and(and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), write_live), read_live), not(self.ACK)) / step"]; + node0 -> node6 [label="and(and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), write_live), read_live), not(self.ACK)) / step"]; + node1 [label="[1] write_live := 0 if or(or(or(or(or(or(or(and(write_live, self.RST), and(write_live, not(eq(self.ADR, write_addr)))), and(write_live, not(self.CYC))), and(write_live, not(eq(self.DAT_O, write_data)))), and(write_live, not(eq(self.SEL, write_mask)))), and(write_live, not(self.STB))), and(write_live, not(self.WE))), and(write_live, not(eq(self.CTI, 0))))\n[write_live] done"]; + node1 -> node0 [label="and(write_live, self.ACK) / step"]; + node1 -> node1 [label="and(write_live, not(self.ACK)) / step"]; + node2 [label="[1] reset_live := 0 if or(or(not(self.RST), self.CYC), self.STB); 1 if not(or(or(not(self.RST), self.CYC), self.STB))\n[or(or(or(reset_live, idle_no_cycle_live), write_live), read_live)] done\n[1] idle_no_cycle_live := 0 if or(self.RST, self.CYC); 1 if not(or(self.RST, self.CYC))\n[1] write_mask := 15 if 1\n[1] write_addr := self.ADR if 1\n[1] write_data := self.DAT_O if 1\n[1] write_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0)))); 0 if or(or(or(or(or(or(or(and(write_live, self.RST), and(write_live, not(eq(self.ADR, write_addr)))), and(write_live, not(self.CYC))), and(write_live, not(eq(self.DAT_O, write_data)))), and(write_live, not(eq(self.SEL, write_mask)))), and(write_live, not(self.STB))), and(write_live, not(self.WE))), and(write_live, not(eq(self.CTI, 0))))\n[1] read_mask := 15 if 1\n[1] read_data := self.DAT_I if self.ACK\n[1] read_addr := self.ADR if 1\n[1] read_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))))\n[1] read_data_known := 1 if self.ACK; 0 if not(self.ACK)\n[or(and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0)))), and(write_live, not(eq(self.ADR, write_addr)))), and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0)))), and(write_live, not(eq(self.DAT_O, write_data)))))] internal_assert_false"]; + node2 -> node0 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), not(and(read_live, not(self.ACK)))) / step"]; + node2 -> node1 [label="and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; + node2 -> node2 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; + node2 -> node3 [label="and(not(or(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; + node2 -> node4 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; + node2 -> node5 [label="and(and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), write_live), read_live), not(self.ACK)) / step"]; + node2 -> node6 [label="and(and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), write_live), read_live), not(self.ACK)) / step"]; + node3 [label="[1] read_live := 0 if or(or(or(or(or(or(or(and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))), and(read_live, self.RST)), and(read_live, not(eq(self.ADR, read_addr)))), and(read_live, not(self.CYC))), and(read_live, not(eq(self.SEL, read_mask)))), and(read_live, not(self.STB))), and(read_live, self.WE)), and(read_live, not(eq(self.CTI, 0))))\n[1] read_data := self.DAT_I if and(and(read_live, self.ACK), not(read_data_known))\n[1] read_data_known := 1 if and(and(read_live, self.ACK), not(read_data_known))\n[read_live] done"]; + node3 -> node0 [label="and(read_live, self.ACK) / step"]; + node3 -> node3 [label="and(read_live, not(self.ACK)) / step"]; + node4 [label="[1] reset_live := 0 if or(or(not(self.RST), self.CYC), self.STB); 1 if not(or(or(not(self.RST), self.CYC), self.STB))\n[or(or(or(reset_live, idle_no_cycle_live), write_live), read_live)] done\n[1] idle_no_cycle_live := 0 if or(self.RST, self.CYC); 1 if not(or(self.RST, self.CYC))\n[1] write_mask := 15 if 1\n[1] write_addr := self.ADR if 1\n[1] write_data := self.DAT_O if 1\n[1] write_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))))\n[1] read_mask := 15 if 1\n[1] read_data := self.DAT_I if self.ACK\n[1] read_addr := self.ADR if 1\n[1] read_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0)))); 0 if or(or(or(or(or(or(or(and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))), and(read_live, self.RST)), and(read_live, not(eq(self.ADR, read_addr)))), and(read_live, not(self.CYC))), and(read_live, not(eq(self.SEL, read_mask)))), and(read_live, not(self.STB))), and(read_live, self.WE)), and(read_live, not(eq(self.CTI, 0))))\n[1] read_data_known := 1 if self.ACK; 0 if not(self.ACK); 1 if and(and(read_live, self.ACK), not(read_data_known))\n[or(and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0)))), and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data)))), and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0)))), and(read_live, not(eq(self.ADR, read_addr)))))] internal_assert_false"]; + node4 -> node0 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), not(and(read_live, not(self.ACK)))) / step"]; + node4 -> node1 [label="and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; + node4 -> node2 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; + node4 -> node3 [label="and(not(or(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; + node4 -> node4 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; + node4 -> node5 [label="and(and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), write_live), read_live), not(self.ACK)) / step"]; + node4 -> node6 [label="and(and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), write_live), read_live), not(self.ACK)) / step"]; + node5 [label="[1] write_live := 0 if or(or(or(or(or(or(or(and(write_live, self.RST), and(write_live, not(eq(self.ADR, write_addr)))), and(write_live, not(self.CYC))), and(write_live, not(eq(self.DAT_O, write_data)))), and(write_live, not(eq(self.SEL, write_mask)))), and(write_live, not(self.STB))), and(write_live, not(self.WE))), and(write_live, not(eq(self.CTI, 0))))\n[or(write_live, read_live)] done\n[1] read_live := 0 if or(or(or(or(or(or(or(and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))), and(read_live, self.RST)), and(read_live, not(eq(self.ADR, read_addr)))), and(read_live, not(self.CYC))), and(read_live, not(eq(self.SEL, read_mask)))), and(read_live, not(self.STB))), and(read_live, self.WE)), and(read_live, not(eq(self.CTI, 0))))\n[1] read_data := self.DAT_I if and(and(read_live, self.ACK), not(read_data_known))\n[1] read_data_known := 1 if and(and(read_live, self.ACK), not(read_data_known))"]; + node5 -> node0 [label="and(and(or(and(write_live, self.ACK), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), not(and(read_live, not(self.ACK)))) / step"]; + node5 -> node1 [label="and(and(not(or(and(write_live, self.ACK), and(read_live, self.ACK))), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; + node5 -> node2 [label="and(and(or(and(write_live, self.ACK), and(read_live, self.ACK)), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; + node5 -> node3 [label="and(not(or(or(and(write_live, self.ACK), and(read_live, self.ACK)), and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; + node5 -> node4 [label="and(and(or(and(write_live, self.ACK), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; + node5 -> node5 [label="and(and(and(not(or(and(write_live, self.ACK), and(read_live, self.ACK))), write_live), read_live), not(self.ACK)) / step"]; + node5 -> node6 [label="and(and(and(or(and(write_live, self.ACK), and(read_live, self.ACK)), write_live), read_live), not(self.ACK)) / step"]; + node6 [label="[1] reset_live := 0 if or(or(not(self.RST), self.CYC), self.STB); 1 if not(or(or(not(self.RST), self.CYC), self.STB))\n[or(or(or(reset_live, idle_no_cycle_live), write_live), read_live)] done\n[1] idle_no_cycle_live := 0 if or(self.RST, self.CYC); 1 if not(or(self.RST, self.CYC))\n[1] write_mask := 15 if 1\n[1] write_addr := self.ADR if 1\n[1] write_data := self.DAT_O if 1\n[1] write_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0)))); 0 if or(or(or(or(or(or(or(and(write_live, self.RST), and(write_live, not(eq(self.ADR, write_addr)))), and(write_live, not(self.CYC))), and(write_live, not(eq(self.DAT_O, write_data)))), and(write_live, not(eq(self.SEL, write_mask)))), and(write_live, not(self.STB))), and(write_live, not(self.WE))), and(write_live, not(eq(self.CTI, 0))))\n[1] read_mask := 15 if 1\n[1] read_data := self.DAT_I if self.ACK\n[1] read_addr := self.ADR if 1\n[1] read_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0)))); 0 if or(or(or(or(or(or(or(and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))), and(read_live, self.RST)), and(read_live, not(eq(self.ADR, read_addr)))), and(read_live, not(self.CYC))), and(read_live, not(eq(self.SEL, read_mask)))), and(read_live, not(self.STB))), and(read_live, self.WE)), and(read_live, not(eq(self.CTI, 0))))\n[1] read_data_known := 1 if self.ACK; 0 if not(self.ACK); 1 if and(and(read_live, self.ACK), not(read_data_known))\n[or(or(or(and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0)))), and(write_live, not(eq(self.ADR, write_addr)))), and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0)))), and(write_live, not(eq(self.DAT_O, write_data))))), and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0)))), and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))))), and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0)))), and(read_live, not(eq(self.ADR, read_addr)))))] internal_assert_false"]; + node6 -> node0 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), not(and(read_live, not(self.ACK)))) / step"]; + node6 -> node1 [label="and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; + node6 -> node2 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; + node6 -> node3 [label="and(not(or(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; + node6 -> node4 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; + node6 -> node5 [label="and(and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), write_live), read_live), not(self.ACK)) / step"]; + node6 -> node6 [label="and(and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), write_live), read_live), not(self.ACK)) / step"]; +} From 0cd2afca8a845474a16d597b066887c5e357a8c8 Mon Sep 17 00:00:00 2001 From: Nikil Shyamsunder Date: Mon, 3 Aug 2026 16:00:34 -0400 Subject: [PATCH 6/7] simplify the guards to prune edges --- protocols/src/ir/determinize.rs | 149 ++++++++++++++++++++++-- protocols/src/ir/to_monitor.rs | 2 +- scripts/wishbone_read_write_monitor.dot | 48 +------- 3 files changed, 144 insertions(+), 55 deletions(-) diff --git a/protocols/src/ir/determinize.rs b/protocols/src/ir/determinize.rs index 2e30cb30..8392a2ab 100644 --- a/protocols/src/ir/determinize.rs +++ b/protocols/src/ir/determinize.rs @@ -8,8 +8,8 @@ use crate::frontend::symbol::SymbolTable; use crate::ir::edge_contract::append_action; use crate::ir::proto_graph::{Node as NFANode, NodeId, ProtoGraph, Transition}; use cranelift_entity::PrimaryMap; -use patronus::expr::ExprRef; -use rustc_hash::FxHashMap; +use patronus::expr::{Expr, ExprRef, TypeCheck, simple_transform_expr}; +use rustc_hash::{FxHashMap, FxHashSet}; /// A DFA Node is a set of NFA nodes active at the same time. type DFANode = BTreeSet; @@ -39,6 +39,68 @@ pub enum SatResult { AlwaysSat, } +fn collect_boolean_atoms(protocol: &ProtoGraph, expr: ExprRef, atoms: &mut FxHashSet) { + if expr == protocol.true_id() || expr == protocol.false_id() { + return; + } + match protocol.expr_ctx[expr] { + Expr::BVAnd(lhs, rhs, 1) | Expr::BVOr(lhs, rhs, 1) => { + collect_boolean_atoms(protocol, lhs, atoms); + collect_boolean_atoms(protocol, rhs, atoms); + } + Expr::BVNot(inner, 1) => collect_boolean_atoms(protocol, inner, atoms), + _ => { + atoms.insert(expr); + } + } +} + +fn eval_boolean_skeleton( + protocol: &ProtoGraph, + expr: ExprRef, + values: &FxHashMap, +) -> bool { + if expr == protocol.true_id() { + return true; + } + if expr == protocol.false_id() { + return false; + } + match protocol.expr_ctx[expr] { + Expr::BVAnd(lhs, rhs, 1) => { + eval_boolean_skeleton(protocol, lhs, values) + && eval_boolean_skeleton(protocol, rhs, values) + } + Expr::BVOr(lhs, rhs, 1) => { + eval_boolean_skeleton(protocol, lhs, values) + || eval_boolean_skeleton(protocol, rhs, values) + } + Expr::BVNot(inner, 1) => !eval_boolean_skeleton(protocol, inner, values), + _ => values[&expr], + } +} + +fn propositionally_unsat(protocol: &ProtoGraph, expr: ExprRef) -> bool { + let mut atoms = FxHashSet::default(); + collect_boolean_atoms(protocol, expr, &mut atoms); + // Keep this lightweight. Falling back to MaybeSat is always sound. + if atoms.len() > 16 { + return false; + } + let atoms: Vec<_> = atoms.into_iter().collect(); + for mask in 0usize..(1usize << atoms.len()) { + let values = atoms + .iter() + .enumerate() + .map(|(index, atom)| (*atom, (mask >> index) & 1 == 1)) + .collect(); + if eval_boolean_skeleton(protocol, expr, &values) { + return false; + } + } + true +} + // TODO: Strengthen this with a real SAT/SMT query to prune more aggressively. pub fn check_sat(protocol: &mut ProtoGraph, guard: ExprRef) -> SatResult { let simplified = { @@ -50,11 +112,69 @@ pub fn check_sat(protocol: &mut ProtoGraph, guard: ExprRef) -> SatResult { SatResult::DefinitelyUnsat } else if simplified == protocol.true_id() { SatResult::AlwaysSat + } else if propositionally_unsat(protocol, simplified) { + SatResult::DefinitelyUnsat } else { - SatResult::MaybeSat + let negated = protocol.not_guard(simplified); + if propositionally_unsat(protocol, negated) { + SatResult::AlwaysSat + } else { + SatResult::MaybeSat + } } } +fn transition_guards_after_node_updates( + protocol: &mut ProtoGraph, + actions: &[crate::ir::proto_graph::Action], + transitions: &[Transition], +) -> Vec { + let mut substitutions = FxHashMap::default(); + + for action in actions { + let crate::ir::proto_graph::Op::Assign(symbol, assignment) = + protocol[action.op].clone() + else { + continue; + }; + if !protocol.state_init.contains_key(&symbol) + || assignment.dont_care != protocol.false_id() + { + continue; + } + let Some(lhs) = protocol.symbol_expr(symbol) else { + continue; + }; + if !lhs.is_bool(&protocol.expr_ctx) { + continue; + } + + // Assignment branches use first-match priority. If no branch fires, + // monitor state holds its old value. + let mut next = lhs; + for (branch_guard, rhs) in assignment.concretes.iter().rev() { + let guard = protocol.and_guard(action.guard, *branch_guard); + let when_set = protocol.and_guard(guard, *rhs); + let not_guard = protocol.not_guard(guard); + let when_held = protocol.and_guard(not_guard, next); + next = protocol.or_guard(when_set, when_held); + } + substitutions.insert(lhs, next); + } + + transitions + .iter() + .map(|transition| { + let guard = simple_transform_expr( + &mut protocol.expr_ctx, + transition.guard, + |_ctx, candidate, _children| substitutions.get(&candidate).copied(), + ); + protocol.simplifier.simplify(&mut protocol.expr_ctx, guard) + }) + .collect() +} + /// Perform subset construction. pub fn determinized(protocol: ProtoGraph, symbols: &SymbolTable) -> ProtoGraph { let mut protocol = protocol.clone(); @@ -133,11 +253,12 @@ pub fn determinized(protocol: ProtoGraph, symbols: &SymbolTable) -> ProtoGraph { let mut new_trans: Vec = Vec::new(); let n = transitions.len(); - let transition_guards: Vec<_> = transitions.iter().map(|t| t.guard).collect(); + let analysis_guards = + transition_guards_after_node_updates(&mut protocol, &actions, &transitions); let mut mutually_exclusive = vec![vec![false; n]; n]; for i in 0..n { for j in (i + 1)..n { - let overlap = protocol.and_guard(transition_guards[i], transition_guards[j]); + let overlap = protocol.and_guard(analysis_guards[i], analysis_guards[j]); let disjoint = matches!( check_sat(&mut protocol, overlap), SatResult::DefinitelyUnsat @@ -152,27 +273,31 @@ pub fn determinized(protocol: ProtoGraph, symbols: &SymbolTable) -> ProtoGraph { assert!(n <= 128); for mask in 1u128..(1u128 << n) { let mut guard = protocol.true_id(); + let mut analysis_guard = protocol.true_id(); let mut targets: DFANode = BTreeSet::new(); for (i, t) in transitions.iter().enumerate() { let selected = (mask >> i) & 1 == 1; - let lit = if selected { + let (lit, analysis_lit) = if selected { targets.insert(t.target); - t.guard + (t.guard, analysis_guards[i]) } else if (0..n).any(|j| (mask >> j) & 1 == 1 && mutually_exclusive[i][j]) { // A selected transition already implies that this guard is // false, so its negation would only add expression noise. continue; } else { - protocol.not_guard(t.guard) + ( + protocol.not_guard(t.guard), + protocol.not_guard(analysis_guards[i]), + ) }; guard = protocol.and_guard(guard, lit); + analysis_guard = protocol.and_guard(analysis_guard, analysis_lit); } - let guard = match check_sat(&mut protocol, guard) { + match check_sat(&mut protocol, analysis_guard) { SatResult::DefinitelyUnsat => continue, - SatResult::AlwaysSat => protocol.true_id(), - SatResult::MaybeSat => guard, - }; + SatResult::AlwaysSat | SatResult::MaybeSat => {} + } let target_id = get_or_create_state(targets, &mut state_ids, &mut worklist, &mut new_nodes); diff --git a/protocols/src/ir/to_monitor.rs b/protocols/src/ir/to_monitor.rs index 7bdfc252..db480e93 100644 --- a/protocols/src/ir/to_monitor.rs +++ b/protocols/src/ir/to_monitor.rs @@ -955,7 +955,7 @@ mod tests { let output = std::path::Path::new(env!("CARGO_MANIFEST_DIR")) .join("../scripts/wishbone_read_write_monitor.dot"); fs::write(output, &serialized).unwrap(); - // assert!(!serialized.contains("internal_assert_false")); + assert!(!serialized.contains("internal_assert_false")); println!("{serialized}"); } } diff --git a/scripts/wishbone_read_write_monitor.dot b/scripts/wishbone_read_write_monitor.dot index e4704ac8..b39ca421 100644 --- a/scripts/wishbone_read_write_monitor.dot +++ b/scripts/wishbone_read_write_monitor.dot @@ -4,49 +4,13 @@ digraph "reset" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label="[1] reset_live := 0 if or(or(not(self.RST), self.CYC), self.STB); 1 if not(or(or(not(self.RST), self.CYC), self.STB))\n[or(or(or(reset_live, idle_no_cycle_live), write_live), read_live)] done\n[1] idle_no_cycle_live := 0 if or(self.RST, self.CYC); 1 if not(or(self.RST, self.CYC))\n[1] write_mask := 15 if 1\n[1] write_addr := self.ADR if 1\n[1] write_data := self.DAT_O if 1\n[1] write_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))))\n[1] read_mask := 15 if 1\n[1] read_data := self.DAT_I if self.ACK\n[1] read_addr := self.ADR if 1\n[1] read_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))))\n[1] read_data_known := 1 if self.ACK; 0 if not(self.ACK)"]; - node0 -> node0 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), not(and(read_live, not(self.ACK)))) / step"]; - node0 -> node1 [label="and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; - node0 -> node2 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; - node0 -> node3 [label="and(not(or(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; - node0 -> node4 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; - node0 -> node5 [label="and(and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), write_live), read_live), not(self.ACK)) / step"]; - node0 -> node6 [label="and(and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), write_live), read_live), not(self.ACK)) / step"]; + node0 -> node0 [label="or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)) / step"]; + node0 -> node1 [label="and(write_live, not(self.ACK)) / step"]; + node0 -> node2 [label="and(read_live, not(self.ACK)) / step"]; node1 [label="[1] write_live := 0 if or(or(or(or(or(or(or(and(write_live, self.RST), and(write_live, not(eq(self.ADR, write_addr)))), and(write_live, not(self.CYC))), and(write_live, not(eq(self.DAT_O, write_data)))), and(write_live, not(eq(self.SEL, write_mask)))), and(write_live, not(self.STB))), and(write_live, not(self.WE))), and(write_live, not(eq(self.CTI, 0))))\n[write_live] done"]; node1 -> node0 [label="and(write_live, self.ACK) / step"]; node1 -> node1 [label="and(write_live, not(self.ACK)) / step"]; - node2 [label="[1] reset_live := 0 if or(or(not(self.RST), self.CYC), self.STB); 1 if not(or(or(not(self.RST), self.CYC), self.STB))\n[or(or(or(reset_live, idle_no_cycle_live), write_live), read_live)] done\n[1] idle_no_cycle_live := 0 if or(self.RST, self.CYC); 1 if not(or(self.RST, self.CYC))\n[1] write_mask := 15 if 1\n[1] write_addr := self.ADR if 1\n[1] write_data := self.DAT_O if 1\n[1] write_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0)))); 0 if or(or(or(or(or(or(or(and(write_live, self.RST), and(write_live, not(eq(self.ADR, write_addr)))), and(write_live, not(self.CYC))), and(write_live, not(eq(self.DAT_O, write_data)))), and(write_live, not(eq(self.SEL, write_mask)))), and(write_live, not(self.STB))), and(write_live, not(self.WE))), and(write_live, not(eq(self.CTI, 0))))\n[1] read_mask := 15 if 1\n[1] read_data := self.DAT_I if self.ACK\n[1] read_addr := self.ADR if 1\n[1] read_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))))\n[1] read_data_known := 1 if self.ACK; 0 if not(self.ACK)\n[or(and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0)))), and(write_live, not(eq(self.ADR, write_addr)))), and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0)))), and(write_live, not(eq(self.DAT_O, write_data)))))] internal_assert_false"]; - node2 -> node0 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), not(and(read_live, not(self.ACK)))) / step"]; - node2 -> node1 [label="and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; - node2 -> node2 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; - node2 -> node3 [label="and(not(or(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; - node2 -> node4 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; - node2 -> node5 [label="and(and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), write_live), read_live), not(self.ACK)) / step"]; - node2 -> node6 [label="and(and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), write_live), read_live), not(self.ACK)) / step"]; - node3 [label="[1] read_live := 0 if or(or(or(or(or(or(or(and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))), and(read_live, self.RST)), and(read_live, not(eq(self.ADR, read_addr)))), and(read_live, not(self.CYC))), and(read_live, not(eq(self.SEL, read_mask)))), and(read_live, not(self.STB))), and(read_live, self.WE)), and(read_live, not(eq(self.CTI, 0))))\n[1] read_data := self.DAT_I if and(and(read_live, self.ACK), not(read_data_known))\n[1] read_data_known := 1 if and(and(read_live, self.ACK), not(read_data_known))\n[read_live] done"]; - node3 -> node0 [label="and(read_live, self.ACK) / step"]; - node3 -> node3 [label="and(read_live, not(self.ACK)) / step"]; - node4 [label="[1] reset_live := 0 if or(or(not(self.RST), self.CYC), self.STB); 1 if not(or(or(not(self.RST), self.CYC), self.STB))\n[or(or(or(reset_live, idle_no_cycle_live), write_live), read_live)] done\n[1] idle_no_cycle_live := 0 if or(self.RST, self.CYC); 1 if not(or(self.RST, self.CYC))\n[1] write_mask := 15 if 1\n[1] write_addr := self.ADR if 1\n[1] write_data := self.DAT_O if 1\n[1] write_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))))\n[1] read_mask := 15 if 1\n[1] read_data := self.DAT_I if self.ACK\n[1] read_addr := self.ADR if 1\n[1] read_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0)))); 0 if or(or(or(or(or(or(or(and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))), and(read_live, self.RST)), and(read_live, not(eq(self.ADR, read_addr)))), and(read_live, not(self.CYC))), and(read_live, not(eq(self.SEL, read_mask)))), and(read_live, not(self.STB))), and(read_live, self.WE)), and(read_live, not(eq(self.CTI, 0))))\n[1] read_data_known := 1 if self.ACK; 0 if not(self.ACK); 1 if and(and(read_live, self.ACK), not(read_data_known))\n[or(and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0)))), and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data)))), and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0)))), and(read_live, not(eq(self.ADR, read_addr)))))] internal_assert_false"]; - node4 -> node0 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), not(and(read_live, not(self.ACK)))) / step"]; - node4 -> node1 [label="and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; - node4 -> node2 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; - node4 -> node3 [label="and(not(or(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; - node4 -> node4 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; - node4 -> node5 [label="and(and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), write_live), read_live), not(self.ACK)) / step"]; - node4 -> node6 [label="and(and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), write_live), read_live), not(self.ACK)) / step"]; - node5 [label="[1] write_live := 0 if or(or(or(or(or(or(or(and(write_live, self.RST), and(write_live, not(eq(self.ADR, write_addr)))), and(write_live, not(self.CYC))), and(write_live, not(eq(self.DAT_O, write_data)))), and(write_live, not(eq(self.SEL, write_mask)))), and(write_live, not(self.STB))), and(write_live, not(self.WE))), and(write_live, not(eq(self.CTI, 0))))\n[or(write_live, read_live)] done\n[1] read_live := 0 if or(or(or(or(or(or(or(and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))), and(read_live, self.RST)), and(read_live, not(eq(self.ADR, read_addr)))), and(read_live, not(self.CYC))), and(read_live, not(eq(self.SEL, read_mask)))), and(read_live, not(self.STB))), and(read_live, self.WE)), and(read_live, not(eq(self.CTI, 0))))\n[1] read_data := self.DAT_I if and(and(read_live, self.ACK), not(read_data_known))\n[1] read_data_known := 1 if and(and(read_live, self.ACK), not(read_data_known))"]; - node5 -> node0 [label="and(and(or(and(write_live, self.ACK), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), not(and(read_live, not(self.ACK)))) / step"]; - node5 -> node1 [label="and(and(not(or(and(write_live, self.ACK), and(read_live, self.ACK))), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; - node5 -> node2 [label="and(and(or(and(write_live, self.ACK), and(read_live, self.ACK)), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; - node5 -> node3 [label="and(not(or(or(and(write_live, self.ACK), and(read_live, self.ACK)), and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; - node5 -> node4 [label="and(and(or(and(write_live, self.ACK), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; - node5 -> node5 [label="and(and(and(not(or(and(write_live, self.ACK), and(read_live, self.ACK))), write_live), read_live), not(self.ACK)) / step"]; - node5 -> node6 [label="and(and(and(or(and(write_live, self.ACK), and(read_live, self.ACK)), write_live), read_live), not(self.ACK)) / step"]; - node6 [label="[1] reset_live := 0 if or(or(not(self.RST), self.CYC), self.STB); 1 if not(or(or(not(self.RST), self.CYC), self.STB))\n[or(or(or(reset_live, idle_no_cycle_live), write_live), read_live)] done\n[1] idle_no_cycle_live := 0 if or(self.RST, self.CYC); 1 if not(or(self.RST, self.CYC))\n[1] write_mask := 15 if 1\n[1] write_addr := self.ADR if 1\n[1] write_data := self.DAT_O if 1\n[1] write_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0)))); 0 if or(or(or(or(or(or(or(and(write_live, self.RST), and(write_live, not(eq(self.ADR, write_addr)))), and(write_live, not(self.CYC))), and(write_live, not(eq(self.DAT_O, write_data)))), and(write_live, not(eq(self.SEL, write_mask)))), and(write_live, not(self.STB))), and(write_live, not(self.WE))), and(write_live, not(eq(self.CTI, 0))))\n[1] read_mask := 15 if 1\n[1] read_data := self.DAT_I if self.ACK\n[1] read_addr := self.ADR if 1\n[1] read_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0)))); 0 if or(or(or(or(or(or(or(and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))), and(read_live, self.RST)), and(read_live, not(eq(self.ADR, read_addr)))), and(read_live, not(self.CYC))), and(read_live, not(eq(self.SEL, read_mask)))), and(read_live, not(self.STB))), and(read_live, self.WE)), and(read_live, not(eq(self.CTI, 0))))\n[1] read_data_known := 1 if self.ACK; 0 if not(self.ACK); 1 if and(and(read_live, self.ACK), not(read_data_known))\n[or(or(or(and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0)))), and(write_live, not(eq(self.ADR, write_addr)))), and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0)))), and(write_live, not(eq(self.DAT_O, write_data))))), and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0)))), and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))))), and(not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0)))), and(read_live, not(eq(self.ADR, read_addr)))))] internal_assert_false"]; - node6 -> node0 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), not(and(read_live, not(self.ACK)))) / step"]; - node6 -> node1 [label="and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; - node6 -> node2 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK))), not(and(read_live, not(self.ACK)))) / step"]; - node6 -> node3 [label="and(not(or(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; - node6 -> node4 [label="and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), not(and(write_live, not(self.ACK)))), and(read_live, not(self.ACK))) / step"]; - node6 -> node5 [label="and(and(and(not(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK))), write_live), read_live), not(self.ACK)) / step"]; - node6 -> node6 [label="and(and(and(or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)), write_live), read_live), not(self.ACK)) / step"]; + node2 [label="[1] read_live := 0 if or(or(or(or(or(or(or(and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))), and(read_live, self.RST)), and(read_live, not(eq(self.ADR, read_addr)))), and(read_live, not(self.CYC))), and(read_live, not(eq(self.SEL, read_mask)))), and(read_live, not(self.STB))), and(read_live, self.WE)), and(read_live, not(eq(self.CTI, 0))))\n[1] read_data := self.DAT_I if and(and(read_live, self.ACK), not(read_data_known))\n[1] read_data_known := 1 if and(and(read_live, self.ACK), not(read_data_known))\n[read_live] done"]; + node2 -> node0 [label="and(read_live, self.ACK) / step"]; + node2 -> node2 [label="and(read_live, not(self.ACK)) / step"]; } From 55fcb1dfbc5dcfe05cbe8f27f24e2e0036cd0572 Mon Sep 17 00:00:00 2001 From: Nikil Shyamsunder Date: Mon, 3 Aug 2026 16:09:45 -0400 Subject: [PATCH 7/7] lower to monitor teansition system --- examples/wishbone/read_write.tx | 2 - examples/wishbone/wishbone_fv.prot | 564 ++++++++++++++++++++ protocols/src/backends/transition_system.rs | 400 ++++++++++++++ protocols/src/ir/determinize.rs | 57 +- protocols/src/ir/to_monitor.rs | 50 +- scripts/wishbone_read_write_monitor.dot | 6 +- 6 files changed, 1025 insertions(+), 54 deletions(-) create mode 100644 examples/wishbone/wishbone_fv.prot diff --git a/examples/wishbone/read_write.tx b/examples/wishbone/read_write.tx index 5c067be3..c01e6d40 100644 --- a/examples/wishbone/read_write.tx +++ b/examples/wishbone/read_write.tx @@ -6,6 +6,4 @@ trace { idle_no_cycle(); write(0b1111, 0x4000000, 0x1111); reset(); - read(0b1111, 0x4000000, 0x1112); - idle_no_cycle(); } diff --git a/examples/wishbone/wishbone_fv.prot b/examples/wishbone/wishbone_fv.prot new file mode 100644 index 00000000..00eec9aa --- /dev/null +++ b/examples/wishbone/wishbone_fv.prot @@ -0,0 +1,564 @@ +// Wishbone pins for this project from the server (the one servicing requests) perspective +interface Wishbone { + // high active RST pin (the wishbone spec requires all signals to be high active) + in i_reset: u1, + // acknowledge (from server) + out i_wb_ack: u1, + // address (from client) + in i_wb_addr: u32, + // cycle output, indicates bus cycle in progress (from client) + in i_wb_cyc: u1, + // read data from server + out i_wb_data: u32, + // write data from client + in i_wb_idata: u32, + // error from server + out i_wb_err: u1, + // mask for data in/out from client + in i_wb_sel: u4, + // indicates a valid transfer cycle from client + in i_wb_stb: u1, + // write enable (i.e. not read) from client + in i_wb_we: u1, + in BTE: u2, + in CTI: u3, +} + +prot reset() { + self.RST := 1'b1; + self.CYC := 1'b0; + self.STB := 1'b0; + step(); +} + +#[idle] +prot idle_no_cycle() { + self.RST := 1'b0; + self.CYC := 1'b0; + step(); +} + +prot idle_continue_cycle() { + self.RST := 1'b0; + self.CYC := 1'b1; + self.STB := 1'b0; + step(); +} + +prot write(mask: u4, addr: u32, data: u32) { + assert_eq(mask, 4'b1111); // TODO: support other masks + // no RST + self.RST := 1'b0; + // classic cycle (in which case bte is don't care) + self.CTI := 3'b0; + 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; + + // apply parameters + self.ADR := addr; + self.SEL := mask; + self.DAT_O := data; + + // TODO: masking + // if !mask[0] { DAT_O[ 7: 0] := X; } + // if !mask[1] { DAT_O[15: 8] := X; } + // if !mask[2] { DAT_O[23:16] := X; } + // if !mask[3] { DAT_O[31:24] := X; } + + + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true + step(); +} + +prot read(mask: u4, addr: u32, data: u32) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // no RST + self.RST := 1'b0; + // classic cycle (in which case bte is don't care) + self.CTI := 3'b0; + self.BTE := X; + + // in our simple version, we always drive cyc and stb together + self.CYC := 1'b1; + self.STB := 1'b1; + + // we are reading + self.WE := 1'b0; + + // apply parameters + self.ADR := addr; + self.SEL := mask; + self.DAT_O := X; + + while self.ACK == 1'b0 { + step(); + } + + // TODO: masking + // if mask[0] { assert_eq(self.DAT_I[ 7: 0], data[ 7: 0]); } + // if mask[1] { assert_eq(self.DAT_I[15: 8], data[15: 8]); } + // if mask[2] { assert_eq(self.DAT_I[23:16], data[23:16]); } + // if mask[3] { assert_eq(self.DAT_I[31:24], data[31:24]); } + + assert_eq(self.DAT_I, data); + step(); +} + +// a burst with only a single item uses a special cti of 7 +prot write_burst_single(mask: u4, addr: u32, data: u32) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // no RST + self.RST := 1'b0; + // final burst item + self.CTI := 3'b111; + 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; + + // apply parameters + self.ADR := addr; + self.SEL := mask; + self.DAT_O := data; + + // wait for ack + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true for one cycle + step(); +} + +// a burst with only a single item uses a special cti of 7 +prot read_burst_single(mask: u4, addr: u32, data: u32) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // no RST + self.RST := 1'b0; + // final burst item + self.CTI := 3'b111; + self.BTE := X; + + // in our simple version, we always drive cyc and stb together + self.CYC := 1'b1; + self.STB := 1'b1; + + // we are reading + self.WE := 1'b0; + + // apply parameters + self.ADR := addr; + self.SEL := mask; + + + // wait for ack + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true for one cycle and we get the data + assert_eq(self.DAT_I, data); // TODO: take mask into account + step(); +} + +prot write_burst_const(mask: u4, addr: u32, data: [u32]++) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // 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; + + // apply parameters + self.ADR := addr; + self.SEL := mask; + + for d in data { + self.DAT_O := d; + + // indicate end of cycle for last item + if is_last() { + self.CTI := 3'b111; + } + + // wait for ack + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true for one cycle + step(); + } +} + +prot read_burst_const(mask: u4, addr: u32, data: [u32]++) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // 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 reading + self.WE := 1'b0; + + // apply parameters + self.ADR := addr; + self.SEL := mask; + + for d in data { + // indicate end of cycle for last item + if is_last() { + self.CTI := 3'b111; + } + + // wait for ack + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true for one cycle and we get the data + assert_eq(self.DAT_I, d); // TODO: take mask into account + step(); + } +} + +prot write_burst_increment_linear(mask: u4, start_addr: u32, data: [u32]++) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // no RST + self.RST := 1'b0; + // incremental linear burst + self.CTI := 3'b010; + self.BTE := 2'b00; + + // 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; + + // apply parameters + self.SEL := mask; + + for d in data { + self.ADR := start_addr + (iter_count::() ## 2'b00); + self.DAT_O := d; + + // indicate end of cycle for last item + if is_last() { + self.CTI := 3'b111; + } + + // wait for ack + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true for one cycle + step(); + } +} + +prot read_burst_increment_linear(mask: u4, start_addr: u32, data: [u32]++) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // no RST + self.RST := 1'b0; + // incremental linear burst + self.CTI := 3'b010; + self.BTE := 2'b00; + + // in our simple version, we always drive cyc and stb together + self.CYC := 1'b1; + self.STB := 1'b1; + + // we are reading + self.WE := 1'b0; + + // apply parameters + self.SEL := mask; + + for d in data { + self.ADR := start_addr + (iter_count::() ## 2'b00); + + // indicate end of cycle for last item + if is_last() { + self.CTI := 3'b111; + } + + // wait for ack + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true for one cycle and we get the data + assert_eq(self.DAT_I, d); // TODO: take mask into account + step(); + } +} + + +prot write_burst_increment_wrap_4(mask: u4, start_addr: u32, data: [u32]++) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // no RST + self.RST := 1'b0; + // incremental linear burst + self.CTI := 3'b010; + self.BTE := 2'b01; // wrap 4 + + // 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; + + // apply parameters + self.SEL := mask; + + for d in data { + // we increment the last 2 bits, modulo the 2-bits that are always zero because of the 32-bit interface + self.ADR := start_addr[31:4] ## (start_addr[3:2] + iter_count::()) ## start_addr[1:0]; + self.DAT_O := d; + + // indicate end of cycle for last item + if is_last() { + self.CTI := 3'b111; + } + + // wait for ack + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true for one cycle + step(); + } +} + +prot read_burst_increment_wrap_4(mask: u4, start_addr: u32, data: [u32]++) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // no RST + self.RST := 1'b0; + // incremental linear burst + self.CTI := 3'b010; + self.BTE := 2'b01; // wrap 4 + + // in our simple version, we always drive cyc and stb together + self.CYC := 1'b1; + self.STB := 1'b1; + + // we are reading + self.WE := 1'b0; + + // apply parameters + self.SEL := mask; + + for d in data { + // we increment the last 2 bits, modulo the 2-bits that are always zero because of the 32-bit interface + self.ADR := start_addr[31:4] ## (start_addr[3:2] + iter_count::()) ## start_addr[1:0]; + + // indicate end of cycle for last item + if is_last() { + self.CTI := 3'b111; + } + + // wait for ack + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true for one cycle and we get the data + assert_eq(self.DAT_I, d); // TODO: take mask into account + step(); + } +} + +prot write_burst_increment_wrap_8(mask: u4, start_addr: u32, data: [u32]++) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // no RST + self.RST := 1'b0; + // incremental linear burst + self.CTI := 3'b010; + self.BTE := 2'b10; // wrap 8 + + // 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; + + // apply parameters + self.SEL := mask; + + for d in data { + // we increment the last 3 bits, modulo the 2-bits that are always zero because of the 32-bit interface + self.ADR := start_addr[31:5] ## (start_addr[4:2] + iter_count::()) ## start_addr[1:0]; + self.DAT_O := d; + + // indicate end of cycle for last item + if is_last() { + self.CTI := 3'b111; + } + + // wait for ack + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true for one cycle + step(); + } +} + +prot read_burst_increment_wrap_8(mask: u4, start_addr: u32, data: [u32]++) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // no RST + self.RST := 1'b0; + // incremental linear burst + self.CTI := 3'b010; + self.BTE := 2'b10; // wrap 8 + + // in our simple version, we always drive cyc and stb together + self.CYC := 1'b1; + self.STB := 1'b1; + + // we are reading + self.WE := 1'b0; + + // apply parameters + self.SEL := mask; + + for d in data { + // we increment the last 3 bits, modulo the 2-bits that are always zero because of the 32-bit interface + self.ADR := start_addr[31:5] ## (start_addr[4:2] + iter_count::()) ## start_addr[1:0]; + + // indicate end of cycle for last item + if is_last() { + self.CTI := 3'b111; + } + + // wait for ack + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true for one cycle and we get the data + assert_eq(self.DAT_I, d); // TODO: take mask into account + step(); + } +} + +prot write_burst_increment_wrap_16(mask: u4, start_addr: u32, data: [u32]++) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // no RST + self.RST := 1'b0; + // incremental linear burst + self.CTI := 3'b010; + self.BTE := 2'b11; // wrap 16 + + // 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; + + // apply parameters + self.SEL := mask; + + for d in data { + // we increment the last 4 bits, modulo the 2-bits that are always zero because of the 32-bit interface + self.ADR := start_addr[31:6] ## (start_addr[5:2] + iter_count::()) ## start_addr[1:0]; + + // indicate end of cycle for last item + if is_last() { + self.CTI := 3'b111; + } + + // wait for ack + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true for one cycle + step(); + } +} + +prot read_burst_increment_wrap_16(mask: u4, start_addr: u32, data: [u32]++) { + assert_eq(mask, 4'b1111); // TODO: support other masks + + // no RST + self.RST := 1'b0; + // incremental linear burst + self.CTI := 3'b010; + self.BTE := 2'b11; // wrap 16 + + // 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'b0; + + // apply parameters + self.SEL := mask; + + for d in data { + // we increment the last 4 bits, modulo the 2-bits that are always zero because of the 32-bit interface + self.ADR := start_addr[31:6] ## (start_addr[5:2] + iter_count::()) ## start_addr[1:0]; + + // indicate end of cycle for last item + if is_last() { + self.CTI := 3'b111; + } + + // wait for ack + while self.ACK == 1'b0 { + step(); + } + + // acknowledge is now true for one cycle and we get the data + assert_eq(self.DAT_I, d); // TODO: take mask into account + step(); + } +} diff --git a/protocols/src/backends/transition_system.rs b/protocols/src/backends/transition_system.rs index 705cdb1c..79d6a199 100644 --- a/protocols/src/backends/transition_system.rs +++ b/protocols/src/backends/transition_system.rs @@ -187,6 +187,229 @@ pub struct CoreLoweredSystem { pub reachable_nodes: Vec, } +pub struct LoweredMonitorSystem { + pub ctx: Context, + pub ts: TransitionSystem, + pub inputs: FxHashMap, + pub node_symbol: ExprRef, + pub done_state: ExprRef, + pub external_assert_state: ExprRef, + pub internal_assert_state: ExprRef, +} + +fn replace_exprs( + ctx: &mut Context, + expr: ExprRef, + substitutions: &FxHashMap, +) -> ExprRef { + simple_transform_expr(ctx, expr, |_ctx, candidate, _children| { + substitutions.get(&candidate).copied() + }) +} + +/// Lower a monitor graph without a DUT transition system. +/// +/// DUT ports become free inputs. Monitor symbols in `state_init` and the +/// control node are transition-system state. Node actions are Moore-style: +/// their updates are substituted into transition and done guards. +pub fn into_monitor_transition_system( + mut pg: ProtoGraph, + mut ts: TransitionSystem, + st: &SymbolTable, +) -> LoweredMonitorSystem { + let mut ctx = std::mem::take(&mut pg.expr_ctx); + + let mut inputs = FxHashMap::default(); + let dut_ports: Vec<_> = pg.proto_ctx.dut_pins(st).collect(); + for symbol in dut_ports { + let symbol::Type::BitVec(width) = st[symbol].tpe() else { + panic!("monitor DUT ports must be bit-vectors"); + }; + let expr = pg.symbol_expr(symbol).unwrap_or_else(|| { + let name = st.full_name_from_symbol_id(&symbol); + ctx.bv_symbol(&name, width as WidthInt) + }); + pg.cache_symbol_expr(symbol, expr); + ts.add_input(&ctx, expr); + inputs.insert(symbol, expr); + } + + let mut reachable_nodes = Vec::new(); + let mut seen = FxHashSet::default(); + let mut worklist = vec![pg.entry]; + while let Some(node) = worklist.pop() { + if !seen.insert(node) { + continue; + } + reachable_nodes.push(node); + worklist.extend( + pg[node] + .transitions + .iter() + .map(|transition| transition.target), + ); + } + + let monitor_states: Vec<_> = pg + .state_init + .iter() + .filter_map(|(&symbol, &init)| { + let expr = pg.symbol_expr(symbol)?; + Some((symbol, expr, init)) + }) + .collect(); + + // Compute each node's simultaneous monitor-state updates. Missing or + // untriggered assignments hold the current value. + let mut node_updates: FxHashMap> = FxHashMap::default(); + for &node in &reachable_nodes { + let mut updates: FxHashMap = monitor_states + .iter() + .map(|(_, expr, _)| (*expr, *expr)) + .collect(); + for action in &pg[node].actions { + let Op::Assign(symbol, assignment) = pg[action.op].clone() else { + continue; + }; + if !pg.state_init.contains_key(&symbol) { + continue; + } + let Some(state_expr) = pg.symbol_expr(symbol) else { + continue; + }; + let prior = updates[&state_expr]; + let assignment = Assignment { + dont_care: replace_exprs(&mut ctx, assignment.dont_care, &updates), + concretes: assignment + .concretes + .into_iter() + .map(|(guard, rhs)| { + ( + replace_exprs(&mut ctx, guard, &updates), + replace_exprs(&mut ctx, rhs, &updates), + ) + }) + .collect(), + }; + let action_guard = replace_exprs(&mut ctx, action.guard, &updates); + let assigned = assignment_to_ite(assignment, &mut ctx, prior, prior); + let updated = ctx.ite(action_guard, assigned, prior); + updates.insert(state_expr, updated); + } + node_updates.insert(node, updates); + } + + let node_count = pg.nodes().try_len().unwrap() as u64 + 2; + let node_id_width = u64::from(u64::BITS - node_count.leading_zeros()); + let node_sym = ctx.bv_symbol("node", node_id_width as WidthInt); + let entry_id = ctx.bit_vec_val(pg.entry.as_u32(), node_id_width); + let external_bad_state_id = ctx.bit_vec_val(pg.next_node_id().as_u32(), node_id_width); + let internal_bad_state_id = ctx.bit_vec_val(pg.next_node_id().as_u32() + 1, node_id_width); + + let mut control_transitions = Vec::new(); + let mut done_next = ctx.get_false(); + for &node in &reachable_nodes { + let node_id = ctx.bit_vec_val(node.as_u32(), node_id_width); + let node_guard = ctx.equal(node_sym, node_id); + let updates = &node_updates[&node]; + + for transition in &pg[node].transitions { + let guard = replace_exprs(&mut ctx, transition.guard, updates); + let guard = ctx.and(node_guard, guard); + control_transitions.push(IfThenExpr { + if_cond: guard, + then: ctx.bit_vec_val(transition.target.as_u32(), node_id_width), + }); + } + + for action in &pg[node].actions { + let action_guard = replace_exprs(&mut ctx, action.guard, updates); + let action_guard = ctx.and(node_guard, action_guard); + match pg[action.op].clone() { + Op::Done => done_next = ctx.or(done_next, action_guard), + Op::AssertEq(lhs, rhs) => { + let lhs = replace_exprs(&mut ctx, lhs, updates); + let rhs = replace_exprs(&mut ctx, rhs, updates); + let equal = ctx.equal(lhs, rhs); + let failed = ctx.not(equal); + let failed = ctx.and(action_guard, failed); + control_transitions.push(IfThenExpr { + if_cond: failed, + then: external_bad_state_id, + }); + } + Op::InternalAssertFalse => control_transitions.push(IfThenExpr { + if_cond: action_guard, + then: internal_bad_state_id, + }), + Op::Assign(_, _) | Op::Fork => {} + } + } + } + + let external_bad_guard = ctx.equal(node_sym, external_bad_state_id); + control_transitions.push(IfThenExpr { + if_cond: external_bad_guard, + then: external_bad_state_id, + }); + let internal_bad_guard = ctx.equal(node_sym, internal_bad_state_id); + control_transitions.push(IfThenExpr { + if_cond: internal_bad_guard, + then: internal_bad_state_id, + }); + let control_next = if_thens_to_ite(control_transitions, &mut ctx, internal_bad_state_id); + ts.add_state( + &ctx, + State { + symbol: node_sym, + init: Some(entry_id), + next: Some(control_next), + }, + ); + ts.bad_states + .push(ctx.equal(node_sym, external_bad_state_id)); + ts.bad_states + .push(ctx.equal(node_sym, internal_bad_state_id)); + + for (_, state_expr, init) in monitor_states { + let mut next = state_expr; + for &node in &reachable_nodes { + let node_id = ctx.bit_vec_val(node.as_u32(), node_id_width); + let node_guard = ctx.equal(node_sym, node_id); + next = ctx.ite(node_guard, node_updates[&node][&state_expr], next); + } + ts.add_state( + &ctx, + State { + symbol: state_expr, + init: Some(init), + next: Some(next), + }, + ); + } + + let done_state = ctx.bv_symbol("monitor.done", 1); + ts.add_state( + &ctx, + State { + symbol: done_state, + init: Some(ctx.get_false()), + next: Some(done_next), + }, + ); + ts.add_output(&mut ctx, Cow::Borrowed("done"), done_state); + + LoweredMonitorSystem { + ctx, + ts, + inputs, + node_symbol: node_sym, + done_state, + external_assert_state: external_bad_state_id, + internal_assert_state: internal_bad_state_id, + } +} + pub fn lower_proto_graph_to_transition_system( mut pg: ProtoGraph, mut ctx: Context, @@ -455,3 +678,180 @@ pub fn into_transition_system( is_dont_care: core.is_dont_care, } } + +#[cfg(test)] +mod tests { + use super::*; + use crate::frontend::diagnostic::DiagnosticHandler; + use crate::frontend::{frontend, require_single_module}; + use crate::interpreter::Value as WaveValue; + use crate::ir::to_monitor::to_monitor; + use crate::scheduler::Scheduler; + use crate::{PatronusSim, transaction_frontend}; + use baa::BitVecValue; + use patronus::sim::{InitKind, Interpreter, Simulator}; + use std::fs; + use tempfile::NamedTempFile; + + #[test] + fn standalone_monitor_system_reads_ports_and_updates_monitor_state() { + let file = NamedTempFile::new().unwrap(); + fs::write( + file.path(), + r#" + struct Dut { + in req: u1, + out ack: u1, + out echo: u1, + } + + prot request(value: u1) { + dut.req := value; + assert_eq(dut.echo, value); + while dut.ack == 1'b0 { + step(); + } + step(); + } + "#, + ) + .unwrap(); + let mut diagnostics = DiagnosticHandler::default(); + let (mut symbols, modules) = frontend(&[file.path()], &mut diagnostics, true).unwrap(); + let module = require_single_module(modules, &[file.path()]).unwrap(); + let monitor = to_monitor(module.protos, &mut symbols, Context::default()).unwrap(); + + let ts = TransitionSystem::new("protocol_monitor".to_string()); + + let lowered = into_monitor_transition_system(monitor, ts, &symbols); + + assert_eq!(lowered.inputs.len(), 3); + assert_eq!(lowered.ts.inputs.len(), 3); + assert_eq!(lowered.ts.bad_states.len(), 2); + assert_eq!(lowered.ts.outputs.len(), 1); + + let req = lowered + .inputs + .iter() + .find_map(|(symbol, expr)| (symbols[*symbol].name() == "req").then_some(*expr)) + .unwrap(); + let ack = lowered + .inputs + .iter() + .find_map(|(symbol, expr)| (symbols[*symbol].name() == "ack").then_some(*expr)) + .unwrap(); + let echo = lowered + .inputs + .iter() + .find_map(|(symbol, expr)| (symbols[*symbol].name() == "echo").then_some(*expr)) + .unwrap(); + + let mut sim = Interpreter::new(&lowered.ctx, &lowered.ts); + sim.init(InitKind::Zero); + sim.set(req, &BitVecValue::from_u64(1, 1)); + sim.set(echo, &BitVecValue::from_u64(1, 1)); + sim.set(ack, &BitVecValue::from_u64(0, 1)); + sim.step(); + assert!(sim.get(lowered.done_state).try_into_u64().unwrap() == 0); + + sim.set(ack, &BitVecValue::from_u64(1, 1)); + sim.step(); + assert!(sim.get(lowered.done_state).try_into_u64().unwrap() == 1); + } + + fn monitor_accepts_waveform( + lowered: &LoweredMonitorSystem, + symbols: &SymbolTable, + waveform: &FxHashMap>, + ) -> bool { + let cycle_count = waveform.values().map(Vec::len).max().unwrap_or(0); + let mut sim = Interpreter::new(&lowered.ctx, &lowered.ts); + sim.init(InitKind::Zero); + + for cycle in 0..cycle_count { + for (&symbol, &input) in &lowered.inputs { + let name = symbols[symbol].name(); + let width = match symbols[symbol].tpe() { + symbol::Type::BitVec(width) => width, + _ => unreachable!("monitor ports must be bit-vectors"), + }; + let value = match &waveform[name][cycle] { + WaveValue::Concrete(value) => value.clone(), + WaveValue::DontCare => BitVecValue::from_u64(0, width), + }; + sim.set(input, &value); + } + sim.step(); + let node = sim.get(lowered.node_symbol); + if node == sim.get(lowered.external_assert_state) + || node == sim.get(lowered.internal_assert_state) + { + return false; + } + } + + sim.get(lowered.done_state).try_into_u64().unwrap() == 1 + } + + #[test] + #[ignore = "requires yosys to execute the Wishbone RTL"] + fn generated_wishbone_waveform_is_accepted_and_mutation_is_rejected() { + let root = std::path::Path::new(env!("CARGO_MANIFEST_DIR")) + .parent() + .unwrap(); + let protocol_file = root.join("examples/wishbone/wishbone.prot"); + let trace_file = root.join("examples/wishbone/read_write.tx"); + let dut_file = root.join("examples/wishbone/rtl/dut.v"); + let tb_file = root.join("examples/wishbone/rtl/tb.v"); + + let mut diagnostics = DiagnosticHandler::default(); + let (mut symbols, modules) = frontend(&[&protocol_file], &mut diagnostics, true).unwrap(); + let module = require_single_module(modules, &[&protocol_file]).unwrap(); + let traces = + transaction_frontend(&trace_file, &symbols, &module.protos, &mut diagnostics).unwrap(); + let trace = traces[0].clone(); + let selected_names: FxHashSet<_> = trace.iter().map(|(name, _)| name.as_str()).collect(); + let selected = module + .protos + .iter() + .filter(|protocol| selected_names.contains(protocol.name.as_str())) + .cloned() + .collect(); + + let temp = tempfile::tempdir().unwrap(); + let fst = temp.path().join("read_write.fst"); + let sim = PatronusSim::new( + &[dut_file, tb_file], + Some("tb"), + &module, + Some(fst.to_str().unwrap()), + ) + .unwrap(); + let mut scheduler = Scheduler::new( + &symbols, + &module.protos, + trace, + sim, + &mut diagnostics, + u32::MAX, + ); + assert!(scheduler.execute_transactions().iter().all(Result::is_ok)); + let raw_waveform = scheduler.waveform(); + let mut waveform: FxHashMap<_, _> = raw_waveform + .into_iter() + .map(|(port, values)| (scheduler.port_name(port).to_string(), values)) + .collect(); + drop(scheduler); + assert!(std::fs::metadata(fst).unwrap().len() > 0); + + let monitor = to_monitor(selected, &mut symbols, Context::default()).unwrap(); + + let ts = TransitionSystem::new("protocol_monitor".to_string()); + let lowered = into_monitor_transition_system(monitor, ts, &symbols); + assert!(monitor_accepts_waveform(&lowered, &symbols, &waveform)); + + // RST=1 and CYC=1 cannot be reset, idle, read, or write. + waveform.get_mut("CYC").unwrap()[0] = WaveValue::Concrete(BitVecValue::from_u64(1, 1)); + assert!(!monitor_accepts_waveform(&lowered, &symbols, &waveform)); + } +} diff --git a/protocols/src/ir/determinize.rs b/protocols/src/ir/determinize.rs index 8392a2ab..c4403e95 100644 --- a/protocols/src/ir/determinize.rs +++ b/protocols/src/ir/determinize.rs @@ -132,32 +132,55 @@ fn transition_guards_after_node_updates( let mut substitutions = FxHashMap::default(); for action in actions { - let crate::ir::proto_graph::Op::Assign(symbol, assignment) = - protocol[action.op].clone() + let crate::ir::proto_graph::Op::Assign(symbol, assignment) = protocol[action.op].clone() else { continue; }; - if !protocol.state_init.contains_key(&symbol) - || assignment.dont_care != protocol.false_id() + if !protocol.state_init.contains_key(&symbol) || assignment.dont_care != protocol.false_id() { continue; } let Some(lhs) = protocol.symbol_expr(symbol) else { continue; }; - if !lhs.is_bool(&protocol.expr_ctx) { - continue; - } + let prior = substitutions.get(&lhs).copied().unwrap_or(lhs); + let action_guard = simple_transform_expr( + &mut protocol.expr_ctx, + action.guard, + |_ctx, candidate, _children| substitutions.get(&candidate).copied(), + ); + let branches: Vec<_> = assignment + .concretes + .iter() + .map(|(guard, rhs)| { + ( + simple_transform_expr( + &mut protocol.expr_ctx, + *guard, + |_ctx, candidate, _children| substitutions.get(&candidate).copied(), + ), + simple_transform_expr( + &mut protocol.expr_ctx, + *rhs, + |_ctx, candidate, _children| substitutions.get(&candidate).copied(), + ), + ) + }) + .collect(); // Assignment branches use first-match priority. If no branch fires, // monitor state holds its old value. - let mut next = lhs; - for (branch_guard, rhs) in assignment.concretes.iter().rev() { - let guard = protocol.and_guard(action.guard, *branch_guard); - let when_set = protocol.and_guard(guard, *rhs); - let not_guard = protocol.not_guard(guard); - let when_held = protocol.and_guard(not_guard, next); - next = protocol.or_guard(when_set, when_held); + let mut next = prior; + for (branch_guard, rhs) in branches.into_iter().rev() { + let guard = protocol.and_guard(action_guard, branch_guard); + next = if lhs.is_bool(&protocol.expr_ctx) { + let when_set = protocol.and_guard(guard, rhs); + let not_guard = protocol.not_guard(guard); + let when_held = protocol.and_guard(not_guard, next); + protocol.or_guard(when_set, when_held) + } else { + protocol.expr_ctx.ite(guard, rhs, next) + }; } substitutions.insert(lhs, next); } @@ -166,9 +189,9 @@ fn transition_guards_after_node_updates( .iter() .map(|transition| { let guard = simple_transform_expr( - &mut protocol.expr_ctx, - transition.guard, - |_ctx, candidate, _children| substitutions.get(&candidate).copied(), + &mut protocol.expr_ctx, + transition.guard, + |_ctx, candidate, _children| substitutions.get(&candidate).copied(), ); protocol.simplifier.simplify(&mut protocol.expr_ctx, guard) }) diff --git a/protocols/src/ir/to_monitor.rs b/protocols/src/ir/to_monitor.rs index db480e93..9a0d082e 100644 --- a/protocols/src/ir/to_monitor.rs +++ b/protocols/src/ir/to_monitor.rs @@ -404,13 +404,11 @@ fn learn_equality_knownness( } else { Knownness::Maybe }; - facts - .entry(candidate) - .and_modify(|knownness| { - if *knownness == Knownness::Unknown { - *knownness = learned; - } - }); + facts.entry(candidate).and_modify(|knownness| { + if *knownness == Knownness::Unknown { + *knownness = learned; + } + }); } } } @@ -604,14 +602,7 @@ fn transform_candidate_fragment( ¶meters, &local_facts, ); - learn_equality_knownness( - pg, - active, - lhs, - rhs, - ¶meters, - &mut local_facts, - ); + learn_equality_knownness(pg, active, lhs, rhs, ¶meters, &mut local_facts); } Op::Fork => return Err(ToMonitorError::UnsupportedFork), Op::InternalAssertFalse | Op::Done => { @@ -713,13 +704,17 @@ fn loop_fragment_exit_to_entry( transition.consumes_step = true; } } - if pg[node] + let return_guards: Vec<_> = pg[node] .transitions .iter() - .any(|transition| transition.target == entry) - { + .filter(|transition| transition.target == entry) + .map(|transition| transition.guard) + .collect(); + let return_guard = or_all(pg, return_guards); + if return_guard != pg.false_id() { let done = pg.o(Op::Done); - pg.push_action(node, Action::new(live_expr, done)); + let done_guard = pg.and_guard(live_expr, return_guard); + pg.push_action(node, Action::new(done_guard, done)); } } } @@ -930,20 +925,11 @@ mod tests { let protocol_file = "../examples/wishbone/wishbone.prot"; let trace_file = "../examples/wishbone/read_write.tx"; let mut diagnostics = DiagnosticHandler::default(); - let (mut symbols, modules) = - frontend(&[protocol_file], &mut diagnostics, true).unwrap(); + let (mut symbols, modules) = frontend(&[protocol_file], &mut diagnostics, true).unwrap(); let module = require_single_module(modules, &[protocol_file]).unwrap(); - let traces = transaction_frontend( - trace_file, - &symbols, - &module.protos, - &mut diagnostics, - ) - .unwrap(); - let selected_names: HashSet<_> = traces[0] - .iter() - .map(|(name, _)| name.as_str()) - .collect(); + let traces = + transaction_frontend(trace_file, &symbols, &module.protos, &mut diagnostics).unwrap(); + let selected_names: HashSet<_> = traces[0].iter().map(|(name, _)| name.as_str()).collect(); let selected = module .protos .into_iter() diff --git a/scripts/wishbone_read_write_monitor.dot b/scripts/wishbone_read_write_monitor.dot index b39ca421..3182d1dd 100644 --- a/scripts/wishbone_read_write_monitor.dot +++ b/scripts/wishbone_read_write_monitor.dot @@ -3,14 +3,14 @@ digraph "reset" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] reset_live := 0 if or(or(not(self.RST), self.CYC), self.STB); 1 if not(or(or(not(self.RST), self.CYC), self.STB))\n[or(or(or(reset_live, idle_no_cycle_live), write_live), read_live)] done\n[1] idle_no_cycle_live := 0 if or(self.RST, self.CYC); 1 if not(or(self.RST, self.CYC))\n[1] write_mask := 15 if 1\n[1] write_addr := self.ADR if 1\n[1] write_data := self.DAT_O if 1\n[1] write_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))))\n[1] read_mask := 15 if 1\n[1] read_data := self.DAT_I if self.ACK\n[1] read_addr := self.ADR if 1\n[1] read_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))))\n[1] read_data_known := 1 if self.ACK; 0 if not(self.ACK)"]; + node0 [label="[1] reset_live := 0 if or(or(not(self.RST), self.CYC), self.STB); 1 if not(or(or(not(self.RST), self.CYC), self.STB))\n[or(or(or(reset_live, idle_no_cycle_live), and(write_live, and(write_live, self.ACK))), and(read_live, and(read_live, self.ACK)))] done\n[1] idle_no_cycle_live := 0 if or(self.RST, self.CYC); 1 if not(or(self.RST, self.CYC))\n[1] write_mask := 15 if 1\n[1] write_addr := self.ADR if 1\n[1] write_data := self.DAT_O if 1\n[1] write_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, write_mask))), not(self.STB)), not(self.WE)), not(eq(self.CTI, 0))))\n[1] read_mask := 15 if 1\n[1] read_data := self.DAT_I if self.ACK\n[1] read_addr := self.ADR if 1\n[1] read_live := 0 if or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))); 1 if not(or(or(or(or(or(self.RST, not(self.CYC)), not(eq(self.SEL, read_mask))), not(self.STB)), self.WE), not(eq(self.CTI, 0))))\n[1] read_data_known := 1 if self.ACK; 0 if not(self.ACK)"]; node0 -> node0 [label="or(or(or(reset_live, idle_no_cycle_live), and(write_live, self.ACK)), and(read_live, self.ACK)) / step"]; node0 -> node1 [label="and(write_live, not(self.ACK)) / step"]; node0 -> node2 [label="and(read_live, not(self.ACK)) / step"]; - node1 [label="[1] write_live := 0 if or(or(or(or(or(or(or(and(write_live, self.RST), and(write_live, not(eq(self.ADR, write_addr)))), and(write_live, not(self.CYC))), and(write_live, not(eq(self.DAT_O, write_data)))), and(write_live, not(eq(self.SEL, write_mask)))), and(write_live, not(self.STB))), and(write_live, not(self.WE))), and(write_live, not(eq(self.CTI, 0))))\n[write_live] done"]; + node1 [label="[1] write_live := 0 if or(or(or(or(or(or(or(and(write_live, self.RST), and(write_live, not(eq(self.ADR, write_addr)))), and(write_live, not(self.CYC))), and(write_live, not(eq(self.DAT_O, write_data)))), and(write_live, not(eq(self.SEL, write_mask)))), and(write_live, not(self.STB))), and(write_live, not(self.WE))), and(write_live, not(eq(self.CTI, 0))))\n[and(write_live, and(write_live, self.ACK))] done"]; node1 -> node0 [label="and(write_live, self.ACK) / step"]; node1 -> node1 [label="and(write_live, not(self.ACK)) / step"]; - node2 [label="[1] read_live := 0 if or(or(or(or(or(or(or(and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))), and(read_live, self.RST)), and(read_live, not(eq(self.ADR, read_addr)))), and(read_live, not(self.CYC))), and(read_live, not(eq(self.SEL, read_mask)))), and(read_live, not(self.STB))), and(read_live, self.WE)), and(read_live, not(eq(self.CTI, 0))))\n[1] read_data := self.DAT_I if and(and(read_live, self.ACK), not(read_data_known))\n[1] read_data_known := 1 if and(and(read_live, self.ACK), not(read_data_known))\n[read_live] done"]; + node2 [label="[1] read_live := 0 if or(or(or(or(or(or(or(and(and(and(read_live, self.ACK), read_data_known), not(eq(self.DAT_I, read_data))), and(read_live, self.RST)), and(read_live, not(eq(self.ADR, read_addr)))), and(read_live, not(self.CYC))), and(read_live, not(eq(self.SEL, read_mask)))), and(read_live, not(self.STB))), and(read_live, self.WE)), and(read_live, not(eq(self.CTI, 0))))\n[1] read_data := self.DAT_I if and(and(read_live, self.ACK), not(read_data_known))\n[1] read_data_known := 1 if and(and(read_live, self.ACK), not(read_data_known))\n[and(read_live, and(read_live, self.ACK))] done"]; node2 -> node0 [label="and(read_live, self.ACK) / step"]; node2 -> node2 [label="and(read_live, not(self.ACK)) / step"]; }