diff --git a/graph-interp/src/main.rs b/graph-interp/src/main.rs index 4d75dded..9c4aff68 100644 --- a/graph-interp/src/main.rs +++ b/graph-interp/src/main.rs @@ -7,11 +7,13 @@ use protocols::frontend::design::{Design, find_a_single_design}; use protocols::frontend::diagnostic::DiagnosticHandler; use protocols::frontend::symbol::SymbolTable; use protocols::ir::determinize::determinized; -use protocols::ir::edge_contract::{contract_edges, normalize_assignments}; +use protocols::ir::edge_contract::contract_edges; use protocols::ir::graph_interpreter; use protocols::ir::graphviz::to_dot_string; 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::trace_lowering::lower_trace_to_ir; use protocols::{PatronusSim, Value, frontend, transaction_frontend}; use rustc_hash::FxHashMap; @@ -61,6 +63,10 @@ struct Cli { /// Prints trace status lines and ASCII waveforms #[arg(long)] ascii_waveform: bool, + + /// Print reaching definition analysis results + #[arg(long)] + reaching_definitions: bool, } fn load_protocols(cli: &Cli) -> Ast { @@ -128,8 +134,16 @@ fn run_classic( if cli.contract_edges { for (_, graph) in &mut graphs { contract_edges(graph, st); - normalize_assignments(graph, st); - graph.simplify_all_exprs(); + + // if !exists_conflicts(&rd, graph) && all_ports_present(&rd, graph, st) { + // propagate_assignments(graph, st, &rd); + // } else { + // normalize_assignments(graph, st); + // } + + if cli.graphout { + println!("{}", to_dot_string(graph, st).as_str()); + } } } @@ -142,8 +156,11 @@ fn run_classic( .iter_mut() .find(|(n, _)| n == &name) .unwrap_or_else(|| panic!("unknown protocol {name}")); + + let rd = reaching_definitions(pg, st); + propagate_assignments(pg, st, &rd); + let args = build_arg_map(&pg.args, st, values); - // println!("{}", to_dot_string(pg, st)); graph_interpreter::interpret(pg, st, args, &mut sim); } print_trace_success(trace_index); @@ -167,13 +184,31 @@ fn run_respect_forks( let mut joint = lower_trace_to_ir(trace, &protos_by_name, st); + if cli.graphout { + println!("// joint graph for trace {trace_index}"); + println!("{}", to_dot_string(&joint, st)); + } + if cli.determinize { joint = determinized(joint, st); } // normalize_assignments(&mut joint, st); if cli.graphout { - println!("// joint graph for trace {trace_index}"); + println!("// post-determinization joint graph for trace {trace_index}"); + println!("{}", to_dot_string(&joint, st)); + } + + let rd = reaching_definitions(&mut joint, st); + if cli.reaching_definitions { + println!("// reaching definitions for trace {trace_index}"); + println!("{}", format_reaching_defs(&joint, st, &rd)); + } + + propagate_assignments(&mut joint, st, &rd); + + if cli.graphout { + println!("// post-propagation joint graph for trace {trace_index}"); println!("{}", to_dot_string(&joint, st)); } @@ -181,6 +216,7 @@ fn run_respect_forks( let waveform = graph_interpreter::interpret(&joint, st, FxHashMap::default(), &mut sim); if cli.ascii_waveform { print_trace_success(trace_index); + // println!("ascii"); print_ascii_waveform( waveform, |port| sim.port_name(port).to_string(), diff --git a/protocols/src/ir/determinize.rs b/protocols/src/ir/determinize.rs index 84741cc9..a89de052 100644 --- a/protocols/src/ir/determinize.rs +++ b/protocols/src/ir/determinize.rs @@ -33,19 +33,23 @@ fn get_or_create_state( } /// Result of a (conservative) satisfiability check on a guard. -enum SatResult { +pub enum SatResult { DefinitelyUnsat, MaybeSat, + DefinitelySat, } // TODO: Strengthen this with a real SAT/SMT query to prune more aggressively. -fn check_sat(protocol: &mut ProtoGraph, guard: ExprRef) -> SatResult { +pub fn check_sat(protocol: &mut ProtoGraph, guard: ExprRef) -> SatResult { let simplified = { let (expr_ctx, simplifier) = (&mut protocol.expr_ctx, &mut protocol.simplifier); simplifier.simplify(expr_ctx, guard) }; + if simplified == protocol.false_id() { SatResult::DefinitelyUnsat + } else if simplified == protocol.true_id() { + SatResult::DefinitelySat } else { SatResult::MaybeSat } @@ -109,13 +113,16 @@ pub fn determinized(protocol: ProtoGraph, symbols: &SymbolTable) -> ProtoGraph { guard = protocol.and_guard(guard, lit); } - match check_sat(&mut protocol, guard) { + let guard = match check_sat(&mut protocol, guard) { SatResult::DefinitelyUnsat => continue, - SatResult::MaybeSat => { - let target_id = - get_or_create_state(targets, &mut state_ids, &mut worklist, &mut new_nodes); - new_trans.push(Transition::new(guard, target_id, true)); - } + SatResult::DefinitelySat => protocol.true_id(), + SatResult::MaybeSat => guard, + }; + + { + let target_id = + get_or_create_state(targets, &mut state_ids, &mut worklist, &mut new_nodes); + new_trans.push(Transition::new(guard, target_id, true)); } } diff --git a/protocols/src/ir/edge_contract.rs b/protocols/src/ir/edge_contract.rs index acebe0c9..96035761 100644 --- a/protocols/src/ir/edge_contract.rs +++ b/protocols/src/ir/edge_contract.rs @@ -1,8 +1,8 @@ use std::collections::{BTreeSet, VecDeque}; use crate::frontend::symbol::{SymbolId, SymbolTable, Type as FrontType}; -use crate::ir::proto_graph::{Action, NodeId, Op, ProtoGraph, Transition}; -use patronus::expr::{Expr, ExprRef}; +use crate::ir::proto_graph::{Action, Assignment, NodeId, Op, ProtoGraph, Transition}; +use patronus::expr::ExprRef; fn symbol_expr(protocol: &mut ProtoGraph, symbols: &SymbolTable, symbol_id: SymbolId) -> ExprRef { if let Some(expr) = protocol.symbol_expr(symbol_id) { @@ -25,17 +25,8 @@ fn symbol_expr(protocol: &mut ProtoGraph, symbols: &SymbolTable, symbol_id: Symb expr } -/// Constrain `rhs` to `guard`, falling back to `fallback` outside it. An -/// unconditional (`true`) guard needs no `ite`. -fn lift(protocol: &mut ProtoGraph, guard: ExprRef, rhs: ExprRef, fallback: ExprRef) -> ExprRef { - if guard == protocol.true_id() { - rhs - } else { - protocol.expr_ctx.ite(guard, rhs, fallback) - } -} - -fn same_assignment_target(symbols: &SymbolTable, lhs: SymbolId, rhs: SymbolId) -> bool { +/// TODO: Better way to deal with this? +pub fn same_assignment_target(symbols: &SymbolTable, lhs: SymbolId, rhs: SymbolId) -> bool { lhs == rhs || symbols[lhs].full_name(symbols) == symbols[rhs].full_name(symbols) } @@ -50,140 +41,118 @@ fn record_internal_assert( }); } -#[derive(Clone, Copy)] -struct AssignmentBranch { - guard: ExprRef, - rhs: ExprRef, - is_dont_care: bool, -} - -fn simplify_expr(protocol: &mut ProtoGraph, expr: ExprRef) -> ExprRef { - let (expr_ctx, simplifier) = (&mut protocol.expr_ctx, &mut protocol.simplifier); - simplifier.simplify(expr_ctx, expr) -} - -fn push_assignment_branch( +pub fn guard_assignment( protocol: &mut ProtoGraph, - branches: &mut Vec, + assignment: Assignment, guard: ExprRef, - rhs: ExprRef, -) { - let guard = simplify_expr(protocol, guard); - if guard == protocol.false_id() { - return; +) -> Assignment { + let dont_care = protocol.and_guard(guard, assignment.dont_care); + let concretes = assignment + .concretes + .into_iter() + .filter_map(|(branch_guard, rhs)| { + let guarded = protocol.and_guard(guard, branch_guard); + (guarded != protocol.false_id()).then_some((guarded, rhs)) + }) + .collect(); + + Assignment { + dont_care, + concretes, } +} - branches.push(AssignmentBranch { - guard, - rhs, - is_dont_care: protocol.dont_cares.contains(&rhs), - }); +pub fn concrete_coverage(protocol: &mut ProtoGraph, assignment: &Assignment) -> ExprRef { + let raw_coverage = assignment + .concretes + .iter() + .fold(protocol.false_id(), |guard, (concrete_guard, _)| { + protocol.or_guard(guard, *concrete_guard) + }); + let not_dont_care = protocol.not_guard(assignment.dont_care); + protocol.and_guard(not_dont_care, raw_coverage) } -// turns an ITE into a list of predicated assignments -fn flatten_assignment_rhs( +pub fn effective_concretes( protocol: &mut ProtoGraph, - rhs: ExprRef, - default_value: ExprRef, - action_guard: ExprRef, -) -> Vec { - // Assignment RHSs are either bare values or ITE chains whose true branches are bare values. - let mut branches = Vec::new(); - let mut path_guard = simplify_expr(protocol, action_guard); - let mut cursor = rhs; - - while path_guard != protocol.false_id() && cursor != default_value { - match protocol.expr_ctx[cursor].clone() { - Expr::BVIte { cond, tru, fals } => { - let branch_guard = protocol.and_guard(path_guard, cond); - push_assignment_branch(protocol, &mut branches, branch_guard, tru); - - let not_cond = protocol.not_guard(cond); - path_guard = protocol.and_guard(path_guard, not_cond); - cursor = fals; - } - _ => { - push_assignment_branch(protocol, &mut branches, path_guard, cursor); - break; - } + assignment: &Assignment, +) -> Vec<(ExprRef, ExprRef)> { + let mut prior = assignment.dont_care; + let mut effective = Vec::with_capacity(assignment.concretes.len()); + + for (guard, rhs) in &assignment.concretes { + let not_prior = protocol.not_guard(prior); + let effective_guard = protocol.and_guard(not_prior, *guard); + if effective_guard != protocol.false_id() { + effective.push((effective_guard, *rhs)); } + prior = protocol.or_guard(prior, *guard); } - branches + effective } -/// Turn branches back into an ITE -fn rebuild_assignment_rhs( +pub fn merge_ordered_assignment( protocol: &mut ProtoGraph, - branches: &[AssignmentBranch], - default_value: ExprRef, -) -> ExprRef { - branches - .iter() - .rev() - .fold(default_value, |fallback, branch| { - lift(protocol, branch.guard, branch.rhs, fallback) - }) -} - -/// Append the new `branches` to `output` -/// Iff DontCare is true, add `DontCare` branches -fn append_assignment_branches( - output: &mut Vec, - branches: &[AssignmentBranch], - dont_care: bool, -) { - output.extend( - branches - .iter() - .copied() - .filter(|branch| branch.is_dont_care == dont_care), - ); + existing: Assignment, + new: Assignment, +) -> Assignment { + // Ordered contraction preserves source order: the later action wins over + // the earlier action. Therefore the new summary's preferences come first. + let new_concretes = concrete_coverage(protocol, &new); + let not_new_concretes = protocol.not_guard(new_concretes); + let old_dont_care = protocol.and_guard(not_new_concretes, existing.dont_care); + let dont_care = protocol.or_guard(new.dont_care, old_dont_care); + + let mut concretes = new.concretes; + concretes.extend(existing.concretes); + + Assignment { + dont_care, + concretes, + } } -fn merge_unordered_assignment_rhs( +pub fn merge_unordered_assignment( protocol: &mut ProtoGraph, internal_assert_guard: &mut Option, - default_value: ExprRef, - existing_guard: ExprRef, - existing_rhs: ExprRef, - new_guard: ExprRef, - new_rhs: ExprRef, -) -> ExprRef { - // flatten the existing assignment in the node we're merging into - let existing_branches = - flatten_assignment_rhs(protocol, existing_rhs, default_value, existing_guard); - // flatten the new assignment we're merging in - let new_branches = flatten_assignment_rhs(protocol, new_rhs, default_value, new_guard); - - for existing_branch in existing_branches - .iter() - .filter(|branch| !branch.is_dont_care) - { - // find all the different concrete values and add internal assertions for their conjunction - for new_branch in new_branches.iter().filter(|branch| !branch.is_dont_care) { + existing: Assignment, + new: Assignment, +) -> Assignment { + let existing_effective = effective_concretes(protocol, &existing); + let new_effective = effective_concretes(protocol, &new); + + for (existing_guard, existing_rhs) in &existing_effective { + for (new_guard, new_rhs) in &new_effective { // assignments to the same value are totally legal - if existing_branch.rhs == new_branch.rhs { + if existing_rhs == new_rhs { continue; } // assignments to different concrete values are illegal - let overlap = protocol.and_guard(existing_branch.guard, new_branch.guard); + let overlap = protocol.and_guard(*existing_guard, *new_guard); if overlap != protocol.false_id() { record_internal_assert(protocol, internal_assert_guard, overlap); } } } - // add the existing concrete branches, new concrete branches, existing DontCare branches, new dontcare branches. Guarantees our Concrete assignments will be preferred to DontCares across nodes. - let mut merged_branches = Vec::with_capacity(existing_branches.len() + new_branches.len()); - append_assignment_branches(&mut merged_branches, &existing_branches, false); - append_assignment_branches(&mut merged_branches, &new_branches, false); - append_assignment_branches(&mut merged_branches, &existing_branches, true); - append_assignment_branches(&mut merged_branches, &new_branches, true); + let existing_concretes = concrete_coverage(protocol, &existing); + let new_concretes = concrete_coverage(protocol, &new); + + let not_new_concretes = protocol.not_guard(new_concretes); + let existing_dont_care = protocol.and_guard(not_new_concretes, existing.dont_care); + let not_existing_concretes = protocol.not_guard(existing_concretes); + let new_dont_care = protocol.and_guard(not_existing_concretes, new.dont_care); + let dont_care = protocol.or_guard(existing_dont_care, new_dont_care); + + let mut concretes = existing_effective; + concretes.extend(new_effective); - // turn it back into an ITE from branches - rebuild_assignment_rhs(protocol, &merged_branches, default_value) + Assignment { + dont_care, + concretes, + } } pub fn append_action( @@ -195,8 +164,12 @@ pub fn append_action( ordered: bool, ) { match protocol[action.op].clone() { - Op::Assign(symbol_id, rhs) => { - let default_value = symbol_expr(protocol, symbols, symbol_id); + Op::Assign(symbol_id, assignment) => { + assert_eq!( + action.guard, + protocol.true_id(), + "assignment action guards must be 1; path conditions belong in Assignment" + ); // By invariant, there can be at most one existing assignment for this symbol. let Some(idx) = actions.iter().position(|prior_action| { @@ -210,29 +183,28 @@ pub fn append_action( return; }; - let existing_guard = actions[idx].guard; - let existing_rhs = match protocol[actions[idx].op].clone() { - Op::Assign(_, existing_rhs) => existing_rhs, + assert_eq!( + actions[idx].guard, + protocol.true_id(), + "assignment action guards must be 1; path conditions belong in Assignment" + ); + let existing_assignment = match protocol[actions[idx].op].clone() { + Op::Assign(_, existing_assignment) => existing_assignment, _ => unreachable!(), }; - let (new_guard, new_rhs) = (action.guard, rhs); - let merged_rhs = if ordered { - let existing_else = lift(protocol, existing_guard, existing_rhs, default_value); - lift(protocol, new_guard, new_rhs, existing_else) + let merged_assignment = if ordered { + merge_ordered_assignment(protocol, existing_assignment, assignment) } else { - merge_unordered_assignment_rhs( + merge_unordered_assignment( protocol, internal_assert_guard, - default_value, - existing_guard, - existing_rhs, - new_guard, - new_rhs, + existing_assignment, + assignment, ) }; - let new_op = protocol.o(Op::Assign(symbol_id, merged_rhs)); + let new_op = protocol.o(Op::Assign(symbol_id, merged_assignment)); actions[idx].guard = protocol.true_id(); actions[idx].op = new_op; } @@ -326,8 +298,23 @@ pub fn contract_edges(protocol: &mut ProtoGraph, symbols: &SymbolTable) { next_path.insert(target_node_id); for action in target_actions { - let merged_action = - Action::with_guard(&action, protocol.and_guard(incoming_guard, action.guard)); + let merged_action = match protocol[action.op].clone() { + Op::Assign(symbol_id, assignment) => { + assert_eq!( + action.guard, + protocol.true_id(), + "assignment action guards must be 1; path conditions belong in Assignment" + ); + let guarded_assignment = + guard_assignment(protocol, assignment, incoming_guard); + let guarded_op = protocol.o(Op::Assign(symbol_id, guarded_assignment)); + Action::new(protocol.true_id(), guarded_op) + } + _ => Action::with_guard( + &action, + protocol.and_guard(incoming_guard, action.guard), + ), + }; append_action( protocol, symbols, @@ -401,7 +388,9 @@ pub fn normalize_assignments(protocol: &mut ProtoGraph, symbols: &SymbolTable) { for symbol_id in unassigned_inputs { // assign the symbol to its current expression (old value) let symbol_expr = symbol_expr(protocol, symbols, symbol_id); - let op = protocol.o(Op::Assign(symbol_id, symbol_expr)); + let assignment = + Assignment::concrete(protocol.false_id(), protocol.true_id(), symbol_expr); + let op = protocol.o(Op::Assign(symbol_id, assignment)); protocol.push_action(node_id, Action::new(protocol.true_id(), op)) } } @@ -415,6 +404,18 @@ mod tests { use cranelift_entity::EntityRef; use patronus::expr::SerializableIrNode; + fn concrete_assignment(protocol: &ProtoGraph, rhs: ExprRef) -> Assignment { + Assignment::concrete(protocol.false_id(), protocol.true_id(), rhs) + } + + fn dont_care_assignment(protocol: &ProtoGraph) -> Assignment { + Assignment::dont_care(protocol.true_id()) + } + + fn expr_str(protocol: &ProtoGraph, expr: ExprRef) -> String { + protocol.expr_ctx[expr].serialize_to_str(&protocol.expr_ctx) + } + #[test] fn allows_overlapping_dont_care_and_concrete_assignments() { let mut protocol = ProtoGraph::new(ProtocolContext::new("test".into(), ROOT_SCOPE)); @@ -425,8 +426,11 @@ mod tests { protocol.cache_symbol_expr(symbol_id, symbol); protocol.dont_cares.insert(dont_care); - let concrete_op = protocol.o(Op::Assign(symbol_id, concrete)); - let dont_care_op = protocol.o(Op::Assign(symbol_id, dont_care)); + let concrete_op = protocol.o(Op::Assign( + symbol_id, + concrete_assignment(&protocol, concrete), + )); + let dont_care_op = protocol.o(Op::Assign(symbol_id, dont_care_assignment(&protocol))); let mut actions = vec![Action::new(protocol.true_id(), concrete_op)]; let mut internal_assert_guard = None; let true_id = protocol.true_id(); @@ -445,13 +449,11 @@ mod tests { // the order in which the assigns are given is preserved (Concrete should not subsume DontCare) assert_eq!(actions.len(), 1); - let Op::Assign(_, rhs) = protocol[actions[0].op] else { + let Op::Assign(_, assignment) = protocol[actions[0].op].clone() else { panic!("expected assignment"); }; - assert_eq!( - protocol.expr_ctx[rhs].serialize_to_str(&protocol.expr_ctx), - "dont_care" - ); + assert_eq!(expr_str(&protocol, assignment.dont_care), "1'b1"); + assert_eq!(assignment.concretes, vec![(protocol.true_id(), concrete)]); } #[test] @@ -474,27 +476,25 @@ mod tests { let mut actions = Vec::new(); let mut internal_assert_guard = None; for (guard, rhs) in [(p, one), (q, two), (r, three)] { - let op = protocol.o(Op::Assign(symbol_id, rhs)); + let assignment = Assignment::concrete(protocol.false_id(), guard, rhs); + let op = protocol.o(Op::Assign(symbol_id, assignment)); + let true_id = protocol.true_id(); append_action( &mut protocol, &SymbolTable::default(), &mut actions, &mut internal_assert_guard, - Action::new(guard, op), + Action::new(true_id, op), false, ); } assert_eq!(actions.len(), 1); - // we should now have an ITE form with [1] always as the guard - assert_eq!( - protocol.expr_ctx[actions[0].guard].serialize_to_str(&protocol.expr_ctx), - "1'b1" - ); + assert_ne!(actions[0].guard, protocol.false_id()); // assert any two guards being run together. (p and q) or (p and r) assert_eq!( - protocol.expr_ctx[internal_assert_guard.unwrap()].serialize_to_str(&protocol.expr_ctx), + expr_str(&protocol, internal_assert_guard.unwrap()), "or(or(and(p, q), and(p, r)), and(and(not(p), q), r))" ); } @@ -514,15 +514,24 @@ mod tests { let r = protocol.expr_ctx.bv_symbol("r", 1); let s = protocol.expr_ctx.bv_symbol("s", 1); - // Node A: [1] DUT.a := ite(s, X, ite(q, 3, DUT.a)) - // Node B: [1] DUT.a := ite(r, 4, DUT.a) + // Node A: [1] DUT.a := { X if s; 3 if q } + // Node B: [1] DUT.a := { 4 if r } - let q_three = protocol.expr_ctx.ite(q, three, symbol); - let node_a_rhs = protocol.expr_ctx.ite(s, dont_care, q_three); - let node_b_rhs = protocol.expr_ctx.ite(r, four, symbol); let true_id = protocol.true_id(); - let node_a_op = protocol.o(Op::Assign(symbol_id, node_a_rhs)); - let node_b_op = protocol.o(Op::Assign(symbol_id, node_b_rhs)); + let node_a_op = protocol.o(Op::Assign( + symbol_id, + Assignment { + dont_care: s, + concretes: vec![(q, three)], + }, + )); + let node_b_op = protocol.o(Op::Assign( + symbol_id, + Assignment { + dont_care: protocol.false_id(), + concretes: vec![(r, four)], + }, + )); let mut actions = vec![Action::new(true_id, node_a_op)]; let mut internal_assert_guard = None; @@ -537,32 +546,27 @@ mod tests { ); assert_eq!(actions.len(), 1); - assert_eq!( - protocol.expr_ctx[actions[0].guard].serialize_to_str(&protocol.expr_ctx), - "1'b1" - ); + assert_ne!(actions[0].guard, protocol.false_id()); // q and r are our concrete assignments to 3 and 4. assignment to 3 only triggers if // not s , so there is only a conflicting assignment under ((not s) and q and r) assert_eq!( - protocol.expr_ctx[internal_assert_guard.unwrap()].serialize_to_str(&protocol.expr_ctx), + expr_str(&protocol, internal_assert_guard.unwrap()), "and(and(not(s), q), r)" ); protocol.simplify_all_exprs(); - let Op::Assign(_, rhs) = protocol[actions[0].op] else { + let Op::Assign(_, assignment) = protocol[actions[0].op].clone() else { panic!("expected assignment"); }; - // the ordering of the concrete assignments is arbitrary, but should come before the - // DontCare. however, the assignment to 3 should only happen if the DontCare - // assignment is not triggered, since those are ordered within a node - // Thus: if q and not s => 3, if r => 4, if s => X, otherwise DUT.a - assert_eq!( - protocol.expr_ctx[rhs].serialize_to_str(&protocol.expr_ctx), - "ite(and(not(s), q), three, ite(r, four, ite(s, dont_care, DUT.a)))" - ); + // Concrete branches from both unordered sides are preferred over DontCare, but the + // original node-local DontCare still suppresses node A's own concrete branch. + assert_eq!(expr_str(&protocol, assignment.dont_care), "and(not(r), s)"); + let not_s = protocol.not_guard(s); + let effective_q = protocol.and_guard(not_s, q); + assert_eq!(assignment.concretes, vec![(effective_q, three), (r, four)]); } #[test] @@ -579,12 +583,21 @@ mod tests { let q = protocol.expr_ctx.bv_symbol("q", 1); let r = protocol.expr_ctx.bv_symbol("r", 1); - let q_three = protocol.expr_ctx.ite(q, three, symbol); - let node_a_rhs = protocol.expr_ctx.ite(p, dont_care, q_three); - let node_b_rhs = protocol.expr_ctx.ite(r, three, symbol); let true_id = protocol.true_id(); - let node_a_op = protocol.o(Op::Assign(symbol_id, node_a_rhs)); - let node_b_op = protocol.o(Op::Assign(symbol_id, node_b_rhs)); + let node_a_op = protocol.o(Op::Assign( + symbol_id, + Assignment { + dont_care: p, + concretes: vec![(q, three)], + }, + )); + let node_b_op = protocol.o(Op::Assign( + symbol_id, + Assignment { + dont_care: protocol.false_id(), + concretes: vec![(r, three)], + }, + )); let mut actions = vec![Action::new(true_id, node_a_op)]; let mut internal_assert_guard = None; diff --git a/protocols/src/ir/graph_interpreter.rs b/protocols/src/ir/graph_interpreter.rs index 53528fce..15810cf2 100644 --- a/protocols/src/ir/graph_interpreter.rs +++ b/protocols/src/ir/graph_interpreter.rs @@ -10,7 +10,7 @@ use crate::dut::{PatronusSim, PortId}; use crate::frontend::serialize::serialize_bitvec; use crate::frontend::symbol::{SymbolId, SymbolTable, Type}; use crate::interpreter::Value as WaveValue; -use crate::ir::proto_graph::{Op, ProtoGraph}; +use crate::ir::proto_graph::{Assignment, Op, ProtoGraph}; enum GraphBinding { Sim(PortId), @@ -164,6 +164,26 @@ fn evaluate_input_value( } } +fn evaluate_assignment( + protocol: &ProtoGraph, + store: &SymbolValueStore, + assignment: &Assignment, +) -> InputValue { + if evaluate_guard(protocol, store, assignment.dont_care) { + return InputValue::DontCare; + } + + for (guard, rhs) in &assignment.concretes { + if evaluate_guard(protocol, store, *guard) { + return evaluate_input_value(protocol, store, *rhs); + } + } + + // TODO: make the an internal assert false + // TODO: these should all pass after our analysis pass + panic!("assignment did not match DontCare or any concrete branch") +} + fn evaluate_assert_equal( protocol: &ProtoGraph, store: &SymbolValueStore, @@ -259,19 +279,27 @@ pub fn interpret( // TODO: assignments should be evaluated in a topo order for action in &node.actions { - if let Op::Assign(symbol_id, _) = &pg[action.op] - && !assigned_inputs.insert(*symbol_id) - { - // panic!("multiple assigns to input {symbol_id} in one node"); + if let Op::Assign(symbol_id, _) = &pg[action.op] { + assert_eq!( + action.guard, + pg.true_id(), + "assignment action guards must be 1; path conditions belong in Assignment" + ); + if !assigned_inputs.insert(*symbol_id) { + // panic!("multiple assigns to input {symbol_id} in one node"); + } } } { for action in &node.actions { - if let Op::Assign(symbol_id, expr_ref) = &pg[action.op] - && evaluate_guard(pg, &store, action.guard) - { - let value = evaluate_input_value(pg, &store, *expr_ref); + if let Op::Assign(symbol_id, assignment) = &pg[action.op] { + assert_eq!( + action.guard, + pg.true_id(), + "assignment action guards must be 1; path conditions belong in Assignment" + ); + let value = evaluate_assignment(pg, &store, assignment); pending_inputs.insert(*symbol_id, value); } @@ -286,12 +314,14 @@ pub fn interpret( current_inputs.insert(port, WaveValue::Concrete(bvv)); } InputValue::DontCare => { - let width = match st[symbol_id].tpe() { - Type::BitVec(w) => w, - _ => panic!("expected BitVec type for input {symbol_id}"), - }; - let random_val = BitVecValue::random(&mut rng, width); - sim.set(port, &random_val); + if !matches!(current_inputs.get(&port), Some(WaveValue::DontCare)) { + let width = match st[symbol_id].tpe() { + Type::BitVec(w) => w, + _ => panic!("expected BitVec type for input {symbol_id}"), + }; + let random_val = BitVecValue::random(&mut rng, width); + sim.set(port, &random_val); + } current_inputs.insert(port, WaveValue::DontCare); } } @@ -344,6 +374,7 @@ pub fn interpret( if t.consumes_step { record_waveform(&mut waveform, sim, ¤t_inputs, &mut rng); update_value_store(&mut store, pg, &bindings, sim, &mut rng); + // println!("stepping"); sim.step(); } curr = t.target; diff --git a/protocols/src/ir/graphviz.rs b/protocols/src/ir/graphviz.rs index b8b5f2fa..85d096ad 100644 --- a/protocols/src/ir/graphviz.rs +++ b/protocols/src/ir/graphviz.rs @@ -4,7 +4,7 @@ use crate::frontend::serialize::serialize_bitvec; use crate::frontend::symbol::SymbolTable; -use crate::ir::proto_graph::{NodeId, Op, ProtoGraph}; +use crate::ir::proto_graph::{Assignment, NodeId, Op, ProtoGraph}; use baa::BitVecValue; use patronus::expr::{Expr, ExprRef}; use std::collections::{BTreeSet, VecDeque}; @@ -79,10 +79,10 @@ fn format_op( op_id: crate::ir::proto_graph::OpId, ) -> String { match &protocol[op_id] { - Op::Assign(symbol_id, expr_id) => format!( + Op::Assign(symbol_id, assignment) => format!( "{} := {}", symbols.full_name_from_symbol_id(symbol_id), - format_expr(protocol, *expr_id) + format_assignment(protocol, assignment) ), Op::AssertEq(lhs, rhs) => format!( "assert_eq({}, {})", @@ -95,7 +95,29 @@ fn format_op( } } -fn format_expr(protocol: &ProtoGraph, expr_ref: ExprRef) -> String { +fn format_assignment(protocol: &ProtoGraph, assignment: &Assignment) -> String { + let mut parts = Vec::new(); + if assignment.dont_care != protocol.false_id() { + parts.push(format!( + "X if {}", + format_expr(protocol, assignment.dont_care) + )); + } + for (guard, rhs) in &assignment.concretes { + parts.push(format!( + "{} if {}", + format_expr(protocol, *rhs), + format_expr(protocol, *guard) + )); + } + if parts.is_empty() { + "internal_assert_false".to_string() + } else { + parts.join("; ") + } +} + +pub fn format_expr(protocol: &ProtoGraph, expr_ref: ExprRef) -> String { if protocol.dont_cares.contains(&expr_ref) { "X".to_string() } else { @@ -179,6 +201,8 @@ mod tests { use crate::frontend::diagnostic::DiagnosticHandler; use crate::ir::edge_contract::{contract_edges, normalize_assignments}; use crate::ir::lowering::lower_ast_to_ir; + use crate::ir::propagate_assigns::propagate_assignments; + use crate::ir::reaching_defs::reaching_definitions; use insta::Settings; fn snap(name: &str, filename: &str) { @@ -187,7 +211,7 @@ mod tests { let mut content = String::new(); let st = &ast.st; for proto_ast in ast.protos { - let ir: ProtoGraph = lower_ast_to_ir(proto_ast, st); + let mut ir: ProtoGraph = lower_ast_to_ir(proto_ast, st); content += "== pre-contract ==\n"; content += &to_dot_string(&ir, st); content += "\n"; @@ -199,6 +223,15 @@ mod tests { content += &to_dot_string(&contracted_ir, st); content += "\n"; + // run the reaching definitions analysis + let reaching_defs = reaching_definitions(&mut ir, st); + + // print post-propagation of assignments + propagate_assignments(&mut contracted_ir, st, &reaching_defs); + content += "== post-propagation ==\n"; + content += &to_dot_string(&ir, st); + content += "\n"; + let mut assignment_normalized_ir = contracted_ir.clone(); normalize_assignments(&mut assignment_normalized_ir, st); content += "== post-normalize ==\n"; @@ -212,7 +245,6 @@ mod tests { insta::assert_snapshot!(name, content); }); } - #[test] fn test_add_d1_dot_snapshot() { snap("ir_graphviz_add_d1", "../tests/adders/adder_d1/add_d1.prot"); diff --git a/protocols/src/ir/lowering.rs b/protocols/src/ir/lowering.rs index 467b8714..f598f4b7 100644 --- a/protocols/src/ir/lowering.rs +++ b/protocols/src/ir/lowering.rs @@ -49,6 +49,21 @@ impl<'a> Lowerer<'a> { node_id } + fn dont_care_expr(&mut self, tpe: PatronusType) -> ExprRef { + let next_dont_care = self.ir.dont_cares.len(); + let name = format!("dont_care_{}", next_dont_care); + let dont_care_expr = match tpe { + PatronusType::BV(width) => self.ir.expr_ctx.bv_symbol(&name, width), + PatronusType::Array(array_tpe) => { + self.ir + .expr_ctx + .array_symbol(&name, array_tpe.index_width, array_tpe.data_width) + } + }; + self.ir.dont_cares.insert(dont_care_expr); + dont_care_expr + } + fn lower_expr( &mut self, ast: &Protocol, @@ -58,19 +73,7 @@ impl<'a> Lowerer<'a> { match &ast[expr] { Expr::DontCare => { let tpe = expected.unwrap_or(PatronusType::BV(1)); - let next_dont_care = self.ir.dont_cares.len(); - // the name here is not relevant for anything other than debugging - let name = format!("dont_care_{}", next_dont_care); - let dont_care_expr = match tpe { - PatronusType::BV(width) => self.ir.expr_ctx.bv_symbol(&name, width), - PatronusType::Array(array_tpe) => self.ir.expr_ctx.array_symbol( - &name, - array_tpe.index_width, - array_tpe.data_width, - ), - }; - self.ir.dont_cares.insert(dont_care_expr); - dont_care_expr + self.dont_care_expr(tpe) } Expr::Const(bvv) => self.ir.expr_ctx.bv_lit(bvv), Expr::Sym(sym) => self.lower_symbol(*sym), @@ -173,7 +176,13 @@ impl<'a> Lowerer<'a> { ), }; let rhs_ref = self.lower_expr(ast, expr_id, Some(expected)); - let op_id = self.ir.o(Op::Assign(symbol_id, rhs_ref)); + let assignment = Assignment::from_rhs( + self.ir.false_id(), + self.ir.true_id(), + rhs_ref, + self.ir.dont_cares.contains(&rhs_ref), + ); + let op_id = self.ir.o(Op::Assign(symbol_id, assignment)); let true_id = self.ir.true_id(); self.ir.push_action(node_id, Action::new(true_id, op_id)); self.ir @@ -268,6 +277,25 @@ impl<'a> Lowerer<'a> { } } + fn add_input_dont_care_assignments(&mut self, ast: &Protocol, node_id: NodeId) { + let dut = ast + .ctx + .type_param + .expect("protocol should have a DUT type parameter"); + + for input in self + .symbols + .get_children(&dut) + .into_iter() + .filter(|sym| self.symbols[*sym].is_in_port()) + { + let assignment = Assignment::dont_care(self.ir.true_id()); + let assign = self.ir.o(Op::Assign(input, assignment)); + self.ir + .push_action(node_id, Action::new(self.ir.true_id(), assign)); + } + } + /// lowers an AST into fresh IR nodes which are unconnected to any existing IR nodes /// If `keep_done`, then the exit node has the Done action. /// Returns the nodes, entry, and exit of the lowered fragment @@ -289,8 +317,16 @@ impl<'a> Lowerer<'a> { self.ir.push_action(done, Action::new(true_id, done_op)); } + // relinquish all ports in the exit node + self.add_input_dont_care_assignments(ast, done); + // lower the protocol, which will add the new nodes to self.current_fragment_nodes - let entry = self.lower_stmt(ast, ast.body, done); + let body_entry = self.lower_stmt(ast, ast.body, done); + let entry = self.n(Node::empty()); + self.add_input_dont_care_assignments(ast, entry); + let true_id = self.ir.true_id(); + self.ir + .push_transition(entry, Transition::new(true_id, body_entry, false)); let nodes = std::mem::take(&mut self.current_fragment_nodes); LoweredFragmentInfo { nodes, diff --git a/protocols/src/ir/mod.rs b/protocols/src/ir/mod.rs index 58ba93ca..952141ca 100644 --- a/protocols/src/ir/mod.rs +++ b/protocols/src/ir/mod.rs @@ -3,9 +3,10 @@ pub mod edge_contract; pub mod graph_interpreter; pub mod graphviz; pub mod lowering; +pub mod propagate_assigns; pub mod proto_graph; +pub mod reaching_defs; pub mod trace_lowering; - // TODO: add a function to transform AST to IR // pub fn frontend( // ast : ast::Protocol diff --git a/protocols/src/ir/propagate_assigns.rs b/protocols/src/ir/propagate_assigns.rs new file mode 100644 index 00000000..8a56fc7d --- /dev/null +++ b/protocols/src/ir/propagate_assigns.rs @@ -0,0 +1,111 @@ +use crate::frontend::symbol::{SymbolId, SymbolTable}; +use crate::ir::proto_graph::{Action, NodeId, Op, ProtoGraph}; +use crate::ir::reaching_defs::{ReachingDefs, assignment_is_total}; +use cranelift_entity::EntitySet; +use rustc_hash::FxHashMap; + +// BFS from the entry +fn reachable_node_ids(pg: &ProtoGraph) -> Vec { + let mut visited: EntitySet = EntitySet::default(); + let mut nodes = Vec::new(); + let mut q = vec![pg.entry]; + + while let Some(nid) = q.pop() { + if !visited.insert(nid) { + continue; + } + + nodes.push(nid); + q.extend( + pg[nid] + .transitions + .iter() + .map(|t| t.target) + .filter(|target| !visited.contains(*target)), + ); + } + + nodes +} + +/// check the invariant that for all nodes reachable from the entry that +/// every node has a reaching definition for every port. +fn all_ports_present( + reaching_defs: &FxHashMap, + pg: &ProtoGraph, + st: &SymbolTable, +) -> bool { + let input_ports: Vec = st + .get_children(&pg.proto_ctx.type_param.unwrap()) + .into_iter() + .filter(|sym_id| st[*sym_id].is_in_port()) + .collect(); + + for nid in reachable_node_ids(pg) { + let Some(rd) = reaching_defs.get(&nid) else { + return false; + }; + + if nid == pg.entry && rd.is_empty() { + continue; + } + + for input in &input_ports { + if !rd.contains_key(&st.full_name_from_symbol_id(input).to_string()) { + return false; + } + } + } + + true +} + +pub fn propagate_assignments( + pg: &mut ProtoGraph, + st: &SymbolTable, + rd: &FxHashMap, +) { + assert!( + all_ports_present(rd, pg, st), + "cannot propagate assignments unless all ports are present at all nodes" + ); + + let input_ports: Vec = st + .get_children(&pg.proto_ctx.type_param.unwrap()) + .into_iter() + .filter(|sym_id| st[*sym_id].is_in_port()) + .collect(); + + let node_ids = reachable_node_ids(pg); + + for id in node_ids { + let Some(node_defs) = rd.get(&id) else { + continue; + }; + if id == pg.entry && node_defs.is_empty() { + continue; + } + + let actions = pg[id] + .actions + .iter() + .filter(|&action| !matches!(pg[action.op], Op::Assign(_, _))) + .cloned() + .collect(); + + pg.node_mut(id).actions = actions; + + for input in &input_ports { + let assignment = node_defs + .get(&st.full_name_from_symbol_id(input)) + .unwrap_or_else(|| panic!("missing reaching definition for {input} at {id}")); + assert!( + assignment_is_total(pg, assignment), + "cannot propagate partial assignment for {input} at {id}" + ); + + let op = pg.o(Op::Assign(*input, assignment.clone())); + pg.push_action(id, Action::new(pg.true_id(), op)); + } + } +} diff --git a/protocols/src/ir/proto_graph.rs b/protocols/src/ir/proto_graph.rs index 65270dc4..f12df776 100644 --- a/protocols/src/ir/proto_graph.rs +++ b/protocols/src/ir/proto_graph.rs @@ -80,9 +80,45 @@ impl Node { } } +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Assignment { + pub dont_care: ExprRef, + pub concretes: Vec<(ExprRef, ExprRef)>, +} + +impl Assignment { + pub fn concrete(false_id: ExprRef, guard: ExprRef, rhs: ExprRef) -> Self { + Self { + dont_care: false_id, + concretes: vec![(guard, rhs)], + } + } + + pub fn dont_care(guard: ExprRef) -> Self { + Self { + dont_care: guard, + concretes: vec![], + } + } + + pub fn from_rhs(false_id: ExprRef, guard: ExprRef, rhs: ExprRef, is_dont_care: bool) -> Self { + if is_dont_care { + Self { + dont_care: guard, + concretes: vec![], + } + } else { + Self { + dont_care: false_id, + concretes: vec![(guard, rhs)], + } + } + } +} + #[derive(Debug, Clone, PartialEq, Eq)] pub enum Op { - Assign(SymbolId, ExprRef), + Assign(SymbolId, Assignment), AssertEq(ExprRef, ExprRef), Fork, InternalAssertFalse, @@ -203,8 +239,12 @@ impl ProtoGraph { for (_, op) in self.ops.iter_mut() { match op { - Op::Assign(_, rhs) => { - *rhs = simplifier.simplify(expr_ctx, *rhs); + Op::Assign(_, assignment) => { + assignment.dont_care = simplifier.simplify(expr_ctx, assignment.dont_care); + for (guard, rhs) in &mut assignment.concretes { + *guard = simplifier.simplify(expr_ctx, *guard); + *rhs = simplifier.simplify(expr_ctx, *rhs); + } } Op::AssertEq(lhs, rhs) => { *lhs = simplifier.simplify(expr_ctx, *lhs); @@ -241,7 +281,7 @@ impl ProtoGraph { self.nodes.iter() } - pub(crate) fn node_mut(&mut self, node_id: NodeId) -> &mut Node { + pub fn node_mut(&mut self, node_id: NodeId) -> &mut Node { &mut self.nodes[node_id] } @@ -355,8 +395,8 @@ mod tests { assert_eq!(ir.name, "pipe"); assert_eq!(ir.args.len(), 2); - assert_eq!(ir.nodes.len(), 5); - assert_eq!(ir.ops.len(), 3); + assert_eq!(ir.nodes.len(), 6); + assert_eq!(ir.ops.len(), 5); let entry = &ir.nodes[ir.entry]; assert!(entry.actions.is_empty()); @@ -365,11 +405,24 @@ mod tests { entry.transitions[0], Transition { guard: ir.true_id(), - target: NodeId(4), + target: NodeId(5), consumes_step: false, } ); + let init = &ir.nodes[NodeId(5)]; + assert_eq!(init.actions.len(), 1); + assert_eq!(init.actions[0].guard, ir.true_id()); + assert!(matches!(ir.ops[init.actions[0].op], Op::Assign(_, _))); + assert_eq!( + init.transitions, + vec![Transition { + guard: ir.true_id(), + target: NodeId(4), + consumes_step: false, + }] + ); + let assign = &ir.nodes[NodeId(4)]; assert_eq!(assign.actions.len(), 1); assert_eq!(assign.actions[0].guard, ir.true_id()); @@ -411,9 +464,10 @@ mod tests { ); let exit = &ir.nodes[NodeId(1)]; - assert_eq!(exit.actions.len(), 1); + assert_eq!(exit.actions.len(), 2); assert_eq!(exit.actions[0].guard, ir.true_id()); assert!(matches!(ir.ops[exit.actions[0].op], Op::Done)); + assert!(matches!(ir.ops[exit.actions[1].op], Op::Assign(_, _))); assert!(exit.transitions.is_empty()); } @@ -432,8 +486,20 @@ mod tests { "#, ); - assert_eq!(ir.nodes.len(), 3); - assert_eq!(ir.ops.len(), 2); + assert_eq!(ir.nodes.len(), 4); + assert_eq!(ir.ops.len(), 4); + + let init = &ir.nodes[NodeId(3)]; + assert_eq!(init.actions.len(), 1); + assert!(matches!(ir.ops[init.actions[0].op], Op::Assign(_, _))); + assert_eq!( + init.transitions, + vec![Transition { + guard: ir.true_id(), + target: NodeId(2), + consumes_step: false, + }] + ); let fork = &ir.nodes[NodeId(2)]; assert_eq!(fork.actions.len(), 1); @@ -448,8 +514,9 @@ mod tests { ); let exit = &ir.nodes[NodeId(1)]; - assert_eq!(exit.actions.len(), 1); + assert_eq!(exit.actions.len(), 2); assert!(matches!(ir.ops[exit.actions[0].op], Op::Done)); + assert!(matches!(ir.ops[exit.actions[1].op], Op::Assign(_, _))); assert!(exit.transitions.is_empty()); } @@ -459,13 +526,26 @@ mod tests { assert_eq!(ir.name, "add"); assert_eq!(ir.args.len(), 3); - assert_eq!(ir.nodes.len(), 10); - assert_eq!(ir.ops.len(), 7); + assert_eq!(ir.nodes.len(), 11); + assert_eq!(ir.ops.len(), 11); let entry = &ir.nodes[ir.entry]; assert!(entry.actions.is_empty()); assert_eq!( entry.transitions, + vec![Transition { + guard: ir.true_id(), + target: NodeId(10), + consumes_step: false, + }] + ); + + let init = &ir.nodes[NodeId(10)]; + assert_eq!(init.actions.len(), 2); + assert!(matches!(ir.ops[init.actions[0].op], Op::Assign(_, _))); + assert!(matches!(ir.ops[init.actions[1].op], Op::Assign(_, _))); + assert_eq!( + init.transitions, vec![Transition { guard: ir.true_id(), target: NodeId(9), @@ -508,8 +588,10 @@ mod tests { ); let exit = &ir.nodes[NodeId(1)]; - assert_eq!(exit.actions.len(), 1); + assert_eq!(exit.actions.len(), 3); assert!(matches!(ir.ops[exit.actions[0].op], Op::Done)); + assert!(matches!(ir.ops[exit.actions[1].op], Op::Assign(_, _))); + assert!(matches!(ir.ops[exit.actions[2].op], Op::Assign(_, _))); assert!(exit.transitions.is_empty()); } } diff --git a/protocols/src/ir/reaching_defs.rs b/protocols/src/ir/reaching_defs.rs new file mode 100644 index 00000000..a47f953d --- /dev/null +++ b/protocols/src/ir/reaching_defs.rs @@ -0,0 +1,404 @@ +// Copyright 2026 Cornell University +// released under MIT License +// author: Nikil Shyamunder + +use crate::frontend::symbol::SymbolTable; +use crate::ir::determinize::{SatResult, check_sat}; +use crate::ir::edge_contract::{merge_ordered_assignment, merge_unordered_assignment}; +use crate::ir::proto_graph::{Assignment, NodeId, Op, ProtoGraph}; +use itertools::Itertools; +use patronus::expr::ExprRef; +use rustc_hash::{FxHashMap, FxHashSet}; + +// Maps ports (by their `String` name`), to the existing Assignment for that port +pub type ReachingDefs = FxHashMap; + +/// Nodes only store their outgoing transitions. This function precomputes and returns +/// the in-neighbors for each node that is reachable from the entry. +fn predecessors(pg: &ProtoGraph) -> FxHashMap> { + let mut predecessors: FxHashMap> = FxHashMap::default(); + + for (n, _) in pg.nodes() { + for t in pg[n].clone().transitions { + predecessors.entry(t.target).or_default().push((n, t.guard)); + } + } + + predecessors +} + +fn simplify_guard(pg: &mut ProtoGraph, guard: ExprRef) -> ExprRef { + let (expr_ctx, simplifier) = (&mut pg.expr_ctx, &mut pg.simplifier); + simplifier.simplify(expr_ctx, guard) +} + +// TODO: I feel like this can be done at *merge-time* in edge-contract.rs instead +// TODO: of as a post-processing step +pub fn canonicalize_assignment(pg: &mut ProtoGraph, assignment: Assignment) -> Assignment { + let dont_care = simplify_guard(pg, assignment.dont_care); + if dont_care == pg.true_id() { + return Assignment { + dont_care, + concretes: Vec::new(), + }; + } + + let mut prior = dont_care; + let mut concretes: Vec<(ExprRef, ExprRef)> = Vec::new(); + + for (guard, rhs) in assignment.concretes { + let guard = simplify_guard(pg, guard); + let not_prior = pg.not_guard(prior); + let effective_guard = pg.and_guard(not_prior, guard); + let effective_guard = simplify_guard(pg, effective_guard); + + match check_sat(pg, effective_guard) { + SatResult::DefinitelyUnsat => {} + SatResult::DefinitelySat => { + merge_concrete_guard(pg, &mut concretes, pg.true_id(), rhs); + break; + } + SatResult::MaybeSat => { + merge_concrete_guard(pg, &mut concretes, effective_guard, rhs); + let next_prior = pg.or_guard(prior, effective_guard); + prior = simplify_guard(pg, next_prior); + } + } + + if prior == pg.true_id() { + break; + } + } + + Assignment { + dont_care, + concretes, + } +} + +/// if the `rhs` already exists in `concretes` with guard `old_guard` +/// `guard` should be an *effective* guard, so that performing +/// `old_guard || guard` does not violate merge semantics +fn merge_concrete_guard( + pg: &mut ProtoGraph, + concretes: &mut Vec<(ExprRef, ExprRef)>, + guard: ExprRef, + rhs: ExprRef, +) { + if let Some((existing_guard, _)) = concretes + .iter_mut() + .find(|(_, existing_rhs)| *existing_rhs == rhs) + { + let merged_guard = pg.or_guard(*existing_guard, guard); + *existing_guard = simplify_guard(pg, merged_guard); + } else { + concretes.push((guard, rhs)); + } +} + +/// An assignment is *total* when at least one of it's guards must trigger. +/// That is, `NOT(dc_guard OR concrete_g1 OR ... OR concrete_gn)` is not satisfiable. +pub fn assignment_is_total(pg: &mut ProtoGraph, assignment: &Assignment) -> bool { + let coverage = assignment + .concretes + .iter() + .fold(assignment.dont_care, |coverage, (guard, _)| { + pg.or_guard(coverage, *guard) + }); + + match check_sat(pg, coverage) { + SatResult::DefinitelySat => true, + SatResult::DefinitelyUnsat | SatResult::MaybeSat => false, + } +} + +/// Take `branch_guard`, i.e. a guard on an assignment and simplify it to `Some(g)` +/// under the assumption that `transition_guard` is true. If returns `None` +/// then the branch can be removed. +fn restrict_branch_to_edge( + pg: &mut ProtoGraph, + branch_guard: ExprRef, + transition_guard: ExprRef, +) -> Option { + let overlap = pg.and_guard(branch_guard, transition_guard); + let overlap = simplify_guard(pg, overlap); + + // are `transition_guard` and `branch_guard` mutually exclusive? + if matches!(check_sat(pg, overlap), SatResult::DefinitelyUnsat) { + return None; + } + + // does `transition_guard` imply `branch_guard`? + // t => b == NOT t OR b == NOT(t AND not B). so check t AND not B is unsat. + let not_branch = pg.not_guard(branch_guard); + let transition_without_branch = pg.and_guard(transition_guard, not_branch); + if matches!( + check_sat(pg, transition_without_branch), + SatResult::DefinitelyUnsat + ) { + return Some(pg.true_id()); + } + + // can't simplify, so we have to return the overlap + Some(overlap) +} + +/// For each branch of `assignment`, rewrite it under the assumption that +/// `transition_guard` is true. +fn restrict_assignment_to_edge( + pg: &mut ProtoGraph, + assignment: Assignment, + transition_guard: ExprRef, +) -> Assignment { + let assignment = canonicalize_assignment(pg, assignment); + let dont_care = restrict_branch_to_edge(pg, assignment.dont_care, transition_guard) + .unwrap_or(pg.false_id()); + let concretes = assignment + .concretes + .into_iter() + .filter_map(|(guard, rhs)| { + restrict_branch_to_edge(pg, guard, transition_guard).map(|guard| (guard, rhs)) + }) + .collect(); + + canonicalize_assignment( + pg, + Assignment { + dont_care, + concretes, + }, + ) +} + +/// Returns `true` if this assignment might produce multiple different values +fn has_multiple_outcomes(pg: &mut ProtoGraph, assignment: &Assignment) -> bool { + let canonicalized = canonicalize_assignment(pg, assignment.clone()); + canonicalized.concretes.len() + usize::from(canonicalized.dont_care != pg.false_id()) > 1 +} + +// the binary merge function for reaching definitions analysis is just `merge_unordered_assignment` +fn merge_assignment(pg: &mut ProtoGraph, existing: Assignment, new: Assignment) -> Assignment { + let assignment = merge_unordered_assignment(pg, &mut None, existing, new); + canonicalize_assignment(pg, assignment) +} + +// the binary transfer function for reaching definitions analysis is just `merge_ordered_assignment` +fn transfer_assignment( + pg: &mut ProtoGraph, + existing: Assignment, + assignment: Assignment, +) -> Assignment { + let assignment = merge_ordered_assignment(pg, existing, assignment); + canonicalize_assignment(pg, assignment) +} + +pub fn reaching_definitions( + // TODO: it's a bit of a shame that we have to pass a mutable graph for an analysis, + // but the SAT checker mutates expressions by simplifying them + pg: &mut ProtoGraph, + st: &SymbolTable, +) -> FxHashMap { + let preds = predecessors(pg); + let mut in_defs: FxHashMap = FxHashMap::default(); + let mut out_defs: FxHashMap = FxHashMap::default(); + + // worklist by default is all reachable nodes. + // let mut worklist: Vec = reachable.iter().copied().collect(); + let mut worklist: Vec = pg.nodes().map(|(id, _)| id).collect(); + + while let Some(id) = worklist.pop() { + let mut merged = ReachingDefs::default(); + let mut incoming_conflicts = FxHashSet::default(); + for (pred_id, transition_guard) in preds.get(&id).into_iter().flatten() { + if let Some(pred_defs) = out_defs.get(pred_id) { + for (symbol_name, pred_assignment) in pred_defs { + let assignment = + restrict_assignment_to_edge(pg, pred_assignment.clone(), *transition_guard); + + // don't insert a reaching definition for a fully empty assignment + if assignment.dont_care == pg.false_id() && assignment.concretes.is_empty() { + continue; + } + + merged + .entry(symbol_name.clone()) + .and_modify(|existing| { + *existing = merge_assignment(pg, existing.clone(), assignment.clone()); + if has_multiple_outcomes(pg, existing) { + incoming_conflicts.insert(symbol_name.clone()); + } + }) + .or_insert(assignment); + } + } + } + + if id != pg.entry { + in_defs.insert(id, merged); + } + + let assignments = pg[id] + .actions + .iter() + .filter_map(|a| match pg[a.op].clone() { + Op::Assign(symbol_id, assignment) => Some((symbol_id, assignment)), + _ => None, + }) + .collect::>(); + + let mut out = in_defs.get(&id).cloned().unwrap_or_default(); + + for (symbol_id, assignment) in assignments { + let key = st.full_name_from_symbol_id(&symbol_id).to_string(); + let existing = out.remove(&key).unwrap_or_else(|| Assignment { + dont_care: pg.false_id(), + concretes: Vec::new(), + }); + incoming_conflicts.remove(&key); + out.insert(key, transfer_assignment(pg, existing, assignment)); + } + + assert!( + incoming_conflicts.is_empty(), + "reaching definition conflict remains after transfer at {id}" + ); + + if out_defs.get(&id) != Some(&out) { + out_defs.insert(id, out); + + worklist.extend( + pg[id] + .clone() + .transitions + .into_iter() + .map(|t| t.target) + .unique(), + ); + } + } + + out_defs +} + +pub fn format_reaching_defs( + protocol: &ProtoGraph, + _symbols: &SymbolTable, + reaching_defs: &FxHashMap, +) -> String { + let mut out = String::new(); + let mut node_ids = reaching_defs.keys().copied().collect::>(); + node_ids.sort(); + + for node_id in node_ids { + out.push_str(&format!("{node_id}:\n")); + let Some(defs) = reaching_defs.get(&node_id) else { + continue; + }; + + let mut symbol_defs = defs.iter().collect::>(); + symbol_defs.sort_by_key(|(symbol_name, _)| *symbol_name); + + for (symbol_name, assignment) in symbol_defs { + out.push_str(&format!( + " {}: {}\n", + symbol_name, + format_assignment(protocol, assignment), + )); + } + } + + out +} + +fn format_assignment(protocol: &ProtoGraph, assignment: &Assignment) -> String { + let mut parts = Vec::new(); + if assignment.dont_care != protocol.false_id() { + parts.push(format!( + "X if {}", + crate::ir::graphviz::format_expr(protocol, assignment.dont_care) + )); + } + for (guard, rhs) in &assignment.concretes { + parts.push(format!( + "{} if {}", + crate::ir::graphviz::format_expr(protocol, *rhs), + crate::ir::graphviz::format_expr(protocol, *guard) + )); + } + if parts.is_empty() { + "internal_assert_false".to_string() + } else { + parts.join("; ") + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::frontend::ast::ProtocolContext; + use crate::frontend::symbol::ROOT_SCOPE; + + fn test_graph() -> ProtoGraph { + ProtoGraph::new(ProtocolContext::new("test".into(), ROOT_SCOPE)) + } + + fn concrete_assignment(pg: &ProtoGraph, guard: ExprRef, rhs: ExprRef) -> Assignment { + Assignment::concrete(pg.false_id(), guard, rhs) + } + + #[test] + fn merge_flags_multiple_reaching_concretes_even_when_guards_are_exclusive() { + let mut pg = test_graph(); + let p = pg.expr_ctx.bv_symbol("p", 1); + let not_p = pg.not_guard(p); + let one = pg.expr_ctx.bv_symbol("one", 1); + let zero = pg.expr_ctx.bv_symbol("zero", 1); + + let from_a = concrete_assignment(&pg, p, one); + let from_b = concrete_assignment(&pg, not_p, zero); + + let merged = merge_assignment(&mut pg, from_a, from_b); + + assert!(has_multiple_outcomes(&mut pg, &merged)); + assert_eq!(merged.dont_care, pg.false_id()); + assert_eq!(merged.concretes.len(), 2); + } + + #[test] + fn merge_flags_maybe_overlapping_reaching_definitions() { + let mut pg = test_graph(); + let p = pg.expr_ctx.bv_symbol("p", 1); + let q = pg.expr_ctx.bv_symbol("q", 1); + let one = pg.expr_ctx.bv_symbol("one", 1); + let zero = pg.expr_ctx.bv_symbol("zero", 1); + + let from_a = concrete_assignment(&pg, p, one); + let from_b = concrete_assignment(&pg, q, zero); + + let merged = merge_assignment(&mut pg, from_a, from_b); + + assert!(has_multiple_outcomes(&mut pg, &merged)); + assert_eq!(merged.dont_care, pg.false_id()); + assert_eq!(merged.concretes.len(), 2); + } + + #[test] + fn total_assignment_kills_incoming_reaching_definition_conflict() { + let mut pg = test_graph(); + let p = pg.expr_ctx.bv_symbol("p", 1); + let q = pg.expr_ctx.bv_symbol("q", 1); + let one = pg.expr_ctx.bv_symbol("one", 1); + let zero = pg.expr_ctx.bv_symbol("zero", 1); + let two = pg.expr_ctx.bv_symbol("two", 1); + + let from_a = concrete_assignment(&pg, p, one); + let from_b = concrete_assignment(&pg, q, zero); + let conflicted = merge_assignment(&mut pg, from_a, from_b); + assert!(has_multiple_outcomes(&mut pg, &conflicted)); + + let reassignment = concrete_assignment(&pg, pg.true_id(), two); + let transferred = transfer_assignment(&mut pg, conflicted, reassignment); + + assert!(assignment_is_total(&mut pg, &transferred)); + } +} diff --git a/protocols/src/ir/trace_lowering.rs b/protocols/src/ir/trace_lowering.rs index 8cb27fec..dd5c0b88 100644 --- a/protocols/src/ir/trace_lowering.rs +++ b/protocols/src/ir/trace_lowering.rs @@ -9,7 +9,7 @@ use rustc_hash::FxHashMap; use crate::Value; use crate::frontend::ast::Protocol; use crate::frontend::symbol::SymbolTable; -use crate::ir::edge_contract::{append_action, contract_edges}; +use crate::ir::edge_contract::{append_action, contract_edges, guard_assignment}; use crate::ir::lowering::{LoweredFragmentInfo, Lowerer, TraceArgSubst}; use crate::ir::proto_graph::{Action, NodeId, Op, ProtoGraph, Transition}; @@ -79,8 +79,23 @@ impl<'a> Lowerer<'a> { let mut internal_assert_guard = None; for action in entry_actions { - let guard = self.ir.and_guard(graft_guard, action.guard); - let guarded_action = action.with_guard(guard); + let guarded_action = match self.ir[action.op].clone() { + Op::Assign(symbol_id, assignment) => { + assert_eq!( + action.guard, + self.ir.true_id(), + "assignment action guards must be 1; path conditions belong in Assignment" + ); + let guarded_assignment = + guard_assignment(&mut self.ir, assignment, graft_guard); + let guarded_op = self.ir.o(Op::Assign(symbol_id, guarded_assignment)); + Action::new(self.ir.true_id(), guarded_op) + } + _ => { + let guard = self.ir.and_guard(graft_guard, action.guard); + action.with_guard(guard) + } + }; append_action( &mut self.ir, self.symbols, @@ -169,6 +184,7 @@ pub fn lower_trace_to_ir( .ir .push_transition(entry_node, Transition::new(true_id, first.entry, false)); contract_edges(&mut lowerer.ir, symbols); + // normalize_assignments(&mut lowerer.ir, symbols); // pass in the initial IR with the first transaction and its graft points, and append_trace_transactions will lower the rest of the trace from here. let graft_points = lowerer.next_trace_graft_points(&first); diff --git a/protocols/src/tests/snapshots/protocols__frontend__serialize__tests__add_d1.snap b/protocols/src/tests/snapshots/protocols__frontend__serialize__tests__add_d1.snap index 3b916297..6c8470fb 100644 --- a/protocols/src/tests/snapshots/protocols__frontend__serialize__tests__add_d1.snap +++ b/protocols/src/tests/snapshots/protocols__frontend__serialize__tests__add_d1.snap @@ -76,6 +76,19 @@ prot assign_after_observation(a: u32, b: u32, s: u32) { step(); } +prot better_if_else(a: u32, b: u32) { + DUT.a := a; + DUT.b := b; + step(); + if DUT.s == 32'd0 { + DUT.a := X; + } else { + DUT.a := 32'd5; + } + fork(); + step(); +} + prot if_else(a1: u32, a2: u32) { if 1'd1 { DUT.a := a1; diff --git a/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_add_d0.snap b/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_add_d0.snap index 2d38ed69..d168a320 100644 --- a/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_add_d0.snap +++ b/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_add_d0.snap @@ -9,12 +9,14 @@ digraph "add_combinational_illegal_observation_in_conditional" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node9 [label="1"]; - node9 [label="[1] DUT.a := X"]; + node0 -> node10 [label="1"]; + node10 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node10 -> node9 [label="1"]; + node9 [label="[1] DUT.a := X if 1"]; node9 -> node8 [label="1"]; - node8 [label="[1] DUT.b := X"]; + node8 [label="[1] DUT.b := X if 1"]; node8 -> node7 [label="1"]; - node7 [label="[1] DUT.a := a"]; + node7 [label="[1] DUT.a := a if 1"]; node7 -> node6 [label="1"]; node6 [label=""]; node6 -> node4 [label="eq(DUT.s, 0)"]; @@ -27,7 +29,7 @@ digraph "add_combinational_illegal_observation_in_conditional" { node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-contract == @@ -36,10 +38,40 @@ digraph "add_combinational_illegal_observation_in_conditional" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := X"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := X if 1"]; node0 -> node1 [label="eq(DUT.s, 0) / step"]; node0 -> node1 [label="not(eq(DUT.s, 0)) / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-propagation == +digraph "add_combinational_illegal_observation_in_conditional" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node10 [label="1"]; + node10 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node10 -> node9 [label="1"]; + node9 [label="[1] DUT.a := X if 1"]; + node9 -> node8 [label="1"]; + node8 [label="[1] DUT.b := X if 1"]; + node8 -> node7 [label="1"]; + node7 [label="[1] DUT.a := a if 1"]; + node7 -> node6 [label="1"]; + node6 [label=""]; + node6 -> node4 [label="eq(DUT.s, 0)"]; + node6 -> node5 [label="not(eq(DUT.s, 0))"]; + node4 [label=""]; + node4 -> node3 [label="1"]; + node5 [label=""]; + node5 -> node3 [label="1"]; + node3 [label=""]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-normalize == @@ -48,10 +80,10 @@ digraph "add_combinational_illegal_observation_in_conditional" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := X"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := X if 1"]; node0 -> node1 [label="eq(DUT.s, 0) / step"]; node0 -> node1 [label="not(eq(DUT.s, 0)) / step"]; - node1 [label="[1] done\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == pre-contract == @@ -61,18 +93,20 @@ digraph "add_combinational_illegal_observation_in_assertion" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node6 [label="1"]; - node6 [label="[1] DUT.a := X"]; + node0 -> node7 [label="1"]; + node7 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node7 -> node6 [label="1"]; + node6 [label="[1] DUT.a := X if 1"]; node6 -> node5 [label="1"]; - node5 [label="[1] DUT.b := X"]; + node5 [label="[1] DUT.b := X if 1"]; node5 -> node4 [label="1"]; - node4 [label="[1] DUT.a := a"]; + node4 [label="[1] DUT.a := a if 1"]; node4 -> node3 [label="1"]; node3 [label="[1] assert_eq(DUT.s, s)"]; node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-contract == @@ -81,9 +115,32 @@ digraph "add_combinational_illegal_observation_in_assertion" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := X\n[1] assert_eq(DUT.s, s)"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := X if 1\n[1] assert_eq(DUT.s, s)"]; node0 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-propagation == +digraph "add_combinational_illegal_observation_in_assertion" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node7 [label="1"]; + node7 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node7 -> node6 [label="1"]; + node6 [label="[1] DUT.a := X if 1"]; + node6 -> node5 [label="1"]; + node5 [label="[1] DUT.b := X if 1"]; + node5 -> node4 [label="1"]; + node4 [label="[1] DUT.a := a if 1"]; + node4 -> node3 [label="1"]; + node3 [label="[1] assert_eq(DUT.s, s)"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-normalize == @@ -92,9 +149,9 @@ digraph "add_combinational_illegal_observation_in_assertion" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := X\n[1] assert_eq(DUT.s, s)"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := X if 1\n[1] assert_eq(DUT.s, s)"]; node0 -> node1 [label="1 / step"]; - node1 [label="[1] done\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == pre-contract == @@ -104,11 +161,13 @@ digraph "add_combinational_legal_observation_illegal_assignment" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node6 [label="1"]; + node0 -> node7 [label="1"]; + node7 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node7 -> node6 [label="1"]; node6 [label=""]; node6 -> node4 [label="eq(DUT.s, 0)"]; node6 -> node5 [label="not(eq(DUT.s, 0))"]; - node4 [label="[1] DUT.a := a"]; + node4 [label="[1] DUT.a := a if 1"]; node4 -> node3 [label="1"]; node5 [label=""]; node5 -> node3 [label="1"]; @@ -116,7 +175,7 @@ digraph "add_combinational_legal_observation_illegal_assignment" { node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-contract == @@ -125,10 +184,34 @@ digraph "add_combinational_legal_observation_illegal_assignment" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[eq(DUT.s, 0)] DUT.a := a"]; + node0 [label="[1] DUT.a := X if not(eq(DUT.s, 0)); a if eq(DUT.s, 0)\n[1] DUT.b := X if 1"]; node0 -> node1 [label="eq(DUT.s, 0) / step"]; node0 -> node1 [label="not(eq(DUT.s, 0)) / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-propagation == +digraph "add_combinational_legal_observation_illegal_assignment" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node7 [label="1"]; + node7 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node7 -> node6 [label="1"]; + node6 [label=""]; + node6 -> node4 [label="eq(DUT.s, 0)"]; + node6 -> node5 [label="not(eq(DUT.s, 0))"]; + node4 [label="[1] DUT.a := a if 1"]; + node4 -> node3 [label="1"]; + node5 [label=""]; + node5 -> node3 [label="1"]; + node3 [label=""]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-normalize == @@ -137,10 +220,10 @@ digraph "add_combinational_legal_observation_illegal_assignment" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[eq(DUT.s, 0)] DUT.a := a\n[1] DUT.b := DUT.b"]; + node0 [label="[1] DUT.a := X if not(eq(DUT.s, 0)); a if eq(DUT.s, 0)\n[1] DUT.b := X if 1"]; node0 -> node1 [label="eq(DUT.s, 0) / step"]; node0 -> node1 [label="not(eq(DUT.s, 0)) / step"]; - node1 [label="[1] done\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == pre-contract == @@ -150,16 +233,18 @@ digraph "add_combinational" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node5 [label="1"]; - node5 [label="[1] DUT.a := a"]; + node0 -> node6 [label="1"]; + node6 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node6 -> node5 [label="1"]; + node5 [label="[1] DUT.a := a if 1"]; node5 -> node4 [label="1"]; - node4 [label="[1] DUT.b := b"]; + node4 [label="[1] DUT.b := b if 1"]; node4 -> node3 [label="1"]; node3 [label="[1] assert_eq(s, DUT.s)"]; node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-contract == @@ -168,9 +253,30 @@ digraph "add_combinational" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := b\n[1] assert_eq(s, DUT.s)"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1\n[1] assert_eq(s, DUT.s)"]; node0 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-propagation == +digraph "add_combinational" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node6 [label="1"]; + node6 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node6 -> node5 [label="1"]; + node5 [label="[1] DUT.a := a if 1"]; + node5 -> node4 [label="1"]; + node4 [label="[1] DUT.b := b if 1"]; + node4 -> node3 [label="1"]; + node3 [label="[1] assert_eq(s, DUT.s)"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-normalize == @@ -179,7 +285,7 @@ digraph "add_combinational" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := b\n[1] assert_eq(s, DUT.s)"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1\n[1] assert_eq(s, DUT.s)"]; node0 -> node1 [label="1 / step"]; - node1 [label="[1] done\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } diff --git a/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_add_d1.snap b/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_add_d1.snap index 6420055b..bc21aeb5 100644 --- a/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_add_d1.snap +++ b/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_add_d1.snap @@ -1,6 +1,5 @@ --- source: protocols/src/ir/graphviz.rs -assertion_line: 212 expression: content --- == pre-contract == @@ -10,16 +9,18 @@ digraph "add" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node9 [label="1"]; - node9 [label="[1] DUT.a := a"]; + node0 -> node10 [label="1"]; + node10 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node10 -> node9 [label="1"]; + node9 [label="[1] DUT.a := a if 1"]; node9 -> node8 [label="1"]; - node8 [label="[1] DUT.b := b"]; + node8 [label="[1] DUT.b := b if 1"]; node8 -> node7 [label="1"]; node7 [label=""]; node7 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := X"]; + node6 [label="[1] DUT.a := X if 1"]; node6 -> node5 [label="1"]; - node5 [label="[1] DUT.b := X"]; + node5 [label="[1] DUT.b := X if 1"]; node5 -> node4 [label="1"]; node4 [label="[1] assert_eq(s, DUT.s)"]; node4 -> node3 [label="1"]; @@ -27,7 +28,7 @@ digraph "add" { node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-contract == @@ -36,11 +37,40 @@ digraph "add" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := b"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node0 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := X\n[1] DUT.b := X\n[1] assert_eq(s, DUT.s)\n[1] fork"]; + node6 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1\n[1] assert_eq(s, DUT.s)\n[1] fork"]; node6 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-propagation == +digraph "add" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node10 [label="1"]; + node10 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node10 -> node9 [label="1"]; + node9 [label="[1] DUT.a := a if 1"]; + node9 -> node8 [label="1"]; + node8 [label="[1] DUT.b := b if 1"]; + node8 -> node7 [label="1"]; + node7 [label=""]; + node7 -> node6 [label="1 / step"]; + node6 [label="[1] DUT.a := X if 1"]; + node6 -> node5 [label="1"]; + node5 [label="[1] DUT.b := X if 1"]; + node5 -> node4 [label="1"]; + node4 [label="[1] assert_eq(s, DUT.s)"]; + node4 -> node3 [label="1"]; + node3 [label="[1] fork"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-normalize == @@ -49,11 +79,11 @@ digraph "add" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := b"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node0 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := X\n[1] DUT.b := X\n[1] assert_eq(s, DUT.s)\n[1] fork"]; + node6 [label="[1] assert_eq(s, DUT.s)\n[1] fork\n[1] DUT.a := X if 1\n[1] DUT.b := b if 1"]; node6 -> node1 [label="1 / step"]; - node1 [label="[1] done\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == pre-contract == @@ -63,24 +93,26 @@ digraph "add_fork_early" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node9 [label="1"]; - node9 [label="[1] DUT.a := a"]; + node0 -> node10 [label="1"]; + node10 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node10 -> node9 [label="1"]; + node9 [label="[1] DUT.a := a if 1"]; node9 -> node8 [label="1"]; - node8 [label="[1] DUT.b := b"]; + node8 [label="[1] DUT.b := b if 1"]; node8 -> node7 [label="1"]; node7 [label=""]; node7 -> node6 [label="1 / step"]; node6 [label="[1] fork"]; node6 -> node5 [label="1"]; - node5 [label="[1] DUT.a := X"]; + node5 [label="[1] DUT.a := X if 1"]; node5 -> node4 [label="1"]; - node4 [label="[1] DUT.b := X"]; + node4 [label="[1] DUT.b := X if 1"]; node4 -> node3 [label="1"]; node3 [label="[1] assert_eq(s, DUT.s)"]; node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-contract == @@ -89,11 +121,40 @@ digraph "add_fork_early" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := b"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node0 -> node6 [label="1 / step"]; - node6 [label="[1] fork\n[1] DUT.a := X\n[1] DUT.b := X\n[1] assert_eq(s, DUT.s)"]; + node6 [label="[1] fork\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1\n[1] assert_eq(s, DUT.s)"]; node6 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-propagation == +digraph "add_fork_early" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node10 [label="1"]; + node10 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node10 -> node9 [label="1"]; + node9 [label="[1] DUT.a := a if 1"]; + node9 -> node8 [label="1"]; + node8 [label="[1] DUT.b := b if 1"]; + node8 -> node7 [label="1"]; + node7 [label=""]; + node7 -> node6 [label="1 / step"]; + node6 [label="[1] fork"]; + node6 -> node5 [label="1"]; + node5 [label="[1] DUT.a := X if 1"]; + node5 -> node4 [label="1"]; + node4 [label="[1] DUT.b := X if 1"]; + node4 -> node3 [label="1"]; + node3 [label="[1] assert_eq(s, DUT.s)"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-normalize == @@ -102,11 +163,11 @@ digraph "add_fork_early" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := b"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node0 -> node6 [label="1 / step"]; - node6 [label="[1] fork\n[1] DUT.a := X\n[1] DUT.b := X\n[1] assert_eq(s, DUT.s)"]; + node6 [label="[1] fork\n[1] assert_eq(s, DUT.s)\n[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node6 -> node1 [label="1 / step"]; - node1 [label="[1] done\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == pre-contract == @@ -116,16 +177,18 @@ digraph "add_incorrect" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node9 [label="1"]; - node9 [label="[1] DUT.a := a"]; + node0 -> node10 [label="1"]; + node10 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node10 -> node9 [label="1"]; + node9 [label="[1] DUT.a := a if 1"]; node9 -> node8 [label="1"]; - node8 [label="[1] DUT.b := b"]; + node8 [label="[1] DUT.b := b if 1"]; node8 -> node7 [label="1"]; node7 [label=""]; node7 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := a"]; + node6 [label="[1] DUT.a := a if 1"]; node6 -> node5 [label="1"]; - node5 [label="[1] DUT.b := b"]; + node5 [label="[1] DUT.b := b if 1"]; node5 -> node4 [label="1"]; node4 [label="[1] assert_eq(s, DUT.s)"]; node4 -> node3 [label="1"]; @@ -133,7 +196,7 @@ digraph "add_incorrect" { node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-contract == @@ -142,11 +205,40 @@ digraph "add_incorrect" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := b"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node0 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := a\n[1] DUT.b := b\n[1] assert_eq(s, DUT.s)\n[1] fork"]; + node6 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1\n[1] assert_eq(s, DUT.s)\n[1] fork"]; node6 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-propagation == +digraph "add_incorrect" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node10 [label="1"]; + node10 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node10 -> node9 [label="1"]; + node9 [label="[1] DUT.a := a if 1"]; + node9 -> node8 [label="1"]; + node8 [label="[1] DUT.b := b if 1"]; + node8 -> node7 [label="1"]; + node7 [label=""]; + node7 -> node6 [label="1 / step"]; + node6 [label="[1] DUT.a := a if 1"]; + node6 -> node5 [label="1"]; + node5 [label="[1] DUT.b := b if 1"]; + node5 -> node4 [label="1"]; + node4 [label="[1] assert_eq(s, DUT.s)"]; + node4 -> node3 [label="1"]; + node3 [label="[1] fork"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-normalize == @@ -155,11 +247,11 @@ digraph "add_incorrect" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := b"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node0 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := a\n[1] DUT.b := b\n[1] assert_eq(s, DUT.s)\n[1] fork"]; + node6 [label="[1] assert_eq(s, DUT.s)\n[1] fork\n[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node6 -> node1 [label="1 / step"]; - node1 [label="[1] done\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == pre-contract == @@ -169,10 +261,12 @@ digraph "add_incorrect_implicit" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node7 [label="1"]; - node7 [label="[1] DUT.a := a"]; + node0 -> node8 [label="1"]; + node8 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node8 -> node7 [label="1"]; + node7 [label="[1] DUT.a := a if 1"]; node7 -> node6 [label="1"]; - node6 [label="[1] DUT.b := b"]; + node6 [label="[1] DUT.b := b if 1"]; node6 -> node5 [label="1"]; node5 [label=""]; node5 -> node4 [label="1 / step"]; @@ -182,7 +276,7 @@ digraph "add_incorrect_implicit" { node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-contract == @@ -191,11 +285,36 @@ digraph "add_incorrect_implicit" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := b"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node0 -> node4 [label="1 / step"]; node4 [label="[1] assert_eq(s, DUT.s)\n[1] fork"]; node4 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-propagation == +digraph "add_incorrect_implicit" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node8 [label="1"]; + node8 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node8 -> node7 [label="1"]; + node7 [label="[1] DUT.a := a if 1"]; + node7 -> node6 [label="1"]; + node6 [label="[1] DUT.b := b if 1"]; + node6 -> node5 [label="1"]; + node5 [label=""]; + node5 -> node4 [label="1 / step"]; + node4 [label="[1] assert_eq(s, DUT.s)"]; + node4 -> node3 [label="1"]; + node3 [label="[1] fork"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-normalize == @@ -204,11 +323,11 @@ digraph "add_incorrect_implicit" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a\n[1] DUT.b := b"]; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node0 -> node4 [label="1 / step"]; - node4 [label="[1] assert_eq(s, DUT.s)\n[1] fork\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node4 [label="[1] assert_eq(s, DUT.s)\n[1] fork\n[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node4 -> node1 [label="1 / step"]; - node1 [label="[1] done\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == pre-contract == @@ -218,16 +337,18 @@ digraph "wait_and_add" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node9 [label="1"]; + node0 -> node10 [label="1"]; + node10 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node10 -> node9 [label="1"]; node9 [label=""]; node9 -> node8 [label="1 / step"]; node8 [label="[1] fork"]; node8 -> node7 [label="1"]; node7 [label=""]; node7 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := a"]; + node6 [label="[1] DUT.a := a if 1"]; node6 -> node5 [label="1"]; - node5 [label="[1] DUT.b := b"]; + node5 [label="[1] DUT.b := b if 1"]; node5 -> node4 [label="1"]; node4 [label=""]; node4 -> node3 [label="1 / step"]; @@ -235,7 +356,7 @@ digraph "wait_and_add" { node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-contract == @@ -244,15 +365,44 @@ digraph "wait_and_add" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label=""]; + node0 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; node0 -> node8 [label="1 / step"]; node8 [label="[1] fork"]; node8 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := a\n[1] DUT.b := b"]; + node6 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node6 -> node3 [label="1 / step"]; node3 [label="[1] assert_eq(s, DUT.s)"]; node3 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-propagation == +digraph "wait_and_add" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node10 [label="1"]; + node10 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node10 -> node9 [label="1"]; + node9 [label=""]; + node9 -> node8 [label="1 / step"]; + node8 [label="[1] fork"]; + node8 -> node7 [label="1"]; + node7 [label=""]; + node7 -> node6 [label="1 / step"]; + node6 [label="[1] DUT.a := a if 1"]; + node6 -> node5 [label="1"]; + node5 [label="[1] DUT.b := b if 1"]; + node5 -> node4 [label="1"]; + node4 [label=""]; + node4 -> node3 [label="1 / step"]; + node3 [label="[1] assert_eq(s, DUT.s)"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-normalize == @@ -261,15 +411,15 @@ digraph "wait_and_add" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node0 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; node0 -> node8 [label="1 / step"]; - node8 [label="[1] fork\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node8 [label="[1] fork\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; node8 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := a\n[1] DUT.b := b"]; + node6 [label="[1] DUT.a := a if 1\n[1] DUT.b := X if 1"]; node6 -> node3 [label="1 / step"]; - node3 [label="[1] assert_eq(s, DUT.s)\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node3 [label="[1] assert_eq(s, DUT.s)\n[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; node3 -> node1 [label="1 / step"]; - node1 [label="[1] done\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == pre-contract == @@ -279,25 +429,27 @@ digraph "assign_after_observation" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node13 [label="1"]; - node13 [label="[1] DUT.a := a"]; + node0 -> node14 [label="1"]; + node14 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node14 -> node13 [label="1"]; + node13 [label="[1] DUT.a := a if 1"]; node13 -> node12 [label="1"]; node12 [label=""]; node12 -> node10 [label="eq(DUT.a, 2)"]; node12 -> node11 [label="not(eq(DUT.a, 2))"]; - node10 [label="[1] DUT.a := 0"]; + node10 [label="[1] DUT.a := 0 if 1"]; node10 -> node9 [label="1"]; node11 [label=""]; node11 -> node9 [label="1"]; node9 [label=""]; node9 -> node8 [label="1"]; - node8 [label="[1] DUT.b := b"]; + node8 [label="[1] DUT.b := b if 1"]; node8 -> node7 [label="1"]; node7 [label=""]; node7 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := X"]; + node6 [label="[1] DUT.a := X if 1"]; node6 -> node5 [label="1"]; - node5 [label="[1] DUT.b := X"]; + node5 [label="[1] DUT.b := X if 1"]; node5 -> node4 [label="1"]; node4 [label="[1] assert_eq(s, DUT.s)"]; node4 -> node3 [label="1"]; @@ -305,7 +457,7 @@ digraph "assign_after_observation" { node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-contract == @@ -314,12 +466,50 @@ digraph "assign_after_observation" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := ite(eq(DUT.a, 2), 0, a)\n[1] DUT.b := ite(eq(DUT.a, 2), b, ite(not(eq(DUT.a, 2)), b, DUT.b))"]; + node0 [label="[1] DUT.a := 0 if eq(DUT.a, 2); a if 1\n[1] DUT.b := b if eq(DUT.a, 2); b if not(eq(DUT.a, 2))"]; node0 -> node6 [label="eq(DUT.a, 2) / step"]; node0 -> node6 [label="not(eq(DUT.a, 2)) / step"]; - node6 [label="[1] DUT.a := X\n[1] DUT.b := X\n[1] assert_eq(s, DUT.s)\n[1] fork"]; + node6 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1\n[1] assert_eq(s, DUT.s)\n[1] fork"]; node6 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-propagation == +digraph "assign_after_observation" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node14 [label="1"]; + node14 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node14 -> node13 [label="1"]; + node13 [label="[1] DUT.a := a if 1"]; + node13 -> node12 [label="1"]; + node12 [label=""]; + node12 -> node10 [label="eq(DUT.a, 2)"]; + node12 -> node11 [label="not(eq(DUT.a, 2))"]; + node10 [label="[1] DUT.a := 0 if 1"]; + node10 -> node9 [label="1"]; + node11 [label=""]; + node11 -> node9 [label="1"]; + node9 [label=""]; + node9 -> node8 [label="1"]; + node8 [label="[1] DUT.b := b if 1"]; + node8 -> node7 [label="1"]; + node7 [label=""]; + node7 -> node6 [label="1 / step"]; + node6 [label="[1] DUT.a := X if 1"]; + node6 -> node5 [label="1"]; + node5 [label="[1] DUT.b := X if 1"]; + node5 -> node4 [label="1"]; + node4 [label="[1] assert_eq(s, DUT.s)"]; + node4 -> node3 [label="1"]; + node3 [label="[1] fork"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-normalize == @@ -328,12 +518,104 @@ digraph "assign_after_observation" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := ite(eq(DUT.a, 2), 0, a)\n[1] DUT.b := ite(eq(DUT.a, 2), b, ite(not(eq(DUT.a, 2)), b, DUT.b))"]; + node0 [label="[1] DUT.a := 0 if eq(DUT.a, 2); a if 1\n[1] DUT.b := b if eq(DUT.a, 2); b if not(eq(DUT.a, 2))"]; node0 -> node6 [label="eq(DUT.a, 2) / step"]; node0 -> node6 [label="not(eq(DUT.a, 2)) / step"]; - node6 [label="[1] DUT.a := X\n[1] DUT.b := X\n[1] assert_eq(s, DUT.s)\n[1] fork"]; + node6 [label="[1] assert_eq(s, DUT.s)\n[1] fork\n[1] DUT.a := X if 1\n[1] DUT.b := b if 1"]; node6 -> node1 [label="1 / step"]; - node1 [label="[1] done\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== pre-contract == +digraph "better_if_else" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node11 [label="1"]; + node11 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node11 -> node10 [label="1"]; + node10 [label="[1] DUT.a := a if 1"]; + node10 -> node9 [label="1"]; + node9 [label="[1] DUT.b := b if 1"]; + node9 -> node8 [label="1"]; + node8 [label=""]; + node8 -> node7 [label="1 / step"]; + node7 [label=""]; + node7 -> node5 [label="eq(DUT.s, 0)"]; + node7 -> node6 [label="not(eq(DUT.s, 0))"]; + node5 [label="[1] DUT.a := X if 1"]; + node5 -> node4 [label="1"]; + node6 [label="[1] DUT.a := 5 if 1"]; + node6 -> node4 [label="1"]; + node4 [label=""]; + node4 -> node3 [label="1"]; + node3 [label="[1] fork"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-contract == +digraph "better_if_else" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; + node0 -> node7 [label="1 / step"]; + node7 [label="[1] DUT.a := X if eq(DUT.s, 0); 5 if not(eq(DUT.s, 0))\n[1] fork\n[0] internal_assert_false"]; + node7 -> node1 [label="not(eq(DUT.s, 0)) / step"]; + node7 -> node1 [label="eq(DUT.s, 0) / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-propagation == +digraph "better_if_else" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node11 [label="1"]; + node11 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node11 -> node10 [label="1"]; + node10 [label="[1] DUT.a := a if 1"]; + node10 -> node9 [label="1"]; + node9 [label="[1] DUT.b := b if 1"]; + node9 -> node8 [label="1"]; + node8 [label=""]; + node8 -> node7 [label="1 / step"]; + node7 [label=""]; + node7 -> node5 [label="eq(DUT.s, 0)"]; + node7 -> node6 [label="not(eq(DUT.s, 0))"]; + node5 [label="[1] DUT.a := X if 1"]; + node5 -> node4 [label="1"]; + node6 [label="[1] DUT.a := 5 if 1"]; + node6 -> node4 [label="1"]; + node4 [label=""]; + node4 -> node3 [label="1"]; + node3 [label="[1] fork"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-normalize == +digraph "better_if_else" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label="[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; + node0 -> node7 [label="1 / step"]; + node7 [label="[1] fork\n[0] internal_assert_false\n[1] DUT.a := a if 1\n[1] DUT.b := b if 1"]; + node7 -> node1 [label="not(eq(DUT.s, 0)) / step"]; + node7 -> node1 [label="eq(DUT.s, 0) / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == pre-contract == @@ -343,20 +625,22 @@ digraph "if_else" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node12 [label="1"]; + node0 -> node13 [label="1"]; + node13 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node13 -> node12 [label="1"]; node12 [label=""]; node12 -> node10 [label="1"]; - node10 [label="[1] DUT.a := a1"]; + node10 [label="[1] DUT.a := a1 if 1"]; node10 -> node9 [label="1"]; node9 [label=""]; node9 -> node8 [label="1"]; - node8 [label="[1] DUT.b := 0"]; + node8 [label="[1] DUT.b := 0 if 1"]; node8 -> node7 [label="1"]; node7 [label=""]; node7 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := X"]; + node6 [label="[1] DUT.a := X if 1"]; node6 -> node5 [label="1"]; - node5 [label="[1] DUT.b := X"]; + node5 [label="[1] DUT.b := X if 1"]; node5 -> node4 [label="1"]; node4 [label="[1] assert_eq(a1, DUT.s)"]; node4 -> node3 [label="1"]; @@ -364,7 +648,7 @@ digraph "if_else" { node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-contract == @@ -373,11 +657,44 @@ digraph "if_else" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a1\n[1] DUT.b := 0"]; + node0 [label="[1] DUT.a := a1 if 1\n[1] DUT.b := 0 if 1"]; node0 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := X\n[1] DUT.b := X\n[1] assert_eq(a1, DUT.s)\n[1] fork"]; + node6 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1\n[1] assert_eq(a1, DUT.s)\n[1] fork"]; node6 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; +} + +== post-propagation == +digraph "if_else" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node13 [label="1"]; + node13 [label="[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; + node13 -> node12 [label="1"]; + node12 [label=""]; + node12 -> node10 [label="1"]; + node10 [label="[1] DUT.a := a1 if 1"]; + node10 -> node9 [label="1"]; + node9 [label=""]; + node9 -> node8 [label="1"]; + node8 [label="[1] DUT.b := 0 if 1"]; + node8 -> node7 [label="1"]; + node7 [label=""]; + node7 -> node6 [label="1 / step"]; + node6 [label="[1] DUT.a := X if 1"]; + node6 -> node5 [label="1"]; + node5 [label="[1] DUT.b := X if 1"]; + node5 -> node4 [label="1"]; + node4 [label="[1] assert_eq(a1, DUT.s)"]; + node4 -> node3 [label="1"]; + node3 [label="[1] fork"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } == post-normalize == @@ -386,9 +703,9 @@ digraph "if_else" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] DUT.a := a1\n[1] DUT.b := 0"]; + node0 [label="[1] DUT.a := a1 if 1\n[1] DUT.b := 0 if 1"]; node0 -> node6 [label="1 / step"]; - node6 [label="[1] DUT.a := X\n[1] DUT.b := X\n[1] assert_eq(a1, DUT.s)\n[1] fork"]; + node6 [label="[1] assert_eq(a1, DUT.s)\n[1] fork\n[1] DUT.a := X if 1\n[1] DUT.b := 0 if 1"]; node6 -> node1 [label="1 / step"]; - node1 [label="[1] done\n[1] DUT.a := DUT.a\n[1] DUT.b := DUT.b"]; + node1 [label="[1] done\n[1] DUT.a := X if 1\n[1] DUT.b := X if 1"]; } diff --git a/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_axis_truncated_include_idle_send_data.snap b/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_axis_truncated_include_idle_send_data.snap index 1b747a2e..e831ebcc 100644 --- a/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_axis_truncated_include_idle_send_data.snap +++ b/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_axis_truncated_include_idle_send_data.snap @@ -1,6 +1,5 @@ --- source: protocols/src/ir/graphviz.rs -assertion_line: 212 expression: content --- == pre-contract == @@ -10,10 +9,12 @@ digraph "send_data" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node7 [label="1"]; - node7 [label="[1] D.m_axis_tdata := data"]; + node0 -> node8 [label="1"]; + node8 [label="[1] D.m_axis_tvalid := X if 1\n[1] D.m_axis_tdata := X if 1"]; + node8 -> node7 [label="1"]; + node7 [label="[1] D.m_axis_tdata := data if 1"]; node7 -> node6 [label="1"]; - node6 [label="[1] D.m_axis_tvalid := 1"]; + node6 [label="[1] D.m_axis_tvalid := 1 if 1"]; node6 -> node4 [label="1"]; node4 [label=""]; node4 -> node5 [label="not(D.m_axis_tready)"]; @@ -24,7 +25,7 @@ digraph "send_data" { node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] D.m_axis_tvalid := X if 1\n[1] D.m_axis_tdata := X if 1"]; } == post-contract == @@ -33,26 +34,52 @@ digraph "send_data" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] D.m_axis_tdata := data\n[1] D.m_axis_tvalid := 1"]; + node0 [label="[1] D.m_axis_tvalid := 1 if 1\n[1] D.m_axis_tdata := data if 1"]; node0 -> node1 [label="D.m_axis_tready / step"]; node0 -> node4 [label="not(D.m_axis_tready) / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] D.m_axis_tvalid := X if 1\n[1] D.m_axis_tdata := X if 1"]; node4 [label=""]; node4 -> node4 [label="not(D.m_axis_tready) / step"]; node4 -> node1 [label="D.m_axis_tready / step"]; } +== post-propagation == +digraph "send_data" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node8 [label="1"]; + node8 [label="[1] D.m_axis_tvalid := X if 1\n[1] D.m_axis_tdata := X if 1"]; + node8 -> node7 [label="1"]; + node7 [label="[1] D.m_axis_tdata := data if 1"]; + node7 -> node6 [label="1"]; + node6 [label="[1] D.m_axis_tvalid := 1 if 1"]; + node6 -> node4 [label="1"]; + node4 [label=""]; + node4 -> node5 [label="not(D.m_axis_tready)"]; + node4 -> node3 [label="D.m_axis_tready"]; + node5 [label=""]; + node5 -> node4 [label="1 / step"]; + node3 [label=""]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] D.m_axis_tvalid := X if 1\n[1] D.m_axis_tdata := X if 1"]; +} + == post-normalize == digraph "send_data" { rankdir=LR; node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] D.m_axis_tdata := data\n[1] D.m_axis_tvalid := 1"]; + node0 [label="[1] D.m_axis_tvalid := 1 if 1\n[1] D.m_axis_tdata := data if 1"]; node0 -> node1 [label="D.m_axis_tready / step"]; node0 -> node4 [label="not(D.m_axis_tready) / step"]; - node1 [label="[1] done\n[1] D.m_axis_tvalid := D.m_axis_tvalid\n[1] D.m_axis_tdata := D.m_axis_tdata"]; - node4 [label="[1] D.m_axis_tvalid := D.m_axis_tvalid\n[1] D.m_axis_tdata := D.m_axis_tdata"]; + node1 [label="[1] done\n[1] D.m_axis_tvalid := X if 1\n[1] D.m_axis_tdata := X if 1"]; + node4 [label="[1] D.m_axis_tvalid := 1 if 1\n[1] D.m_axis_tdata := data if 1"]; node4 -> node4 [label="not(D.m_axis_tready) / step"]; node4 -> node1 [label="D.m_axis_tready / step"]; } @@ -64,12 +91,14 @@ digraph "idle" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node3 [label="1"]; - node3 [label="[1] D.m_axis_tvalid := 0"]; + node0 -> node4 [label="1"]; + node4 [label="[1] D.m_axis_tvalid := X if 1\n[1] D.m_axis_tdata := X if 1"]; + node4 -> node3 [label="1"]; + node3 [label="[1] D.m_axis_tvalid := 0 if 1"]; node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] D.m_axis_tvalid := X if 1\n[1] D.m_axis_tdata := X if 1"]; } == post-contract == @@ -78,9 +107,26 @@ digraph "idle" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] D.m_axis_tvalid := 0"]; + node0 [label="[1] D.m_axis_tvalid := 0 if 1\n[1] D.m_axis_tdata := X if 1"]; node0 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] D.m_axis_tvalid := X if 1\n[1] D.m_axis_tdata := X if 1"]; +} + +== post-propagation == +digraph "idle" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node4 [label="1"]; + node4 [label="[1] D.m_axis_tvalid := X if 1\n[1] D.m_axis_tdata := X if 1"]; + node4 -> node3 [label="1"]; + node3 [label="[1] D.m_axis_tvalid := 0 if 1"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] D.m_axis_tvalid := X if 1\n[1] D.m_axis_tdata := X if 1"]; } == post-normalize == @@ -89,7 +135,7 @@ digraph "idle" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] D.m_axis_tvalid := 0\n[1] D.m_axis_tdata := D.m_axis_tdata"]; + node0 [label="[1] D.m_axis_tvalid := 0 if 1\n[1] D.m_axis_tdata := X if 1"]; node0 -> node1 [label="1 / step"]; - node1 [label="[1] done\n[1] D.m_axis_tvalid := D.m_axis_tvalid\n[1] D.m_axis_tdata := D.m_axis_tdata"]; + node1 [label="[1] done\n[1] D.m_axis_tvalid := X if 1\n[1] D.m_axis_tdata := X if 1"]; } diff --git a/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_bounded_ready_valid.snap b/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_bounded_ready_valid.snap index 19e366d3..482dacae 100644 --- a/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_bounded_ready_valid.snap +++ b/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_bounded_ready_valid.snap @@ -1,6 +1,5 @@ --- source: protocols/src/ir/graphviz.rs -assertion_line: 212 expression: content --- == pre-contract == @@ -10,10 +9,12 @@ digraph "send_data" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node13 [label="1"]; - node13 [label="[1] D.data := data"]; + node0 -> node14 [label="1"]; + node14 [label="[1] D.valid := X if 1\n[1] D.data := X if 1"]; + node14 -> node13 [label="1"]; + node13 [label="[1] D.data := data if 1"]; node13 -> node12 [label="1"]; - node12 [label="[1] D.valid := 1"]; + node12 [label="[1] D.valid := 1 if 1"]; node12 -> node11 [label="1"]; node11 [label=""]; node11 -> node9 [label="not(D.ready)"]; @@ -37,7 +38,7 @@ digraph "send_data" { node5 -> node4 [label="1"]; node4 [label=""]; node4 -> node3 [label="1"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] D.valid := X if 1\n[1] D.data := X if 1"]; } == post-contract == @@ -46,10 +47,10 @@ digraph "send_data" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] D.data := data\n[1] D.valid := 1"]; + node0 [label="[1] D.valid := 1 if 1\n[1] D.data := data if 1"]; node0 -> node1 [label="D.ready / step"]; node0 -> node8 [label="not(D.ready) / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] D.valid := X if 1\n[1] D.data := X if 1"]; node8 [label=""]; node8 -> node5 [label="not(D.ready) / step"]; node8 -> node1 [label="D.ready / step"]; @@ -57,19 +58,58 @@ digraph "send_data" { node5 -> node1 [label="1 / step"]; } +== post-propagation == +digraph "send_data" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node14 [label="1"]; + node14 [label="[1] D.valid := X if 1\n[1] D.data := X if 1"]; + node14 -> node13 [label="1"]; + node13 [label="[1] D.data := data if 1"]; + node13 -> node12 [label="1"]; + node12 [label="[1] D.valid := 1 if 1"]; + node12 -> node11 [label="1"]; + node11 [label=""]; + node11 -> node9 [label="not(D.ready)"]; + node11 -> node10 [label="D.ready"]; + node9 [label=""]; + node9 -> node8 [label="1 / step"]; + node10 [label=""]; + node10 -> node3 [label="1"]; + node8 [label=""]; + node8 -> node6 [label="not(D.ready)"]; + node8 -> node7 [label="D.ready"]; + node3 [label=""]; + node3 -> node2 [label="1"]; + node6 [label=""]; + node6 -> node5 [label="1 / step"]; + node7 [label=""]; + node7 -> node4 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node5 [label="[1] assert_eq(D.ready, 1)"]; + node5 -> node4 [label="1"]; + node4 [label=""]; + node4 -> node3 [label="1"]; + node1 [label="[1] done\n[1] D.valid := X if 1\n[1] D.data := X if 1"]; +} + == post-normalize == digraph "send_data" { rankdir=LR; node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] D.data := data\n[1] D.valid := 1"]; + node0 [label="[1] D.valid := 1 if 1\n[1] D.data := data if 1"]; node0 -> node1 [label="D.ready / step"]; node0 -> node8 [label="not(D.ready) / step"]; - node1 [label="[1] done\n[1] D.valid := D.valid\n[1] D.data := D.data"]; - node8 [label="[1] D.valid := D.valid\n[1] D.data := D.data"]; + node1 [label="[1] done\n[1] D.valid := X if 1\n[1] D.data := X if 1"]; + node8 [label="[1] D.valid := 1 if 1\n[1] D.data := data if 1"]; node8 -> node5 [label="not(D.ready) / step"]; node8 -> node1 [label="D.ready / step"]; - node5 [label="[1] assert_eq(D.ready, 1)\n[1] D.valid := D.valid\n[1] D.data := D.data"]; + node5 [label="[1] assert_eq(D.ready, 1)\n[1] D.valid := 1 if 1\n[1] D.data := data if 1"]; node5 -> node1 [label="1 / step"]; } diff --git a/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_counter.snap b/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_counter.snap index aa174eba..4b265460 100644 --- a/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_counter.snap +++ b/protocols/src/tests/snapshots/protocols__ir__graphviz__tests__ir_graphviz_counter.snap @@ -1,6 +1,5 @@ --- source: protocols/src/ir/graphviz.rs -assertion_line: 212 expression: content --- == pre-contract == @@ -10,8 +9,10 @@ digraph "count_up" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node9 [label="1"]; - node9 [label="[1] dut.a := a"]; + node0 -> node10 [label="1"]; + node10 [label="[1] dut.a := X if 1"]; + node10 -> node9 [label="1"]; + node9 [label="[1] dut.a := a if 1"]; node9 -> node7 [label="1"]; node7 [label=""]; node7 -> node8 [label="not(eq(dut.s, dut.a))"]; @@ -28,7 +29,7 @@ digraph "count_up" { node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] dut.a := X if 1"]; } == post-contract == @@ -37,7 +38,7 @@ digraph "count_up" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] dut.a := a"]; + node0 [label="[1] dut.a := a if 1"]; node0 -> node4 [label="eq(dut.s, dut.a) / step"]; node0 -> node7 [label="not(eq(dut.s, dut.a)) / step"]; node4 [label="[1] assert_eq(dut.s, 0)\n[1] fork"]; @@ -45,7 +46,37 @@ digraph "count_up" { node7 [label=""]; node7 -> node7 [label="not(eq(dut.s, dut.a)) / step"]; node7 -> node4 [label="eq(dut.s, dut.a) / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] dut.a := X if 1"]; +} + +== post-propagation == +digraph "count_up" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node10 [label="1"]; + node10 [label="[1] dut.a := X if 1"]; + node10 -> node9 [label="1"]; + node9 [label="[1] dut.a := a if 1"]; + node9 -> node7 [label="1"]; + node7 [label=""]; + node7 -> node8 [label="not(eq(dut.s, dut.a))"]; + node7 -> node6 [label="eq(dut.s, dut.a)"]; + node8 [label=""]; + node8 -> node7 [label="1 / step"]; + node6 [label=""]; + node6 -> node5 [label="1"]; + node5 [label=""]; + node5 -> node4 [label="1 / step"]; + node4 [label="[1] assert_eq(dut.s, 0)"]; + node4 -> node3 [label="1"]; + node3 [label="[1] fork"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] dut.a := X if 1"]; } == post-normalize == @@ -54,15 +85,15 @@ digraph "count_up" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] dut.a := a"]; + node0 [label="[1] dut.a := a if 1"]; node0 -> node4 [label="eq(dut.s, dut.a) / step"]; node0 -> node7 [label="not(eq(dut.s, dut.a)) / step"]; - node4 [label="[1] assert_eq(dut.s, 0)\n[1] fork\n[1] dut.a := dut.a"]; + node4 [label="[1] assert_eq(dut.s, 0)\n[1] fork\n[1] dut.a := a if 1"]; node4 -> node1 [label="1 / step"]; - node7 [label="[1] dut.a := dut.a"]; + node7 [label="[1] dut.a := a if 1"]; node7 -> node7 [label="not(eq(dut.s, dut.a)) / step"]; node7 -> node4 [label="eq(dut.s, dut.a) / step"]; - node1 [label="[1] done\n[1] dut.a := dut.a"]; + node1 [label="[1] done\n[1] dut.a := X if 1"]; } == pre-contract == @@ -72,8 +103,10 @@ digraph "count_up_extra_assertion" { entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; node0 [label=""]; - node0 -> node10 [label="1"]; - node10 [label="[1] dut.a := a"]; + node0 -> node11 [label="1"]; + node11 [label="[1] dut.a := X if 1"]; + node11 -> node10 [label="1"]; + node10 [label="[1] dut.a := a if 1"]; node10 -> node8 [label="1"]; node8 [label=""]; node8 -> node9 [label="not(eq(dut.s, dut.a))"]; @@ -92,7 +125,7 @@ digraph "count_up_extra_assertion" { node3 -> node2 [label="1"]; node2 [label=""]; node2 -> node1 [label="1 / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] dut.a := X if 1"]; } == post-contract == @@ -101,7 +134,7 @@ digraph "count_up_extra_assertion" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] dut.a := a\n[eq(dut.s, dut.a)] assert_eq(dut.s, a)"]; + node0 [label="[1] dut.a := a if 1\n[eq(dut.s, dut.a)] assert_eq(dut.s, a)"]; node0 -> node4 [label="eq(dut.s, dut.a) / step"]; node0 -> node8 [label="not(eq(dut.s, dut.a)) / step"]; node4 [label="[1] assert_eq(dut.s, 0)\n[1] fork"]; @@ -109,7 +142,39 @@ digraph "count_up_extra_assertion" { node8 [label="[eq(dut.s, dut.a)] assert_eq(dut.s, a)"]; node8 -> node8 [label="not(eq(dut.s, dut.a)) / step"]; node8 -> node4 [label="eq(dut.s, dut.a) / step"]; - node1 [label="[1] done"]; + node1 [label="[1] done\n[1] dut.a := X if 1"]; +} + +== post-propagation == +digraph "count_up_extra_assertion" { + rankdir=LR; + node [shape=box]; + entry_marker [shape=plain,label="ENTRY"]; + entry_marker -> node0; + node0 [label=""]; + node0 -> node11 [label="1"]; + node11 [label="[1] dut.a := X if 1"]; + node11 -> node10 [label="1"]; + node10 [label="[1] dut.a := a if 1"]; + node10 -> node8 [label="1"]; + node8 [label=""]; + node8 -> node9 [label="not(eq(dut.s, dut.a))"]; + node8 -> node7 [label="eq(dut.s, dut.a)"]; + node9 [label=""]; + node9 -> node8 [label="1 / step"]; + node7 [label=""]; + node7 -> node6 [label="1"]; + node6 [label="[1] assert_eq(dut.s, a)"]; + node6 -> node5 [label="1"]; + node5 [label=""]; + node5 -> node4 [label="1 / step"]; + node4 [label="[1] assert_eq(dut.s, 0)"]; + node4 -> node3 [label="1"]; + node3 [label="[1] fork"]; + node3 -> node2 [label="1"]; + node2 [label=""]; + node2 -> node1 [label="1 / step"]; + node1 [label="[1] done\n[1] dut.a := X if 1"]; } == post-normalize == @@ -118,13 +183,13 @@ digraph "count_up_extra_assertion" { node [shape=box]; entry_marker [shape=plain,label="ENTRY"]; entry_marker -> node0; - node0 [label="[1] dut.a := a\n[eq(dut.s, dut.a)] assert_eq(dut.s, a)"]; + node0 [label="[1] dut.a := a if 1\n[eq(dut.s, dut.a)] assert_eq(dut.s, a)"]; node0 -> node4 [label="eq(dut.s, dut.a) / step"]; node0 -> node8 [label="not(eq(dut.s, dut.a)) / step"]; - node4 [label="[1] assert_eq(dut.s, 0)\n[1] fork\n[1] dut.a := dut.a"]; + node4 [label="[1] assert_eq(dut.s, 0)\n[1] fork\n[1] dut.a := a if 1"]; node4 -> node1 [label="1 / step"]; - node8 [label="[eq(dut.s, dut.a)] assert_eq(dut.s, a)\n[1] dut.a := dut.a"]; + node8 [label="[eq(dut.s, dut.a)] assert_eq(dut.s, a)\n[1] dut.a := a if 1"]; node8 -> node8 [label="not(eq(dut.s, dut.a)) / step"]; node8 -> node4 [label="eq(dut.s, dut.a) / step"]; - node1 [label="[1] done\n[1] dut.a := dut.a"]; + node1 [label="[1] done\n[1] dut.a := X if 1"]; } diff --git a/runt/waveform/runt.toml b/runt/waveform/runt.toml index efb989d1..a0c4d3d6 100644 --- a/runt/waveform/runt.toml +++ b/runt/waveform/runt.toml @@ -18,6 +18,24 @@ expect_dir = "../../examples/picorv32/expects" expect_name = "unsigned_mul.waveform.expect" cmd = "cd ../.. && target/debug/graph-interp --transactions examples/picorv32/unsigned_mul.tx --respect-forks --determinize --ascii-waveform --verilog examples/picorv32/picorv32.v --protocol examples/picorv32/pcpi_mul.prot --module picorv32_pcpi_mul 2>/dev/null" +[[tests]] +name = "waveform.examples_serv_serv_regfile.serv_regfile_waveform.ast" +paths = [ + "../../examples/serv/serv_regfile.tx", +] +expect_dir = "../../examples/serv/expects" +expect_name = "serv_regfile.waveform.expect" +cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions examples/serv/serv_regfile.tx --ascii-waveform --verilog examples/serv/rtl/serv_regfile.v --protocol examples/serv/serv_regfile.prot 2>/dev/null" + +[[tests]] +name = "waveform.examples_serv_serv_regfile.serv_regfile_waveform.graph" +paths = [ + "../../examples/serv/serv_regfile.tx", +] +expect_dir = "../../examples/serv/expects" +expect_name = "serv_regfile.waveform.expect" +cmd = "cd ../.. && target/debug/graph-interp --transactions examples/serv/serv_regfile.tx --respect-forks --determinize --ascii-waveform --verilog examples/serv/rtl/serv_regfile.v --protocol examples/serv/serv_regfile.prot 2>/dev/null" + [[tests]] name = "waveform.examples_tinyaes128_aes128.aes128_waveform.ast" paths = [ @@ -234,24 +252,6 @@ expect_dir = "../../tests/brave_new_world/bit_truncation/expects" expect_name = "bit_truncation_sha_fix.waveform.expect" cmd = "cd ../.. && target/debug/graph-interp --transactions tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.tx --respect-forks --determinize --ascii-waveform --verilog tests/brave_new_world/bit_truncation/bit_truncation_sha_fix.v --protocol tests/brave_new_world/bit_truncation/bit_truncation_sha.prot --module bit_truncation_sha_fixed 2>/dev/null" -[[tests]] -name = "waveform.tests_brave_new_world_failure_to_update_ftu_sha_fix.ftu_sha_fix_waveform.ast" -paths = [ - "../../tests/brave_new_world/failure_to_update/ftu_sha_fix.tx", -] -expect_dir = "../../tests/brave_new_world/failure_to_update/expects" -expect_name = "ftu_sha_fix.waveform.expect" -cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/brave_new_world/failure_to_update/ftu_sha_fix.tx --ascii-waveform --verilog tests/brave_new_world/failure_to_update/ftu_sha_fix.v --protocol tests/brave_new_world/failure_to_update/ftu_sha.prot --module fsm_update_fixed_gated 2>/dev/null" - -[[tests]] -name = "waveform.tests_brave_new_world_failure_to_update_ftu_sha_fix.ftu_sha_fix_waveform.graph" -paths = [ - "../../tests/brave_new_world/failure_to_update/ftu_sha_fix.tx", -] -expect_dir = "../../tests/brave_new_world/failure_to_update/expects" -expect_name = "ftu_sha_fix.waveform.expect" -cmd = "cd ../.. && target/debug/graph-interp --transactions tests/brave_new_world/failure_to_update/ftu_sha_fix.tx --respect-forks --determinize --ascii-waveform --verilog tests/brave_new_world/failure_to_update/ftu_sha_fix.v --protocol tests/brave_new_world/failure_to_update/ftu_sha.prot --module fsm_update_fixed_gated 2>/dev/null" - [[tests]] name = "waveform.tests_brave_new_world_signal_asynchrony_signal_async_fix.signal_async_fix_waveform.ast" paths = [ @@ -306,6 +306,42 @@ expect_dir = "../../tests/counters/expects" expect_name = "counter.waveform.expect" cmd = "cd ../.. && target/debug/graph-interp --transactions tests/counters/counter.tx --respect-forks --determinize --ascii-waveform --verilog tests/counters/counter.v --protocol tests/counters/counter.prot 2>/dev/null" +[[tests]] +name = "waveform.tests_fifo_fifo.fifo_waveform.ast" +paths = [ + "../../tests/fifo/fifo.tx", +] +expect_dir = "../../tests/fifo/expects" +expect_name = "fifo.waveform.expect" +cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fifo/fifo.tx --ascii-waveform --verilog tests/fifo/bsg_mem_1rw_sync.v tests/fifo/bsg_mem_1rw_sync_synth.v tests/fifo/bsg_circular_ptr.v tests/fifo/bsg_fifo_1rw_large.v tests/fifo/fifo_wrapper.v --protocol tests/fifo/fifo.prot --module fifo_wrapper 2>/dev/null" + +[[tests]] +name = "waveform.tests_fifo_fifo.fifo_waveform.graph" +paths = [ + "../../tests/fifo/fifo.tx", +] +expect_dir = "../../tests/fifo/expects" +expect_name = "fifo.waveform.expect" +cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fifo/fifo.tx --respect-forks --determinize --ascii-waveform --verilog tests/fifo/bsg_mem_1rw_sync.v tests/fifo/bsg_mem_1rw_sync_synth.v tests/fifo/bsg_circular_ptr.v tests/fifo/bsg_fifo_1rw_large.v tests/fifo/fifo_wrapper.v --protocol tests/fifo/fifo.prot --module fifo_wrapper 2>/dev/null" + +[[tests]] +name = "waveform.tests_fifo_push_pop_identity_ok.push_pop_identity_ok_waveform.ast" +paths = [ + "../../tests/fifo/push_pop_identity_ok.tx", +] +expect_dir = "../../tests/fifo/expects" +expect_name = "push_pop_identity_ok.waveform.expect" +cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/fifo/push_pop_identity_ok.tx --ascii-waveform --verilog tests/fifo/bsg_mem_1rw_sync.v tests/fifo/bsg_mem_1rw_sync_synth.v tests/fifo/bsg_circular_ptr.v tests/fifo/bsg_fifo_1rw_large.v tests/fifo/fifo_wrapper.v --protocol tests/fifo/fifo.prot --module fifo_wrapper 2>/dev/null" + +[[tests]] +name = "waveform.tests_fifo_push_pop_identity_ok.push_pop_identity_ok_waveform.graph" +paths = [ + "../../tests/fifo/push_pop_identity_ok.tx", +] +expect_dir = "../../tests/fifo/expects" +expect_name = "push_pop_identity_ok.waveform.expect" +cmd = "cd ../.. && target/debug/graph-interp --transactions tests/fifo/push_pop_identity_ok.tx --respect-forks --determinize --ascii-waveform --verilog tests/fifo/bsg_mem_1rw_sync.v tests/fifo/bsg_mem_1rw_sync_synth.v tests/fifo/bsg_circular_ptr.v tests/fifo/bsg_fifo_1rw_large.v tests/fifo/fifo_wrapper.v --protocol tests/fifo/fifo.prot --module fifo_wrapper 2>/dev/null" + [[tests]] name = "waveform.tests_identities_identity_d0_passthrough_combdep.passthrough_combdep_waveform.ast" paths = [ @@ -360,24 +396,6 @@ expect_dir = "../../tests/identities/identity_d2/expects" expect_name = "single_thread_passes.waveform.expect" cmd = "cd ../.. && target/debug/graph-interp --transactions tests/identities/identity_d2/single_thread_passes.tx --respect-forks --determinize --ascii-waveform --verilog tests/identities/identity_d2/identity_d2.v --protocol tests/identities/identity_d2/identity_d2.prot 2>/dev/null" -[[tests]] -name = "waveform.tests_identities_identity_d2_two_assignments_same_value.two_assignments_same_value_waveform.ast" -paths = [ - "../../tests/identities/identity_d2/two_assignments_same_value.tx", -] -expect_dir = "../../tests/identities/identity_d2/expects" -expect_name = "two_assignments_same_value.waveform.expect" -cmd = "cd ../.. && target/debug/protocols-interp --color never --transactions tests/identities/identity_d2/two_assignments_same_value.tx --ascii-waveform --verilog tests/identities/identity_d2/identity_d2.v --protocol tests/identities/identity_d2/identity_d2.prot 2>/dev/null" - -[[tests]] -name = "waveform.tests_identities_identity_d2_two_assignments_same_value.two_assignments_same_value_waveform.graph" -paths = [ - "../../tests/identities/identity_d2/two_assignments_same_value.tx", -] -expect_dir = "../../tests/identities/identity_d2/expects" -expect_name = "two_assignments_same_value.waveform.expect" -cmd = "cd ../.. && target/debug/graph-interp --transactions tests/identities/identity_d2/two_assignments_same_value.tx --respect-forks --determinize --ascii-waveform --verilog tests/identities/identity_d2/identity_d2.v --protocol tests/identities/identity_d2/identity_d2.prot 2>/dev/null" - [[tests]] name = "waveform.tests_multi_multi0_multi0.multi0_waveform.ast" paths = [ diff --git a/scripts/generate_runt_configs.py b/scripts/generate_runt_configs.py index 011e7293..f5233389 100644 --- a/scripts/generate_runt_configs.py +++ b/scripts/generate_runt_configs.py @@ -282,11 +282,13 @@ def waveform_cases(cases: list[dict]) -> list[dict]: # these cases are correct, but our ASCII diffing isn't good enough # for us to know they are the same xfailed = [ - "examples/serv/serv_regfile.tx", + # "examples/serv/serv_regfile.tx", "tests/adders/adder_d1/wait_and_add_correct.tx", - "tests/fifo/fifo.tx", - "tests/fifo/push_pop_identity_ok.tx", + "tests/identities/identity_d2/two_assignments_same_value.tx", + # "tests/fifo/fifo.tx", + # "tests/fifo/push_pop_identity_ok.tx", "tests/wishbone/wishbone.tx", + "tests/brave_new_world/failure_to_update/ftu_sha_fix.tx", ] return list(filter(lambda c: c["path"] not in xfailed, graph_interp_cases(cases))) diff --git a/tests/adders/adder_d1/add_d1.prot b/tests/adders/adder_d1/add_d1.prot index cacf3ce0..bb677dcf 100644 --- a/tests/adders/adder_d1/add_d1.prot +++ b/tests/adders/adder_d1/add_d1.prot @@ -89,6 +89,27 @@ prot assign_after_observation(a: u32, b: u32, s: u32) { step(); } + +// conditional assignment +prot better_if_else(a: u32, b: u32) { + DUT.a := a; + DUT.b := b; + + step(); + + if (DUT.s == 32'b0){ + DUT.a := X; + } + else { + DUT.a := 32'd5; + } + +// assert_eq(, DUT.s); + + fork(); + step(); +} + // conditional assignment prot if_else(a1: u32, a2: u32) { if (1'b1) {