#![allow(dead_code)]
use std::collections::{BTreeSet, HashMap, HashSet};
use sv_lang::kinds::{AssertionExprKind, ExpressionKind, SymbolKind};
use sv_lang::nodes::{
IdentifierNameSyntax, ParenthesizedSequenceExprSyntax, SequenceRepetitionSyntax,
SimpleSequenceExprSyntax,
};
use sv_lang::{
ArgumentDirection, AssertionExpr, AstNode, Expression, KnownSystemName, Node, SemNode, Symbol,
UnaryOp,
};
use sv_sim_sim::sva::ir::{self, ClockId, LeafId, LocalVarId, ThreadStateId, Transition};
use super::actions::{self, CallSite};
use super::flow::{Flow, VarSet};
use super::op::{AssertionBinaryOp, Op};
use super::ranges::{self, SequenceRangeValue};
use super::trees::{Trees, key};
use crate::error::LoweringError;
pub mod property;
#[derive(Clone, Debug, Default, PartialEq, Eq)]
pub struct LeafLocals<'d> {
pub reads: Vec<(Symbol<'d>, LocalVarId)>,
pub lvalue: Option<LocalVarId>,
pub end_flags: Vec<LocalVarId>,
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct LimbSel {
pub width: u32,
pub unknown: bool,
pub index: u32,
pub group: u32,
}
pub const MAX_LOCAL_VAR_BITS: u32 = 1 << 20;
#[derive(Clone, Copy, Debug)]
pub struct EndSite<'d> {
pub method: ir::EndMethod,
pub instance: Expression<'d>,
pub clock: Option<SemNode<'d>>,
}
#[derive(Clone, Copy, Debug)]
struct ScopeVar<'d> {
sym: Symbol<'d>,
slot: LocalVarId,
}
#[derive(Debug)]
struct ShadowCtx {
outer_touched: BTreeSet<LocalVarId>,
made: Vec<(LocalVarId, LocalVarId, LocalVarId)>,
}
#[derive(Debug)]
pub struct LeafTable<'d> {
leaves: Vec<Expression<'d>>,
negated: Vec<bool>,
leaf_locals: Vec<LeafLocals<'d>>,
limbs: Vec<Option<LimbSel>>,
scope: Vec<ScopeVar<'d>>,
flow_in: VarSet,
touched: Vec<LocalVarId>,
shadows: Vec<ShadowCtx>,
env: ranges::FormalEnv,
chain: Vec<ranges::ChainLink>,
instance_depth: usize,
clocks: Vec<Option<SemNode<'d>>>,
cur: ClockId,
inferred: Vec<Option<SemNode<'d>>>,
root_inferred: bool,
disable_inferred: bool,
pub(super) calls: Vec<CallSite<'d>>,
end_sites: Vec<EndSite<'d>>,
future_gclk: bool,
}
impl<'d> LeafTable<'d> {
fn new(root_clock: Option<SemNode<'d>>) -> Self {
LeafTable {
future_gclk: false,
calls: Vec::new(),
end_sites: Vec::new(),
leaves: Vec::new(),
negated: Vec::new(),
leaf_locals: Vec::new(),
limbs: Vec::new(),
scope: Vec::new(),
flow_in: VarSet::new(),
touched: Vec::new(),
shadows: Vec::new(),
env: ranges::FormalEnv::default(),
chain: Vec::new(),
instance_depth: 0,
clocks: vec![root_clock],
cur: ClockId(0),
inferred: Vec::new(),
root_inferred: false,
disable_inferred: false,
}
}
pub fn disable_inferred(&self) -> bool {
self.disable_inferred
}
fn intern_clock(&mut self, event: SemNode<'d>) -> ClockId {
for (i, known) in self.clocks.iter().enumerate() {
if known.is_some_and(|k| events_equivalent(k, event)) {
return ClockId(i as u32);
}
}
if self.clocks[0].is_none() {
self.clocks[0] = Some(event);
return ClockId(0);
}
self.clocks.push(Some(event));
ClockId(self.clocks.len() as u32 - 1)
}
fn resolve_clock(
&mut self,
event: SemNode<'d>,
scope: &Symbol<'d>,
) -> Result<ClockId, LoweringError> {
if is_inferred_clock_event(event) {
let at = self
.inferred
.last()
.copied()
.unwrap_or(self.clocks[self.cur.0 as usize]);
let Some(ev) = at else {
return Err(LoweringError::unsupported_at(
"`$inferred_clock` (LRM 16.14.7) in an assertion whose instantiation \
context has no clock (clock inference, 16.14.6, found none)",
scope,
));
};
return Ok(self.intern_clock(ev));
}
Ok(self.intern_clock(event))
}
fn rebind_inferred_root(&mut self, event: SemNode<'d>) {
if std::mem::take(&mut self.root_inferred)
&& self.cur == ClockId(0)
&& self.clocks.len() == 1
&& !is_inferred_clock_event(event)
{
self.clocks[0] = Some(event);
}
}
pub fn clock_count(&self) -> usize {
self.clocks.len()
}
pub fn clock_event(&self, clock: ClockId) -> Option<SemNode<'d>> {
self.clocks[clock.0 as usize]
}
pub fn locals_of(&self, id: LeafId) -> &LeafLocals<'d> {
&self.leaf_locals[id.0 as usize]
}
pub fn call_site(&self, id: ir::CallId) -> &CallSite<'d> {
&self.calls[id.0 as usize]
}
pub fn uses_future_gclk(&self) -> bool {
self.future_gclk
}
pub fn call_count(&self) -> usize {
self.calls.len()
}
pub fn calls(&self) -> &[CallSite<'d>] {
&self.calls
}
pub fn end_site(&self, site: u32) -> &EndSite<'d> {
&self.end_sites[site as usize]
}
pub fn end_site_count(&self) -> usize {
self.end_sites.len()
}
pub(super) fn push_leaf(
&mut self,
a: &mut ir::Automaton,
e: Expression<'d>,
lvalue: Option<LocalVarId>,
scope: &Symbol<'d>,
) -> Result<LeafId, LoweringError> {
let mut points = Vec::new();
collect_end_points(e, &mut points);
if !points.is_empty() {
return Err(LoweringError::unsupported_at(
"a sequence method `.triggered`/`.matched` inside a match item or a local \
variable initializer is not implemented (the end point is tested where a \
sequence operand stands, LRM 16.9.11/16.13.5; sva T15)",
scope,
));
}
self.push_leaf_flags(a, e, lvalue, &[], false, scope)
}
fn push_leaf_flags(
&mut self,
a: &mut ir::Automaton,
e: Expression<'d>,
lvalue: Option<LocalVarId>,
flags: &[LocalVarId],
negated: bool,
scope: &Symbol<'d>,
) -> Result<LeafId, LoweringError> {
let mut syms = Vec::new();
let mut reads_lvalue = false;
collect_local_reads(e.as_sem_node(), &mut syms, &mut reads_lvalue);
let mut locals = LeafLocals {
end_flags: flags.to_vec(),
..LeafLocals::default()
};
for sym in syms {
let slot = self.resolve(sym, scope)?;
self.check_flows(sym, slot, scope)?;
let phys = self.phys_of(a, slot);
if !locals.reads.iter().any(|(s, _)| *s == sym) {
locals.reads.push((sym, phys));
}
}
if let Some(target) = lvalue {
if reads_lvalue {
let name = self
.scope
.iter()
.rev()
.find(|v| v.slot == target)
.map(|v| v.sym.name().to_string())
.unwrap_or_default();
if !self.flow_in.contains(&target) {
return Err(not_flowing(&name, scope));
}
}
locals.lvalue = Some(self.phys_of(a, target));
}
let id = LeafId(self.leaves.len() as u32);
self.leaves.push(e);
self.negated.push(negated);
self.leaf_locals.push(locals);
self.limbs.push(None);
Ok(id)
}
pub fn limb_of(&self, id: LeafId) -> Option<LimbSel> {
self.limbs[id.0 as usize]
}
pub(super) fn push_arg_leaves(
&mut self,
a: &mut ir::Automaton,
e: Expression<'d>,
width: u32,
scope: &Symbol<'d>,
) -> Result<Vec<LeafId>, LoweringError> {
if width <= 64 {
return Ok(vec![self.push_leaf(a, e, None, scope)?]);
}
if width > MAX_LOCAL_VAR_BITS {
return Err(LoweringError::unsupported_at(
&format!(
"a by-value argument of {width} bits in a sequence match-item call (16.11): \
at most {MAX_LOCAL_VAR_BITS} bits is implemented"
),
scope,
));
}
let n = width.div_ceil(64);
let mut out = Vec::with_capacity(2 * n as usize);
let mut group = None;
for slot in 0..2 * n {
let leaf = self.push_leaf(a, e, None, scope)?;
self.limbs[leaf.0 as usize] = Some(LimbSel {
width,
unknown: slot >= n,
index: slot % n,
group: group.get_or_insert(leaf.0).to_owned(),
});
out.push(leaf);
}
Ok(out)
}
pub(super) fn slot_leaves(
&mut self,
a: &mut ir::Automaton,
var: LocalVarId,
e: Expression<'d>,
lvalue: Option<LocalVarId>,
scope: &Symbol<'d>,
) -> Result<Vec<(LocalVarId, LeafId)>, LoweringError> {
let decl = *a.local_var(var);
if !decl.is_wide() {
return Ok(vec![(var, self.push_leaf(a, e, lvalue, scope)?)]);
}
let n = decl.limbs() as u32;
let mut out = Vec::with_capacity(2 * n as usize);
let mut group = None;
for slot in 0..2 * n {
let leaf = self.push_leaf(a, e, lvalue, scope)?;
self.limbs[leaf.0 as usize] = Some(LimbSel {
width: decl.width,
unknown: slot >= n,
index: slot % n,
group: group.get_or_insert(leaf.0).to_owned(),
});
out.push((LocalVarId(var.0 + slot), leaf));
}
Ok(out)
}
pub(super) fn assign_var(
&mut self,
a: &mut ir::Automaton,
canon: LocalVarId,
phys: LocalVarId,
e: Expression<'d>,
scope: &Symbol<'d>,
) -> Result<Vec<Transition>, LoweringError> {
let decl = *a.local_var(phys);
let mut syms = Vec::new();
let mut reads_lvalue = false;
collect_local_reads(e.as_sem_node(), &mut syms, &mut reads_lvalue);
let reads_target = reads_lvalue
|| syms
.iter()
.any(|s| self.resolve(*s, scope).is_ok_and(|c| c == canon));
let temp =
(decl.is_wide() && reads_target).then(|| a.new_local_var(decl.width, decl.signed));
let dst = temp.unwrap_or(phys);
let mut out: Vec<Transition> = self
.slot_leaves(a, dst, e, Some(canon), scope)?
.into_iter()
.map(|(var, value)| Transition::LocalVarWrite { var, value })
.collect();
if let Some(src) = temp {
out.push(Transition::LocalVarCopy { dst: phys, src });
}
Ok(out)
}
fn resolve(&self, sym: Symbol<'d>, scope: &Symbol<'d>) -> Result<LocalVarId, LoweringError> {
self.scope
.iter()
.rev()
.find(|v| v.sym == sym)
.map(|v| v.slot)
.ok_or_else(|| {
LoweringError::unsupported_at(
&format!(
"local variable `{}` is not declared by an enclosing named sequence \
(assertion variable declarations of a property or assertion statement \
are sva T19/T20's)",
sym.name()
),
scope,
)
})
}
fn check_flows(
&self,
sym: Symbol<'d>,
slot: LocalVarId,
scope: &Symbol<'d>,
) -> Result<(), LoweringError> {
if self.flow_in.contains(&slot) {
Ok(())
} else {
Err(not_flowing(sym.name(), scope))
}
}
fn phys_of(&mut self, a: &mut ir::Automaton, canon: LocalVarId) -> LocalVarId {
self.touched.push(canon);
let mut current = canon;
for ctx in &mut self.shadows {
if let Some(&(_, _, s)) = ctx.made.iter().find(|(c, _, _)| *c == canon) {
current = s;
} else if ctx.outer_touched.contains(&canon) {
let decl = *a.local_var(canon);
let shadow = a.new_local_var(decl.width, decl.signed);
ctx.made.push((canon, current, shadow));
current = shadow;
}
}
current
}
fn declare(
&mut self,
a: &mut ir::Automaton,
sym: Symbol<'d>,
scope: &Symbol<'d>,
) -> Result<LocalVarId, LoweringError> {
let ty = sym.declared_type().filter(|t| {
t.is_integral()
|| t.is_floating()
|| t.is_string()
|| t.is_class()
|| is_stored_aggregate(t)
|| is_integral_collection(t)
});
let Some(ty) = ty else {
if sym
.declared_type()
.is_some_and(|t| t.is_dynamically_sized_array())
{
return Err(LoweringError::unsupported_at(
&format!(
"local variable `{}` is a queue, dynamic array or associative array \
whose elements are not integral or unpacked structs of integral fields \
(they are themselves collections, or hold handles): only collections of \
integral or plain-struct elements are implemented as sequence local \
variables (LRM 16.10)",
sym.name()
),
scope,
));
}
return Err(LoweringError::unsupported_at(
&format!(
"local variable `{}` has a type that is neither integral, real, string, class handle nor unpacked struct nor fixed-size unpacked array of integral elements; only \
those local variables are implemented",
sym.name()
),
scope,
));
};
let is_coll = is_integral_collection(&ty);
let width = if ty.is_string() || ty.is_class() || is_coll {
64
} else if let Some(rows) = flat_array_rows(&ty) {
let shape = crate::arrays::array_shape(&ty).expect("flat_array_rows saw a shape");
rows * u64::from(crate::types::TypeWidth::value_width(&shape.elem))
} else if ty.is_floating() || is_stored_aggregate(&ty) {
u64::from(crate::types::TypeWidth::value_width(&ty))
} else {
ty.bit_width()
};
if width == 0 || width > u64::from(MAX_LOCAL_VAR_BITS) {
return Err(LoweringError::unsupported_at(
&format!(
"local variable `{}` is {width} bits wide; a local variable of 1 to \
{MAX_LOCAL_VAR_BITS} bits is implemented (a variable wider than 64 bits \
takes a frame slot per 64-bit limb of its value and of its unknown bits, \
and each assignment of it a leaf per slot)",
sym.name()
),
scope,
));
}
let slot = a.new_local_var(
width as u32,
!(ty.is_string() || ty.is_class() || is_coll || is_stored_aggregate(&ty))
&& ty.is_signed(),
);
self.scope.push(ScopeVar { sym, slot });
Ok(slot)
}
pub fn get(&self, id: LeafId) -> Expression<'d> {
self.leaves[id.0 as usize]
}
pub fn is_negated(&self, id: LeafId) -> bool {
self.negated[id.0 as usize]
}
pub fn len(&self) -> usize {
self.leaves.len()
}
}
pub(super) fn collect_local_reads<'d>(
n: SemNode<'d>,
out: &mut Vec<Symbol<'d>>,
lvalue: &mut bool,
) {
if let Some(e) = n.as_expression() {
if end_point_call(e).is_some() {
return;
}
let k = e.kind();
if k == ExpressionKind::NamedValue {
if let Some(s) = e
.referenced_symbol()
.filter(|s| s.kind() == SymbolKind::LocalAssertionVar)
{
out.push(s);
}
} else if k == ExpressionKind::LValueReference {
*lvalue = true;
}
}
for c in n.children() {
collect_local_reads(c, out, lvalue);
}
}
fn end_point_call<'d>(e: Expression<'d>) -> Option<(ir::EndMethod, Expression<'d>)> {
if e.kind() != ExpressionKind::Call {
return None;
}
let name = e.system_subroutine()?.known_name_id();
let method = if name == KnownSystemName::Triggered {
ir::EndMethod::Triggered
} else if name == KnownSystemName::Matched {
ir::EndMethod::Matched
} else {
return None;
};
let operand = *e.operands().first()?;
(operand.kind() == ExpressionKind::AssertionInstance).then_some((method, operand))
}
pub(crate) fn collect_end_points<'d>(
e: Expression<'d>,
out: &mut Vec<(ir::EndMethod, Expression<'d>)>,
) {
if let Some(p) = end_point_call(e) {
out.push(p);
return;
}
for c in e.as_sem_node().children() {
if let Some(c) = c.as_expression() {
collect_end_points(c, out);
}
}
}
fn is_local_collection_method(e: Expression<'_>) -> bool {
let ops = e.operands();
e.call_subroutine().is_none()
&& ops.first().is_some_and(|r| {
crate::collections::coll_of_expr(r).is_some()
&& r.kind() == ExpressionKind::NamedValue
&& r.referenced_symbol()
.is_some_and(|s| s.kind() == SymbolKind::LocalAssertionVar)
})
}
fn is_integral_collection(t: &sv_lang::Type<'_>) -> bool {
sv_sim_sim::state::storage::is_collection(t)
&& t.element_type().is_some_and(|e| {
(e.is_integral()
|| e.is_unpacked_struct()
|| sv_sim_sim::state::storage::is_collection(&e))
&& crate::collections::handle_offsets(&e)
.iter()
.all(|s| s.kind == crate::collections::HandleKind::Coll && s.guards.is_empty())
&& collection_nest(t).is_some()
})
}
pub(super) fn collection_nest(ty: &sv_lang::Type<'_>) -> Option<sv_sim_sim::collections::Nest> {
let elem = ty.element_type()?;
let mut slots = Vec::new();
nest_slots(&elem, 0, &mut slots)?;
Some(sv_sim_sim::collections::Nest { slots })
}
fn nest_slots(
ty: &sv_lang::Type<'_>,
base: u32,
out: &mut Vec<(u32, sv_sim_sim::collections::Nest)>,
) -> Option<()> {
use sv_sim_sim::state::storage;
if storage::is_collection(ty) {
out.push((base, collection_nest(ty)?));
} else if ty.is_class() {
return None;
} else if ty.is_unpacked_struct() {
for f in ty.fields() {
let (Some(fty), Some((lo, _))) =
(f.value_type(), storage::field_slice(ty, f.field_index()))
else {
continue;
};
nest_slots(&fty, base + lo as u32, out)?;
}
} else if ty.is_unpacked_array() {
let elem = ty.element_type()?;
let ew = storage::storage_width(&elem)?;
for i in 0..ty.fixed_unpacked_array_range().width() {
nest_slots(&elem, base + i * ew as u32, out)?;
}
} else if !crate::collections::handle_offsets(ty).is_empty() {
return None;
}
Some(())
}
fn is_stored_aggregate(t: &sv_lang::Type<'_>) -> bool {
t.is_unpacked_struct() || flat_array_rows(t).is_some()
}
fn flat_array_rows(t: &sv_lang::Type<'_>) -> Option<u64> {
let shape = crate::arrays::array_shape(t)?;
(!shape.dims.is_empty()
&& shape.rows() <= crate::arrays::MAX_UNROLLED_ROWS
&& shape.elem.is_integral()
&& crate::collections::handle_offsets(&shape.elem).is_empty())
.then(|| shape.rows())
}
fn not_flowing(name: &str, scope: &Symbol<'_>) -> LoweringError {
LoweringError::unsupported_at(
&format!(
"local variable `{name}` does not flow out to this read: it is not assigned on every \
path that reaches it, or it is blocked by the parallel threads of an `and`/\
`intersect` that both assign it (LRM 16.10, Annex F.5.4)"
),
scope,
)
}
struct Fragment {
entry: ThreadStateId,
exits: Vec<ThreadStateId>,
empty: bool,
flow: Flow,
clock: Option<Span>,
}
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
struct Span {
start: ClockId,
end: ClockId,
multi: bool,
}
impl Span {
fn single(c: ClockId) -> Self {
Span {
start: c,
end: c,
multi: false,
}
}
}
pub fn build_automaton<'d>(
root: AssertionExpr<'d>,
root_clock: Option<SemNode<'d>>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<(ir::Automaton, LeafTable<'d>), LoweringError> {
let mut automaton = blank_automaton();
let mut leaves = LeafTable::new(root_clock);
leaves.future_gclk = super::gclk::check(root, scope)?;
let frag = build_assertion(&mut automaton, &mut leaves, root, tree, scope)?;
finish_automaton(&mut automaton, frag);
Ok((automaton, leaves))
}
fn blank_automaton() -> ir::Automaton {
ir::Automaton {
states: Vec::new(),
start: ThreadStateId(0),
admits_empty: false,
first_match_groups: 0,
local_vars: Vec::new(),
end_points: Vec::new(),
entry_clock: ClockId(0),
}
}
fn finish_automaton(a: &mut ir::Automaton, frag: Fragment) {
a.entry_clock = frag.clock.map_or(ClockId(0), |s| s.start);
a.start = frag.entry;
a.admits_empty = frag.empty;
add_match_edges(a, frag.exits);
prune_unreachable(a);
}
fn add_match_edges(a: &mut ir::Automaton, exits: Vec<ThreadStateId>) {
let mut seen = HashSet::new();
for exit in exits {
if !seen.insert(exit) {
continue;
}
a.add_edge(
exit,
None,
Transition::Match {
actions: Vec::new(),
},
exit,
);
}
}
fn prune_unreachable(a: &mut ir::Automaton) {
prune_from(a, &[a.start]);
}
fn prune_from(a: &mut ir::Automaton, roots: &[ThreadStateId]) -> Vec<Option<ThreadStateId>> {
let mut new_id: Vec<Option<u32>> = vec![None; a.states.len()];
let mut order: Vec<ThreadStateId> = Vec::new();
let mut next = 0;
for &root in roots {
if new_id[root.0 as usize].is_none() {
new_id[root.0 as usize] = Some(order.len() as u32);
order.push(root);
}
while next < order.len() {
let s = order[next];
next += 1;
for e in &a.states[s.0 as usize].edges {
let slot = &mut new_id[e.target.0 as usize];
if slot.is_none() {
*slot = Some(order.len() as u32);
order.push(e.target);
}
}
}
}
let states = order
.iter()
.map(|s| {
let mut st = a.states[s.0 as usize].clone();
for e in &mut st.edges {
e.target = ThreadStateId(
new_id[e.target.0 as usize].expect("a reachable state's targets are reachable"),
);
}
st
})
.collect();
a.states = states;
a.start = roots
.first()
.and_then(|r| new_id[r.0 as usize])
.map_or(ThreadStateId(0), ThreadStateId);
new_id.into_iter().map(|n| n.map(ThreadStateId)).collect()
}
fn build_assertion<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
expr: AssertionExpr<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
match expr.kind() {
AssertionExprKind::Simple => build_simple(a, leaves, expr, tree, scope),
AssertionExprKind::SequenceConcat => build_concat(a, leaves, expr, tree, scope),
AssertionExprKind::SequenceWithMatch => {
build_sequence_with_match(a, leaves, expr, tree, scope)
}
AssertionExprKind::Binary => build_binary(a, leaves, expr, tree, scope),
AssertionExprKind::FirstMatch => build_first_match(a, leaves, expr, tree, scope),
AssertionExprKind::Clocking => build_clocking(a, leaves, expr, tree, scope),
other => Err(LoweringError::unsupported_at(
&format!(
"sva automaton builder: AssertionExprKind::{other:?} is a property expression, \
not a sequence (LRM 16.12.1): a sequence is built from Boolean operands, \
`##` concatenation, repetition, match items, first_match and the sequence \
operators and/or/intersect/throughout/within; the property operators are \
built by `build_property`"
),
scope,
)),
}
}
fn build_node<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
node: SemNode<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
if let Some(e) = node.as_expression() {
return build_operand(a, leaves, e, tree, scope);
}
if let Some(ae) = node.as_assertion_expr() {
return build_assertion(a, leaves, ae, tree, scope);
}
Err(LoweringError::unsupported_at(
"sva automaton builder: a sequence operand is neither an Expression nor an \
AssertionExpr (unexpected SemNode kind)",
scope,
))
}
fn build_leaf<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
leaf: Expression<'d>,
negated: bool,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let mut points = Vec::new();
collect_end_points(leaf, &mut points);
let entry = a.new_state();
let mut at = entry;
let mut flags = Vec::with_capacity(points.len());
for (method, inst) in points {
let built = build_end_point(a, leaves, method, inst, false, tree, scope)?;
let flag = a.new_local_var(1, false);
let next = a.new_state();
a.add_edge(
at,
None,
Transition::EndPoint {
point: built.point,
flag: Some(flag),
},
next,
);
flags.push(flag);
at = next;
}
let exit = a.new_state();
let id = leaves.push_leaf_flags(a, leaf, None, &flags, negated, scope)?;
a.add_edge(at, Some(id), Transition::Epsilon, exit);
Ok(Fragment {
entry,
exits: vec![exit],
empty: false,
flow: Flow::identity(),
clock: None,
})
}
fn empty_fragment(a: &mut ir::Automaton) -> Fragment {
Fragment {
entry: a.new_state(),
exits: Vec::new(),
empty: true,
flow: Flow::identity(),
clock: None,
}
}
fn build_simple<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
expr: AssertionExpr<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let kids = expr.children();
let [leaf_node] = kids.as_slice() else {
if kids.is_empty() {
return Err(LoweringError::unsupported_at(
"sva automaton builder: a Boolean operand has no semantic expression -- slang \
could not bind it, so the design has an error (check `Design::diagnostics()`; \
`named::check_formal_argument_rules` names the LRM 16.8/16.8.1 rule; also the \
case of an omitted checker actual (LRM 17.3) whose sequence/property default \
names a SIBLING formal of the same checker, e.g. `sequence s = req`, which \
slang does not bind -- pass the actual explicitly)",
scope,
));
}
return Err(LoweringError::unsupported_at(
&format!(
"sva automaton builder: Simple node must have exactly one child (its Boolean \
operand), found {}",
kids.len()
),
scope,
));
};
let leaf_expr = leaf_node.as_expression().ok_or_else(|| {
LoweringError::unsupported_at(
"sva automaton builder: Simple node's own child is not an Expression",
scope,
)
})?;
let syn = tree.syntax(&expr).ok_or_else(|| {
LoweringError::unsupported_at(
"sva automaton builder: Simple node has no syntax node in the given tree",
scope,
)
})?;
let syn = ranges::peel_sequence_parens(syn);
let simple_syn = SimpleSequenceExprSyntax::cast(syn).ok_or_else(|| {
LoweringError::unsupported_at(
&format!(
"sva automaton builder: expected SimpleSequenceExprSyntax, found {:?}",
syn.kind()
),
scope,
)
})?;
match simple_syn.repetition() {
None => build_operand(a, leaves, leaf_expr, tree, scope),
Some(rep) => {
if leaf_expr.kind() == ExpressionKind::AssertionInstance
&& matches!(rep.op().map(|t| t.text()), Some("->") | Some("="))
{
return Err(LoweringError::unsupported_at(
"goto/nonconsecutive repetition (`[->n:m]`/`[=n:m]`) cannot be applied to a \
named sequence instance (LRM 16.9.2: only a Boolean expression may carry \
it; only `[*...]`/`[+]` may repeat a sequence)",
scope,
));
}
build_repetition(
a,
leaves,
rep,
scope,
&mut |a, leaves| build_operand(a, leaves, leaf_expr, tree, scope),
&mut |a, leaves| build_gap_operand(a, leaves, leaf_expr, tree, scope),
)
}
}
}
const MAX_INSTANCE_DEPTH: usize = 128;
fn build_operand<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
e: Expression<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
if e.kind() == ExpressionKind::AssertionInstance {
build_instance(a, leaves, e, tree, scope)
} else if let Some((method, inst)) = end_point_call(e) {
build_end_point_guard(a, leaves, method, inst, tree, scope)
} else {
build_leaf(a, leaves, e, false, tree, scope)
}
}
fn build_gap_operand<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
e: Expression<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
if e.kind() == ExpressionKind::AssertionInstance {
return Err(LoweringError::unsupported_at(
"goto/nonconsecutive repetition (`[->n:m]`/`[=n:m]`) cannot be applied to a named \
sequence instance (LRM 16.9.2: only a Boolean expression may carry it)",
scope,
));
}
build_leaf(a, leaves, e, true, tree, scope)
}
fn build_end_point_guard<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
method: ir::EndMethod,
inst: Expression<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let built = build_end_point(a, leaves, method, inst, true, tree, scope)?;
let entry = a.new_state();
let exit = a.new_state();
a.add_edge(
entry,
None,
Transition::EndPoint {
point: built.point,
flag: None,
},
exit,
);
let mut flow = Flow::identity();
for v in built.flows_out {
flow = flow.concat(&Flow::assign(v));
}
Ok(Fragment {
entry,
exits: vec![exit],
empty: false,
flow,
clock: None,
})
}
struct BuiltEndPoint {
point: ir::EndPointId,
flows_out: Vec<LocalVarId>,
}
fn build_end_point<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
method: ir::EndMethod,
inst: Expression<'d>,
maximal: bool,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<BuiltEndPoint, LoweringError> {
let what = if method == ir::EndMethod::Triggered {
"triggered"
} else {
"matched"
};
for g in inst.assertion_arguments() {
if !g.port.assertion_port_is_local_var() {
continue;
}
let dir = g
.port
.assertion_port_direction()
.unwrap_or(ArgumentDirection::In);
if dir == ArgumentDirection::In || dir == ArgumentDirection::InOut {
return Err(LoweringError::unsupported_at(
&format!(
"the sequence method `.{what}` is applied to an instance of a sequence with \
the `input`/`inout` local variable formal argument `{}` (LRM 16.8.2: it is \
an error to apply `triggered` or `matched` to such an instance)",
g.port.name()
),
scope,
));
}
}
let prefix = a.local_vars.len() as u32;
let mut sub = blank_automaton();
sub.local_vars = a.local_vars.clone();
let saved_flow = std::mem::take(&mut leaves.flow_in);
let saved_shadows = std::mem::take(&mut leaves.shadows);
let touched = leaves.touched.len();
let built = build_instance(&mut sub, leaves, inst, tree, scope);
leaves.touched.truncate(touched);
leaves.shadows = saved_shadows;
leaves.flow_in = saved_flow;
let frag = built?;
let span = frag.clock;
let own_clock = span.and_then(|s| leaves.clock_event(s.start));
if method == ir::EndMethod::Triggered
&& let Some(s) = span
&& s.end != leaves.cur
{
return Err(LoweringError::unsupported_at(
"the sequence method `.triggered` is applied to an instance that ends on a different \
clock than the context it appears in (LRM 16.9.11, 16.13.5: the ending clock shall \
be the same; `.matched` synchronises two clocks)",
scope,
));
}
let flowing = frag.flow.flow_out(&VarSet::new());
finish_automaton(&mut sub, frag);
sub.entry_clock = span.map_or(leaves.cur, |s| s.start);
let flows_out: Vec<LocalVarId> = if maximal {
flowing.into_iter().filter(|v| v.0 < prefix).collect()
} else {
Vec::new()
};
let flow_out = flows_out
.iter()
.map(|&v| (v, leaves.phys_of(a, v)))
.collect();
let site = leaves.end_sites.len() as u32;
leaves.end_sites.push(EndSite {
method,
instance: inst,
clock: own_clock,
});
let point = a.new_end_point(ir::EndPoint {
method,
site,
automaton: sub,
flow_out,
});
Ok(BuiltEndPoint { point, flows_out })
}
fn build_instance<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
inst: Expression<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let origin = formal_reference_origin(tree.syntax(&inst), &leaves.env).map(<[_]>::to_vec);
let Some(origin) = origin else {
return expand_instance(a, leaves, inst, tree, scope);
};
let saved = std::mem::replace(&mut leaves.chain, origin);
let built = expand_instance(a, leaves, inst, tree, scope);
leaves.chain = saved;
built
}
fn formal_reference_origin<'e>(
syntax: Option<Node<'_>>,
env: &'e ranges::FormalEnv,
) -> Option<&'e [ranges::ChainLink]> {
let node = syntax?;
let ident = IdentifierNameSyntax::cast(node)?.identifier()?;
env.origin_of(&key(node), ident.value_text())
}
fn expand_instance<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
inst: Expression<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
if !inst.expr_type().is_some_and(|t| t.is_sequence_type()) {
return Err(LoweringError::unsupported_at(
"a property instance stands where a sequence is required (LRM 16.12.1: a property \
is not a sequence_expr, so it cannot be an operand of a sequence operator, a \
delay or a repetition; a property is built by `build_property`)",
scope,
));
}
let args = inst.assertion_arguments();
let body = inst
.as_sem_node()
.children()
.into_iter()
.find_map(|c| c.as_assertion_expr())
.ok_or_else(|| {
LoweringError::unsupported_at(
"sva automaton builder: a sequence instance has no body AssertionExpr",
scope,
)
})?;
let block_event = if body.kind() == AssertionExprKind::Clocking {
None
} else {
enclosing_clocking_event(body, tree, scope)?
};
let entered = enter_instance(a, leaves, inst, &args, true, tree, scope)?;
let built = match block_event {
Some(event) => build_clocked(a, leaves, event, body, tree, scope),
None => build_assertion(a, leaves, body, tree, scope),
};
let locals = leave_instance(leaves, entered);
match locals {
None => built,
Some(l) => finish_instance_locals(a, leaves, l, built?, scope),
}
}
struct EnteredInstance<'d> {
chain_len: usize,
pushed: bool,
caller_flow: VarSet,
locals: Option<InstanceLocals<'d>>,
}
fn enter_instance<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
inst: Expression<'d>,
args: &[sv_lang::AssertionInstanceArg<'d>],
check_cycle: bool,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<EnteredInstance<'d>, LoweringError> {
if leaves.instance_depth >= MAX_INSTANCE_DEPTH {
return Err(LoweringError::unsupported_at(
&format!(
"named sequence or property instances nest more than {MAX_INSTANCE_DEPTH} deep \
(a cyclic dependency among named sequences, LRM 16.8, a recursive property \
that does not terminate, or an absurd design)"
),
scope,
));
}
let frame = match args.first() {
None => None,
Some(first) => {
let seq = first.port.parent().ok_or_else(|| {
LoweringError::unsupported_at(
"sva automaton builder: a formal argument has no parent declaration",
scope,
)
})?;
let name = seq.name().to_string();
let decl = key(tree.syntax(&seq).ok_or_else(|| {
LoweringError::unsupported_at(
&format!(
"`{name}` has no syntax node in any source file of the compilation, so \
its formals cannot be bound (a declaration slang made up)"
),
scope,
)
})?);
if check_cycle && leaves.chain.iter().any(|(_, d)| *d == decl) {
let walk: Vec<String> = leaves
.chain
.iter()
.map(|(n, _)| n.as_str())
.chain(std::iter::once(name.as_str()))
.map(|n| format!("`{n}`"))
.collect();
return Err(LoweringError::unsupported_at(
&format!(
"cyclic dependency among named sequences (LRM 16.8): `{name}` is \
instantiated while it is already being expanded ({})",
walk.join(" -> ")
),
scope,
));
}
let mut here = leaves.chain.clone();
here.push((name.clone(), decl.clone()));
let mut bindings = Vec::new();
let mut origins = Vec::new();
for g in args {
let actual = actual_syntax(g.actual, tree);
bindings.push((
g.port.name().to_string(),
ranges::bind_actual(actual, formal_cast(&g.port), scope, &leaves.env),
));
let origin = formal_reference_origin(actual, &leaves.env)
.map_or_else(|| here.clone(), <[_]>::to_vec);
origins.push((g.port.name().to_string(), origin));
}
Some((
ranges::FormalFrame {
name: name.clone(),
decl: decl.clone(),
bindings,
origins,
},
(name, decl),
))
}
};
let caller_flow = leaves.flow_in.clone();
let locals = begin_instance_locals(a, leaves, inst, args, scope)?;
if let Some(l) = &locals {
leaves.flow_in = l.x_body.clone();
}
let chain_len = leaves.chain.len();
let pushed = frame.is_some();
if let Some((f, link)) = frame {
leaves.env.push(f);
leaves.chain.push(link);
}
leaves.instance_depth += 1;
leaves.inferred.push(leaves.clocks[leaves.cur.0 as usize]);
Ok(EnteredInstance {
chain_len,
pushed,
caller_flow,
locals,
})
}
fn leave_instance<'d>(
leaves: &mut LeafTable<'d>,
entered: EnteredInstance<'d>,
) -> Option<InstanceLocals<'d>> {
leaves.instance_depth -= 1;
leaves.inferred.pop();
leaves.chain.truncate(entered.chain_len);
if entered.pushed {
leaves.env.pop();
}
leaves.flow_in = entered.caller_flow;
entered.locals
}
struct InstanceLocals<'d> {
syms: Vec<Symbol<'d>>,
slots: Vec<LocalVarId>,
own: VarSet,
init: Vec<Transition>,
x_body: VarSet,
write_back: Vec<(LocalVarId, LocalVarId, String)>,
scope_len: usize,
}
fn local_actual<'d>(actual: SemNode<'d>) -> Option<Symbol<'d>> {
let mut e = actual.as_expression()?;
while e.kind() == ExpressionKind::Conversion {
e = e
.as_sem_node()
.children()
.into_iter()
.next()?
.as_expression()?;
}
if e.kind() != ExpressionKind::NamedValue {
return None;
}
e.referenced_symbol()
.filter(|s| s.kind() == SymbolKind::LocalAssertionVar)
}
fn begin_instance_locals<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
inst: Expression<'d>,
args: &[sv_lang::AssertionInstanceArg<'d>],
scope: &Symbol<'d>,
) -> Result<Option<InstanceLocals<'d>>, LoweringError> {
let syms = inst.assertion_local_vars();
let local_formals: Vec<_> = args
.iter()
.filter(|g| g.port.assertion_port_is_local_var())
.collect();
if syms.is_empty() {
if let Some(g) = local_formals.first() {
return Err(LoweringError::unsupported_at(
&format!(
"sva automaton builder: `local` formal `{}` has no local variable in the \
sequence body",
g.port.name()
),
scope,
));
}
return Ok(None);
}
let scope_len = leaves.scope.len();
let mut own = VarSet::new();
let mut slots = Vec::with_capacity(syms.len());
for sym in &syms {
let slot = leaves.declare(a, *sym, scope)?;
own.insert(slot);
slots.push(slot);
}
let slot_of = |name: &str| -> Option<LocalVarId> {
syms.iter().position(|s| s.name() == name).map(|i| slots[i])
};
let mut x = leaves.flow_in.clone();
let mut init = Vec::new();
let mut write_back = Vec::new();
let mut bound = BTreeSet::new();
for g in local_formals {
let name = g.port.name().to_string();
let slot = slot_of(&name).ok_or_else(|| {
LoweringError::unsupported_at(
&format!(
"sva automaton builder: `local` formal `{name}` has no local variable in the \
sequence body"
),
scope,
)
})?;
let dir = g
.port
.assertion_port_direction()
.unwrap_or(ArgumentDirection::In);
match dir {
ArgumentDirection::Ref => {
return Err(LoweringError::unsupported_at(
&format!(
"`local` formal `{name}` is a `ref` argument; a local variable formal \
argument is `input`, `inout` or `output` (LRM 16.8.2)"
),
scope,
));
}
ArgumentDirection::In | ArgumentDirection::InOut => {
leaves.flow_in = x.clone();
let actual = g.actual.as_expression().ok_or_else(|| {
LoweringError::unsupported_at(
&format!("the actual of `local` formal `{name}` is not an expression"),
scope,
)
})?;
let phys = leaves.phys_of(a, slot);
for (var, value) in leaves.slot_leaves(a, phys, actual, None, scope)? {
init.push(Transition::LocalVarWrite { var, value });
}
x.insert(slot);
}
ArgumentDirection::Out => {}
}
if matches!(dir, ArgumentDirection::Out | ArgumentDirection::InOut) {
let target = local_actual(g.actual).ok_or_else(|| {
LoweringError::unsupported_at(
&format!(
"the actual of the `{}` formal `{name}` must be a local variable (LRM \
16.8.2)",
if dir == ArgumentDirection::Out {
"output"
} else {
"inout"
}
),
scope,
)
})?;
let actual = leaves.resolve(target, scope)?;
if !bound.insert(actual) {
return Err(LoweringError::unsupported_at(
&format!(
"the local variable `{}` is bound to two or more `inout`/`output` \
`local` formal arguments of one instance, the second being `{name}` \
(LRM 16.8.2)",
target.name()
),
scope,
));
}
write_back.push((slot, actual, name));
}
}
for (sym, &slot) in syms.iter().zip(&slots) {
if let Some(initializer) = sym.initializer() {
leaves.flow_in = x.clone();
let phys = leaves.phys_of(a, slot);
for (var, value) in leaves.slot_leaves(a, phys, initializer, None, scope)? {
init.push(Transition::LocalVarWrite { var, value });
}
x.insert(slot);
}
}
Ok(Some(InstanceLocals {
syms,
slots,
own,
init,
x_body: x,
write_back,
scope_len,
}))
}
fn finish_instance_locals<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
il: InstanceLocals<'d>,
body: Fragment,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
leaves.scope.truncate(il.scope_len);
if !il.write_back.is_empty() {
if body.empty {
return Err(LoweringError::unsupported_at(
"a named sequence with a `local` output or inout formal argument admits an \
empty match, which has no end to write the formal back at (LRM 16.8.2)",
scope,
));
}
let out = body.flow.flow_out(&il.x_body);
for (formal, _, name) in &il.write_back {
if !out.contains(formal) {
return Err(not_flowing(name, scope));
}
}
}
let mut flow = body.flow.scoped(&il.own);
let mut copies = Vec::with_capacity(il.write_back.len());
for &(formal, actual, _) in &il.write_back {
let dst = leaves.phys_of(a, actual);
copies.push(Transition::LocalVarCopy { dst, src: formal });
flow = flow.concat(&Flow::assign(actual));
}
let entry = if body.exits.is_empty() {
body.entry
} else {
prefix_actions(a, il.init, body.entry)
};
let exits = suffix_actions(a, body.exits, copies);
Ok(Fragment {
entry,
exits,
empty: body.empty,
flow,
clock: body.clock,
})
}
fn formal_cast(port: &Symbol<'_>) -> Option<ranges::FormalCast> {
let ty = port.declared_type()?;
if !ty.is_integral() || ty.is_untyped_type() {
return None;
}
Some(ranges::FormalCast {
width: ty.bit_width(),
signed: ty.is_signed(),
})
}
fn actual_syntax<'t>(actual: SemNode<'_>, tree: Trees<'t>) -> Option<Node<'t>> {
let e = actual.as_expression()?;
if let Some(s) = tree.syntax(&e) {
return Some(s);
}
if e.kind() == ExpressionKind::Conversion {
let inner = e.as_sem_node().children().into_iter().next()?;
return actual_syntax(inner, tree);
}
None
}
fn build_clocking<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
expr: AssertionExpr<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let ch = super::op::clocking_children(expr, scope)?;
build_clocked(a, leaves, ch.event, ch.body, tree, scope)
}
fn build_clocked<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
event: SemNode<'d>,
body: AssertionExpr<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let id = leaves.resolve_clock(event, scope)?;
let saved = std::mem::replace(&mut leaves.cur, id);
let built = build_assertion(a, leaves, body, tree, scope);
leaves.cur = saved;
let mut frag = built?;
frag.clock = Some(frag.clock.unwrap_or(Span::single(id)));
Ok(frag)
}
pub(super) fn enclosing_clocking_event<'d>(
body: AssertionExpr<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Option<SemNode<'d>>, LoweringError> {
use sv_lang::kinds::SyntaxKind;
let declaration_of = |mut node: Node<'_>| -> Option<std::ops::Range<usize>> {
loop {
if node.kind() == SyntaxKind::ClockingDeclaration {
return Some(key(node));
}
node = node.parent()?;
}
};
let Some(range) = tree.syntax(&body).and_then(declaration_of) else {
return Ok(None);
};
let inst = sv_sim_sim::netlist::enclosing_instance_body(scope).unwrap_or(*scope);
let mut chain = Vec::new();
let mut up = Some(*scope);
while let Some(s) = up {
chain.push(s);
up = s.parent();
}
let candidates: Vec<Symbol<'d>> = sv_sim_sim::netlist::module_items(&inst)
.into_iter()
.filter(|m| m.kind() == SymbolKind::ClockingBlock)
.filter(|cb| {
tree.syntax(cb)
.and_then(declaration_of)
.is_some_and(|r| r == range)
})
.collect();
let cb = candidates
.iter()
.find(|cb| cb.parent().is_some_and(|p| chain.contains(&p)))
.or_else(|| candidates.first())
.copied();
let Some(cb) = cb else {
return Err(LoweringError::unsupported_at(
"a property or sequence declared in a clocking block of another instance than the \
assertion's is not executable yet (its clocking event is not reachable from the \
assertion's scope)",
scope,
));
};
cb.clocking_block_event().map(Some).ok_or_else(|| {
LoweringError::unsupported_at(
&format!("the clocking block `{}` has no clocking event", cb.name()),
scope,
)
})
}
pub(super) fn is_inferred_clock_event(event: SemNode<'_>) -> bool {
if let Some(e) = event.as_expression() {
return e.call_subroutine_name().as_deref() == Some("$inferred_clock");
}
match event.children().as_slice() {
[only] => is_inferred_clock_event(*only),
_ => false,
}
}
pub(super) fn events_equivalent(a: SemNode<'_>, b: SemNode<'_>) -> bool {
match (a.as_expression(), b.as_expression()) {
(Some(x), Some(y)) => return x.is_equivalent_to(&y),
(None, None) => {}
_ => return false,
}
let (Some(x), Some(y)) = (a.as_timing_control(), b.as_timing_control()) else {
return false;
};
if x.kind() != y.kind() || x.edge() != y.edge() {
return false;
}
let (xs, ys) = (a.children(), b.children());
xs.len() == ys.len() && xs.iter().zip(&ys).all(|(p, q)| events_equivalent(*p, *q))
}
fn build_concat<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
expr: AssertionExpr<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let kids = expr.children();
let delays = ranges::sequence_range_of_in(expr, tree, scope, &leaves.env)?;
let leading = kids.len() == delays.len();
if !leading && kids.len() != delays.len() + 1 {
return Err(LoweringError::unsupported_at(
&format!(
"sva automaton builder: SequenceConcat has {} semantic children but {} \
recovered delay(s) -- expected children.len() == delays.len() (a leading \
delay) or delays.len() + 1",
kids.len(),
delays.len()
),
scope,
));
}
let x0 = leaves.flow_in.clone();
let (mut frag, first_operand) = if leading {
(empty_fragment(a), 0)
} else {
(build_node(a, leaves, kids[0], tree, scope)?, 1)
};
for (i, delay) in delays.iter().enumerate() {
if delay.max.is_some_and(|max| delay.min > max) {
return Err(LoweringError::unsupported_at(
&format!(
"sva automaton builder: `##` delay range has min ({}) > max ({})",
delay.min,
delay.max.unwrap_or_default()
),
scope,
));
}
let mut d = *delay;
if leading && i == 0 {
let widen = |v: u32| {
v.checked_add(1).ok_or_else(|| {
LoweringError::unsupported_at(
"sva automaton builder: leading `##` delay bound overflows u32",
scope,
)
})
};
d = SequenceRangeValue {
min: widen(d.min)?,
max: d.max.map(widen).transpose()?,
};
}
leaves.flow_in = frag.flow.flow_out(&x0);
let next = build_node(a, leaves, kids[i + first_operand], tree, scope)?;
frag = concat_clocked(a, leaves, frag, d, next, scope)?;
}
leaves.flow_in = x0;
Ok(frag)
}
fn concat_clocked<'d>(
a: &mut ir::Automaton,
leaves: &LeafTable<'d>,
l: Fragment,
d: SequenceRangeValue,
r: Fragment,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let ls = l.clock.unwrap_or(Span::single(leaves.cur));
let rs = r.clock.unwrap_or(Span::single(leaves.cur));
let stamped = if l.clock.is_none() && r.clock.is_none() {
None
} else {
Some(Span {
start: ls.start,
end: rs.end,
multi: ls.multi || rs.multi || ls.end != rs.start,
})
};
if ls.end == rs.start {
let mut f = concat(a, l, d, r);
f.clock = stamped;
return Ok(f);
}
let strict = match (d.min, d.max) {
(0, Some(0)) => false,
(1, Some(1)) => true,
_ => {
return Err(LoweringError::unsupported_at(
"a `##` delay between differently clocked operands of a multiclocked sequence \
must be exactly `##1` or `##0` (LRM 16.13.1: the first synchronises to the \
nearest strictly subsequent tick of the second operand's clock, the second to \
the nearest possibly overlapping one); a range or a longer delay has no \
meaning across a clock change",
scope,
));
}
};
if l.empty || r.empty {
return Err(LoweringError::unsupported_at(
"a maximal singly clocked subsequence of a multiclocked sequence admits an empty \
match (LRM 16.13.1: it shall admit only nonempty matches), e.g. a leading `##n` \
delay or a `[*0]`/`[*0:n]` repetition next to a clock change",
scope,
));
}
let flow = l.flow.concat(&r.flow);
for &e in &l.exits {
a.add_edge(
e,
None,
Transition::ClockSync {
to: rs.start,
strict,
},
r.entry,
);
}
Ok(Fragment {
entry: l.entry,
exits: r.exits,
empty: false,
flow,
clock: stamped,
})
}
fn join_clocks<'d>(
leaves: &LeafTable<'d>,
operands: &[&Fragment],
what: &str,
scope: &Symbol<'d>,
) -> Result<Option<Span>, LoweringError> {
if operands.iter().all(|f| f.clock.is_none()) {
return Ok(None);
}
let resolved: Vec<Span> = operands
.iter()
.map(|f| f.clock.unwrap_or(Span::single(leaves.cur)))
.collect();
let first = resolved[0];
if resolved.iter().any(|s| s.multi || s.start != first.start) {
return Err(LoweringError::unsupported_at(
&format!(
"the operands of `{what}` are clocked differently or are multiclocked \
sequences (LRM 16.13.1: a multiclocked sequence is built only with `##1`/`##0` \
between singly clocked subsequences; `{what}` needs its operands on one clock)"
),
scope,
));
}
Ok(Some(first))
}
fn single_clock(f: &Fragment, what: &str) -> Result<Option<Span>, String> {
if f.clock.is_some_and(|s| s.multi) {
return Err(format!(
"{what} is applied to a multiclocked sequence (LRM 16.13.1: only a singly clocked \
sequence can be repeated or have its first match selected; the match set of a \
clock change inside a repeated operand is not defined by Annex F)"
));
}
Ok(f.clock)
}
fn concat(a: &mut ir::Automaton, l: Fragment, d: SequenceRangeValue, r: Fragment) -> Fragment {
let flow = l.flow.concat(&r.flow);
let mut f = concat_shape(a, l, d, r);
f.flow = flow;
f
}
fn concat_shape(
a: &mut ir::Automaton,
l: Fragment,
d: SequenceRangeValue,
r: Fragment,
) -> Fragment {
if d.min == 1 && d.max == Some(1) {
if l.empty && l.exits.is_empty() {
return r;
}
if r.empty && r.exits.is_empty() {
return l;
}
}
let ne_l = !l.exits.is_empty();
let ne_r = !r.exits.is_empty();
let k1_min = d.min.max(1);
let k1_ok = d.max.is_none_or(|m| m >= k1_min);
let k2_min = d.min.max(2);
let k2_ok = d.max.is_none_or(|m| m >= k2_min);
let path_a = ne_l && ne_r;
let path_b = l.empty && ne_r && k1_ok;
let path_c = ne_l && r.empty && k1_ok;
let path_d = l.empty && r.empty && k2_ok;
let start = if l.empty {
let s = a.new_state();
if path_a || path_c {
a.add_edge(s, None, Transition::Epsilon, l.entry);
}
Some(s)
} else {
None
};
let entry = start.unwrap_or(l.entry);
if path_a {
for &e in &l.exits {
a.add_edge(
e,
None,
Transition::Delay {
min: d.min,
max: d.max,
},
r.entry,
);
}
}
if path_b {
let s = start.expect("path_b implies l.empty");
a.add_edge(
s,
None,
Transition::Delay {
min: k1_min - 1,
max: d.max.map(|m| m - 1),
},
r.entry,
);
}
let tail = (path_c || path_d).then(|| a.new_state());
if let Some(t) = tail {
if path_c {
for &e in &l.exits {
a.add_edge(
e,
None,
Transition::Delay {
min: k1_min - 1,
max: d.max.map(|m| m - 1),
},
t,
);
}
}
if path_d {
let s = start.expect("path_d implies l.empty");
a.add_edge(
s,
None,
Transition::Delay {
min: k2_min - 2,
max: d.max.map(|m| m - 2),
},
t,
);
}
}
let mut exits = Vec::new();
if path_a || path_b {
exits.extend(r.exits.iter().copied());
}
exits.extend(tail);
Fragment {
entry,
exits,
empty: l.empty && r.empty && d.min <= 1 && d.max.is_none_or(|m| m >= 1),
flow: Flow::identity(),
clock: None,
}
}
fn build_sequence_with_match<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
expr: AssertionExpr<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let syn = tree.syntax(&expr).ok_or_else(|| {
LoweringError::unsupported_at(
"sva automaton builder: SequenceWithMatch node has no syntax node in the given tree",
scope,
)
})?;
let syn = ranges::peel_sequence_parens(syn);
let paren = ParenthesizedSequenceExprSyntax::cast(syn).ok_or_else(|| {
LoweringError::unsupported_at(
&format!(
"sva automaton builder: expected ParenthesizedSequenceExprSyntax for a \
SequenceWithMatch node, found {:?}",
syn.kind()
),
scope,
)
})?;
let kids = expr.children();
let sub_kids: Vec<SemNode<'d>> = kids
.iter()
.copied()
.filter(|c| c.as_assertion_expr().is_some())
.collect();
let [sub_node] = sub_kids.as_slice() else {
return Err(LoweringError::unsupported_at(
&format!(
"sva automaton builder: SequenceWithMatch must have exactly one sub-sequence \
child, found {}",
sub_kids.len()
),
scope,
));
};
let sub = sub_node
.as_assertion_expr()
.expect("filtered above to only AssertionExpr-castable nodes");
let has_match_items = paren.match_list().is_some();
let items: Vec<SemNode<'d>> = kids
.iter()
.copied()
.filter(|c| c.as_assertion_expr().is_none())
.collect();
match paren.repetition() {
None => {
if has_match_items {
return build_match_items(a, leaves, sub, &items, tree, scope);
}
build_assertion(a, leaves, sub, tree, scope)
}
Some(rep) => {
let op_text = rep.op().map(|t| t.text());
if has_match_items && matches!(op_text, Some("->") | Some("=")) {
return Err(LoweringError::unsupported_at(
"goto/nonconsecutive repetition (`[->n:m]`/`[=n:m]`) applied to a sequence \
that also carries a match item is illegal (LRM 16.9.2/16.10's own worked \
example, `(b, v=e)[->2]`)",
scope,
));
}
build_repetition(
a,
leaves,
rep,
scope,
&mut |a, leaves| {
if has_match_items {
build_match_items(a, leaves, sub, &items, tree, scope)
} else {
build_assertion(a, leaves, sub, tree, scope)
}
},
&mut |a, leaves| {
let plain = tree.syntax(&sub).is_some_and(|syn| {
SimpleSequenceExprSyntax::cast(ranges::peel_sequence_parens(syn))
.is_some_and(|s| s.repetition().is_none())
});
let boolean = (sub.kind() == AssertionExprKind::Simple && plain)
.then(|| sub.children())
.and_then(|kids| match kids.as_slice() {
[only] => only.as_expression(),
_ => None,
});
match boolean {
Some(e) => build_gap_operand(a, leaves, e, tree, scope),
None => Err(LoweringError::unsupported_at(
"goto/nonconsecutive repetition (`[->n:m]`/`[=n:m]`) can only be \
applied to a Boolean expression, not a compound sequence (LRM \
16.9.2)",
scope,
)),
}
},
)
}
}
}
fn build_match_items<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
sub: AssertionExpr<'d>,
items: &[SemNode<'d>],
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let x0 = leaves.flow_in.clone();
let frag = build_assertion(a, leaves, sub, tree, scope)?;
attach_match_items(a, leaves, frag, items, &x0, scope)
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
enum MatchItemKind {
Assignment,
Step(i64),
Call,
}
fn classify_match_item(
e: Expression<'_>,
scope: &Symbol<'_>,
) -> Result<MatchItemKind, LoweringError> {
let ek = e.kind();
if ek == ExpressionKind::Assignment {
return Ok(MatchItemKind::Assignment);
}
if ek == ExpressionKind::UnaryOp
&& let Some(op) = e.unary_op()
{
if matches!(op, UnaryOp::Preincrement | UnaryOp::Postincrement) {
return Ok(MatchItemKind::Step(1));
}
if matches!(op, UnaryOp::Predecrement | UnaryOp::Postdecrement) {
return Ok(MatchItemKind::Step(-1));
}
}
if actions::is_call(e) {
return Ok(MatchItemKind::Call);
}
Err(LoweringError::unsupported_at(
&format!(
"a sequence match item of kind {ek:?} is not a local-variable assignment, an \
increment/decrement or a subroutine call (LRM 16.11)"
),
scope,
))
}
fn match_item_target<'d>(
leaves: &LeafTable<'d>,
target: Expression<'d>,
what: &str,
scope: &Symbol<'d>,
) -> Result<(Symbol<'d>, LocalVarId), LoweringError> {
let sym = target
.referenced_symbol()
.filter(|s| {
target.kind() == ExpressionKind::NamedValue && s.kind() == SymbolKind::LocalAssertionVar
})
.ok_or_else(|| {
LoweringError::unsupported_at(
&format!(
"a sequence match item must {what} a whole local variable (LRM 16.11); an \
operation on anything else is not a match item"
),
scope,
)
})?;
Ok((sym, leaves.resolve(sym, scope)?))
}
fn attach_match_items<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
frag: Fragment,
items: &[SemNode<'d>],
x0: &VarSet,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
if frag.empty {
return Err(LoweringError::unsupported_at(
"a sequence match item is attached to a sequence that admits an empty match \
(LRM 16.11: it shall be an error to attach a match item to such a sequence)",
scope,
));
}
let mut flow = frag.flow.clone();
let mut actions = Vec::with_capacity(items.len());
for item in items {
let item_expr = item.as_expression().ok_or_else(|| {
LoweringError::unsupported_at(
"sva automaton builder: a sequence match item is not an Expression",
scope,
)
})?;
match classify_match_item(item_expr, scope)? {
MatchItemKind::Call => {
if is_local_collection_method(item_expr) {
continue;
}
leaves.flow_in = flow.flow_out(x0);
actions.push(actions::lower_call(a, leaves, item_expr, scope)?);
continue;
}
MatchItemKind::Step(delta) => {
let kids = item_expr.as_sem_node().children();
let [operand] = kids.as_slice() else {
return Err(LoweringError::unsupported_at(
"sva automaton builder: an increment/decrement match item must have \
exactly one operand",
scope,
));
};
let operand = operand.as_expression().ok_or_else(|| {
LoweringError::unsupported_at(
"sva automaton builder: an increment/decrement operand is not an \
Expression",
scope,
)
})?;
let (sym, canon) =
match_item_target(leaves, operand, "increment or decrement", scope)?;
leaves.flow_in = flow.flow_out(x0);
leaves.check_flows(sym, canon, scope)?;
let phys = leaves.phys_of(a, canon);
actions.push(Transition::LocalVarStep { var: phys, delta });
flow = flow.concat(&Flow::assign(canon));
continue;
}
MatchItemKind::Assignment => {}
}
let kids = item_expr.as_sem_node().children();
let [lhs, rhs] = kids.as_slice() else {
return Err(LoweringError::unsupported_at(
"sva automaton builder: an assignment match item must have a target and a value",
scope,
));
};
let (lhs, rhs) = (
lhs.as_expression().ok_or_else(|| {
LoweringError::unsupported_at(
"sva automaton builder: a match item's target is not an Expression",
scope,
)
})?,
rhs.as_expression().ok_or_else(|| {
LoweringError::unsupported_at(
"sva automaton builder: a match item's value is not an Expression",
scope,
)
})?,
);
let (_, canon) = match_item_target(leaves, lhs, "assign", scope)?;
leaves.flow_in = flow.flow_out(x0);
let phys = leaves.phys_of(a, canon);
actions.extend(leaves.assign_var(a, canon, phys, rhs, scope)?);
flow = flow.concat(&Flow::assign(canon));
}
leaves.flow_in = x0.clone();
let exits = suffix_actions(a, frag.exits, actions);
Ok(Fragment {
entry: frag.entry,
exits,
empty: false,
flow,
clock: frag.clock,
})
}
fn build_repetition<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
rep: SequenceRepetitionSyntax<'_>,
scope: &Symbol<'d>,
make_unit: &mut dyn FnMut(
&mut ir::Automaton,
&mut LeafTable<'d>,
) -> Result<Fragment, LoweringError>,
make_gap: &mut dyn FnMut(
&mut ir::Automaton,
&mut LeafTable<'d>,
) -> Result<Fragment, LoweringError>,
) -> Result<Fragment, LoweringError> {
let op_text = rep.op().map(|t| t.text()).ok_or_else(|| {
LoweringError::unsupported_at(
"sva automaton builder: `[...]` repetition has no operator token",
scope,
)
})?;
let range = ranges::repetition_range_in(rep, scope, &leaves.env)?;
match op_text {
"*" | "+" => build_repeated(
a,
leaves,
range.min,
range.max,
SequenceRangeValue {
min: 1,
max: Some(1),
},
make_unit,
),
"->" | "=" => build_goto(
a,
leaves,
op_text == "=",
(range.min, range.max),
make_unit,
make_gap,
),
other => Err(LoweringError::unsupported_at(
&format!("sva automaton builder: unknown sequence repetition operator {other:?}"),
scope,
)),
}
}
fn build_goto<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
nonconsecutive: bool,
(min, max): (u32, Option<u32>),
make_unit: &mut dyn FnMut(
&mut ir::Automaton,
&mut LeafTable<'d>,
) -> Result<Fragment, LoweringError>,
make_gap: &mut dyn FnMut(
&mut ir::Automaton,
&mut LeafTable<'d>,
) -> Result<Fragment, LoweringError>,
) -> Result<Fragment, LoweringError> {
let one = SequenceRangeValue {
min: 1,
max: Some(1),
};
let body = {
let mut repeat = |a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>|
-> Result<Fragment, LoweringError> {
let gap = build_repeated(a, leaves, 0, None, one, make_gap)?;
let hit = make_unit(a, leaves)?;
Ok(concat(a, gap, one, hit))
};
build_repeated(a, leaves, min, max, one, &mut repeat)?
};
if !nonconsecutive {
return Ok(body);
}
let tail = build_repeated(a, leaves, 0, None, one, make_gap)?;
Ok(concat(a, body, one, tail))
}
fn build_repeated<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
min: u32,
max: Option<u32>,
link: SequenceRangeValue,
make_unit: &mut dyn FnMut(
&mut ir::Automaton,
&mut LeafTable<'d>,
) -> Result<Fragment, LoweringError>,
) -> Result<Fragment, LoweringError> {
if max.is_some_and(|m| min > m) {
return Err(LoweringError::unsupported(
&format!(
"sequence repetition range min ({min}) > max ({})",
max.unwrap_or_default()
),
"sva::build::build_repeated",
));
}
if max == Some(0) {
return Ok(empty_fragment(a));
}
let x0 = leaves.flow_in.clone();
let first = make_unit(a, leaves)?;
let min = if first.empty { 0 } else { min };
let clock = single_clock(&first, "a sequence repetition")
.map_err(|msg| LoweringError::unsupported(&msg, "sva::build::build_repeated"))?;
if first.exits.is_empty() {
return Ok(Fragment {
entry: first.entry,
exits: Vec::new(),
empty: min == 0,
flow: Flow::identity(),
clock,
});
}
let built = match max {
Some(max) => build_repeated_finite(a, leaves, &x0, first, (min, max), link, make_unit),
None => build_repeated_unbounded(a, leaves, &x0, first, min, link, make_unit),
};
leaves.flow_in = x0;
built.map(|f| Fragment { clock, ..f })
}
fn link_all(
a: &mut ir::Automaton,
from: &[ThreadStateId],
link: SequenceRangeValue,
target: ThreadStateId,
) {
for &e in from {
a.add_edge(
e,
None,
Transition::Delay {
min: link.min,
max: link.max,
},
target,
);
}
}
fn build_repeated_finite<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
x0: &VarSet,
first: Fragment,
(min, max): (u32, u32),
link: SequenceRangeValue,
make_unit: &mut dyn FnMut(
&mut ir::Automaton,
&mut LeafTable<'d>,
) -> Result<Fragment, LoweringError>,
) -> Result<Fragment, LoweringError> {
let entry = first.entry;
let mut prev_exits = first.exits.clone();
let mut copy_exits: Vec<Vec<ThreadStateId>> = Vec::with_capacity(max as usize);
copy_exits.push(first.exits);
let mut acc: Vec<Flow> = Vec::with_capacity(max as usize);
acc.push(first.flow);
for k in 1..max as usize {
leaves.flow_in = acc[k - 1].flow_out(x0);
let unit = make_unit(a, leaves)?;
link_all(a, &prev_exits, link, unit.entry);
prev_exits = unit.exits.clone();
copy_exits.push(unit.exits);
let chained = acc[k - 1].concat(&unit.flow);
acc.push(chained);
}
let mut exits = Vec::new();
let mut flow: Option<Flow> = (min == 0).then(Flow::identity);
for k in min.max(1)..=max {
exits.extend(copy_exits[(k - 1) as usize].iter().copied());
let f = &acc[(k - 1) as usize];
flow = Some(match flow {
None => f.clone(),
Some(so_far) => so_far.or(f),
});
}
Ok(Fragment {
entry,
exits,
empty: min == 0,
flow: flow.unwrap_or_default(),
clock: None,
})
}
fn build_repeated_unbounded<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
x0: &VarSet,
first: Fragment,
min: u32,
link: SequenceRangeValue,
make_unit: &mut dyn FnMut(
&mut ir::Automaton,
&mut LeafTable<'d>,
) -> Result<Fragment, LoweringError>,
) -> Result<Fragment, LoweringError> {
let mandatory = min.max(1);
let entry = first.entry;
let mut tail_exits = first.exits;
let mut acc = first.flow;
for _ in 1..mandatory {
leaves.flow_in = acc.flow_out(x0);
let unit = make_unit(a, leaves)?;
link_all(a, &tail_exits, link, unit.entry);
tail_exits = unit.exits;
acc = acc.concat(&unit.flow);
}
leaves.flow_in = acc.flow_out(x0);
let loop_unit = make_unit(a, leaves)?;
link_all(a, &tail_exits, link, loop_unit.entry);
link_all(a, &loop_unit.exits, link, loop_unit.entry);
let mut exits = tail_exits;
exits.extend(loop_unit.exits);
let looped = Flow {
sample: loop_unit.flow.sample,
block: loop_unit.flow.block,
flow0: VarSet::new(),
};
let mut flow = acc.concat(&looped);
if min == 0 {
flow = flow.or_empty();
}
Ok(Fragment {
entry,
exits,
empty: min == 0,
flow,
clock: None,
})
}
const MAX_PRODUCT_STATES: usize = 20_000;
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
enum ProductKind {
Intersect,
And,
}
impl ProductKind {
fn name(self) -> &'static str {
match self {
ProductKind::Intersect => "intersect",
ProductKind::And => "and",
}
}
}
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
enum Comp {
Real(ThreadStateId),
Wait {
target: ThreadStateId,
lo: u32,
hi: Option<u32>,
},
Done,
}
impl Comp {
fn wait(target: ThreadStateId, lo: u32, hi: Option<u32>) -> Comp {
if lo == 0 && hi == Some(0) {
Comp::Real(target)
} else {
Comp::Wait { target, lo, hi }
}
}
fn tick(self) -> Option<Comp> {
match self {
Comp::Real(_) => None,
Comp::Wait { target, lo, hi } => Some(Comp::wait(
target,
lo.saturating_sub(1),
hi.map(|h| h.saturating_sub(1)),
)),
Comp::Done => Some(Comp::Done),
}
}
}
struct Move {
guard: Option<LeafId>,
label: Transition,
to: Comp,
}
fn comp_moves(
a: &ir::Automaton,
c: Comp,
exits: &HashSet<ThreadStateId>,
kind: ProductKind,
scope: &Symbol<'_>,
) -> Result<Vec<Move>, LoweringError> {
let mut out = Vec::new();
match c {
Comp::Done => {}
Comp::Wait { target, lo, .. } => {
if lo == 0 {
out.push(Move {
guard: None,
label: Transition::Epsilon,
to: Comp::Real(target),
});
}
}
Comp::Real(s) => {
for e in &a.state(s).edges {
let (label, to) = match &e.label {
Transition::Epsilon => (Transition::Epsilon, Comp::Real(e.target)),
Transition::Delay { min, max } => {
if max.is_some_and(|m| *min > m) {
continue;
}
(Transition::Epsilon, Comp::wait(e.target, *min, *max))
}
Transition::FirstMatchBegin { .. }
| Transition::FirstMatchEnd { .. }
| Transition::LocalVarWrite { .. }
| Transition::LocalVarCopy { .. }
| Transition::LocalVarStep { .. } => (e.label.clone(), Comp::Real(e.target)),
Transition::EndPoint { .. } => (e.label.clone(), Comp::Real(e.target)),
Transition::Match { .. }
| Transition::Abort { .. }
| Transition::ClockSync { .. }
| Transition::SubroutineCall { .. } => {
return Err(LoweringError::unsupported_at(
&format!(
"sva automaton builder: `{}` operand contains a {} edge, which \
the lockstep product does not know how to compose",
kind.name(),
e.label.kind_name()
),
scope,
));
}
};
out.push(Move {
guard: e.guard,
label,
to,
});
}
if kind == ProductKind::And && exits.contains(&s) {
out.push(Move {
guard: None,
label: Transition::Epsilon,
to: Comp::Done,
});
}
}
}
Ok(out)
}
fn intern_product(
a: &mut ir::Automaton,
ids: &mut HashMap<(Comp, Comp), ThreadStateId>,
order: &mut Vec<(Comp, Comp)>,
key: (Comp, Comp),
kind: ProductKind,
scope: &Symbol<'_>,
) -> Result<ThreadStateId, LoweringError> {
if let Some(&id) = ids.get(&key) {
return Ok(id);
}
if order.len() >= MAX_PRODUCT_STATES {
return Err(LoweringError::unsupported_at(
&format!(
"sva automaton builder: the `{}` of these operands needs more than \
{MAX_PRODUCT_STATES} product states (its operands' delay bounds are too large \
to compose in lockstep)",
kind.name()
),
scope,
));
}
let id = a.new_state();
ids.insert(key, id);
order.push(key);
Ok(id)
}
fn build_product<'d>(
a: &mut ir::Automaton,
l: Fragment,
r: Fragment,
kind: ProductKind,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let ne_l = !l.exits.is_empty();
let ne_r = !r.exits.is_empty();
let empty = l.empty && r.empty;
let mut routes: Vec<(Comp, Comp)> = Vec::new();
if ne_l && ne_r {
routes.push((Comp::Real(l.entry), Comp::Real(r.entry)));
}
if kind == ProductKind::And {
if l.empty && ne_r {
routes.push((Comp::Done, Comp::Real(r.entry)));
}
if r.empty && ne_l {
routes.push((Comp::Real(l.entry), Comp::Done));
}
}
let exits_l: HashSet<ThreadStateId> = l.exits.iter().copied().collect();
let exits_r: HashSet<ThreadStateId> = r.exits.iter().copied().collect();
let mut ids: HashMap<(Comp, Comp), ThreadStateId> = HashMap::new();
let mut order: Vec<(Comp, Comp)> = Vec::new();
let mut route_ids = Vec::new();
for &route in &routes {
route_ids.push(intern_product(a, &mut ids, &mut order, route, kind, scope)?);
}
let mut next = 0;
while next < order.len() {
let key @ (cl, cr) = order[next];
next += 1;
let from = ids[&key];
for m in comp_moves(a, cl, &exits_l, kind, scope)? {
let to = intern_product(a, &mut ids, &mut order, (m.to, cr), kind, scope)?;
a.add_edge(from, m.guard, m.label, to);
}
for m in comp_moves(a, cr, &exits_r, kind, scope)? {
let to = intern_product(a, &mut ids, &mut order, (cl, m.to), kind, scope)?;
a.add_edge(from, m.guard, m.label, to);
}
let waiting = |c: Comp| matches!(c, Comp::Wait { .. });
if let (Some(tl), Some(tr)) = (cl.tick(), cr.tick())
&& (waiting(cl) || waiting(cr))
{
let to = intern_product(a, &mut ids, &mut order, (tl, tr), kind, scope)?;
a.add_edge(
from,
None,
Transition::Delay {
min: 1,
max: Some(1),
},
to,
);
}
}
let is_exit = |&(cl, cr): &(Comp, Comp)| match (kind, cl, cr) {
(ProductKind::Intersect, Comp::Real(x), Comp::Real(y)) => {
exits_l.contains(&x) && exits_r.contains(&y)
}
(ProductKind::And, Comp::Done, Comp::Done) => true,
_ => false,
};
let live = trim_dead_product_states(a, &ids, &order, is_exit);
let live_routes: Vec<ThreadStateId> = route_ids
.iter()
.copied()
.filter(|id| live.contains(id))
.collect();
let entry = match live_routes.as_slice() {
[only] => *only,
many => {
let entry = a.new_state();
for &id in many {
a.add_edge(entry, None, Transition::Epsilon, id);
}
entry
}
};
let exits = order
.iter()
.filter(|key| is_exit(key))
.map(|key| ids[key])
.collect();
Ok(Fragment {
entry,
exits,
empty,
flow: Flow::identity(),
clock: None,
})
}
fn trim_dead_product_states(
a: &mut ir::Automaton,
ids: &HashMap<(Comp, Comp), ThreadStateId>,
order: &[(Comp, Comp)],
is_exit: impl Fn(&(Comp, Comp)) -> bool,
) -> HashSet<ThreadStateId> {
let index: HashMap<ThreadStateId, usize> = order
.iter()
.enumerate()
.map(|(i, key)| (ids[key], i))
.collect();
let mut preds: Vec<Vec<usize>> = vec![Vec::new(); order.len()];
let mut live = vec![false; order.len()];
let mut stack = Vec::new();
for (i, key) in order.iter().enumerate() {
let edges = &a.state(ids[key]).edges;
for e in edges {
preds[index[&e.target]].push(i);
}
let ends = edges
.iter()
.any(|e| matches!(e.label, Transition::FirstMatchEnd { .. }));
if ends || is_exit(key) {
live[i] = true;
stack.push(i);
}
}
while let Some(i) = stack.pop() {
for &p in &preds[i] {
if !live[p] {
live[p] = true;
stack.push(p);
}
}
}
for (i, key) in order.iter().enumerate() {
let id = ids[key];
if live[i] {
a.states[id.0 as usize].edges.retain(|e| {
live[index[&e.target]] || matches!(e.label, Transition::FirstMatchEnd { .. })
});
} else {
a.states[id.0 as usize].edges.clear();
}
}
order
.iter()
.enumerate()
.filter(|(i, _)| live[*i])
.map(|(_, key)| ids[key])
.collect()
}
fn true_fragment(a: &mut ir::Automaton) -> Fragment {
let entry = a.new_state();
let exit = a.new_state();
a.add_edge(entry, None, Transition::Epsilon, exit);
Fragment {
entry,
exits: vec![exit],
empty: false,
flow: Flow::identity(),
clock: None,
}
}
fn true_run(a: &mut ir::Automaton, leaves: &mut LeafTable<'_>) -> Result<Fragment, LoweringError> {
build_repeated(a, leaves, 0, None, CONSECUTIVE_LINK, &mut |a, _| {
Ok(true_fragment(a))
})
}
const CONSECUTIVE_LINK: SequenceRangeValue = SequenceRangeValue {
min: 1,
max: Some(1),
};
fn build_binary<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
expr: AssertionExpr<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let op = match Op::of(expr, scope)? {
Op::Binary(op) => op,
Op::Unary(op) => {
return Err(LoweringError::unsupported_at(
&format!("sva automaton builder: a Binary node carries the unary operator {op:?}"),
scope,
));
}
};
let kids = expr.children();
let [lhs, rhs] = kids.as_slice() else {
return Err(LoweringError::unsupported_at(
&format!(
"sva automaton builder: a `{op:?}` node must have exactly two operands, found {}",
kids.len()
),
scope,
));
};
match op {
AssertionBinaryOp::And | AssertionBinaryOp::Intersect => {
let kind = if op == AssertionBinaryOp::And {
ProductKind::And
} else {
ProductKind::Intersect
};
build_threads(
a,
leaves,
kind,
if op == AssertionBinaryOp::And {
"and"
} else {
"intersect"
},
scope,
&mut |a, leaves| build_node(a, leaves, *lhs, tree, scope),
&mut |a, leaves| build_node(a, leaves, *rhs, tree, scope),
)
}
AssertionBinaryOp::Or => {
let l = build_node(a, leaves, *lhs, tree, scope)?;
let r = build_node(a, leaves, *rhs, tree, scope)?;
let clock = join_clocks(leaves, &[&l, &r], "or", scope)?;
Ok(Fragment {
clock,
..build_or(a, l, r)
})
}
AssertionBinaryOp::Throughout => {
let cond = *lhs;
build_threads(
a,
leaves,
ProductKind::Intersect,
"throughout",
scope,
&mut |a, leaves| {
build_repeated(a, leaves, 0, None, CONSECUTIVE_LINK, &mut |a, leaves| {
build_node(a, leaves, cond, tree, scope)
})
},
&mut |a, leaves| build_node(a, leaves, *rhs, tree, scope),
)
}
AssertionBinaryOp::Within => build_threads(
a,
leaves,
ProductKind::Intersect,
"within",
scope,
&mut |a, leaves| {
let seq1 = build_node(a, leaves, *lhs, tree, scope)?;
let clock = single_clock(&seq1, "the inner sequence of `within`")
.map_err(|msg| LoweringError::unsupported_at(&msg, scope))?;
let one = CONSECUTIVE_LINK;
let before = true_run(a, leaves)?;
let after = true_run(a, leaves)?;
let inner = concat(a, before, one, seq1);
Ok(Fragment {
clock,
..concat(a, inner, one, after)
})
},
&mut |a, leaves| build_node(a, leaves, *rhs, tree, scope),
),
AssertionBinaryOp::Iff
| AssertionBinaryOp::Until
| AssertionBinaryOp::SUntil
| AssertionBinaryOp::UntilWith
| AssertionBinaryOp::SUntilWith
| AssertionBinaryOp::Implies
| AssertionBinaryOp::OverlappedImplication
| AssertionBinaryOp::NonOverlappedImplication
| AssertionBinaryOp::OverlappedFollowedBy
| AssertionBinaryOp::NonOverlappedFollowedBy => Err(LoweringError::unsupported_at(
&format!(
"sva automaton builder: AssertionExprKind::Binary operator {op:?} is a property \
operator (LRM 16.12), not a sequence operator: it is built by \
`build_property`, and cannot be an operand of a sequence operator, a delay or \
a repetition (16.12.1)"
),
scope,
)),
}
}
fn build_or(a: &mut ir::Automaton, l: Fragment, r: Fragment) -> Fragment {
let entry = a.new_state();
for f in [&l, &r] {
if !f.exits.is_empty() {
a.add_edge(entry, None, Transition::Epsilon, f.entry);
}
}
let flow = l.flow.or(&r.flow);
let mut exits = l.exits;
exits.extend(r.exits);
Fragment {
entry,
exits,
empty: l.empty || r.empty,
flow,
clock: None,
}
}
fn prefix_actions(
a: &mut ir::Automaton,
actions: Vec<Transition>,
target: ThreadStateId,
) -> ThreadStateId {
let Some((last, init)) = actions.split_last() else {
return target;
};
let entry = a.new_state();
let mut cur = entry;
for t in init {
let next = a.new_state();
a.add_edge(cur, None, t.clone(), next);
cur = next;
}
a.add_edge(cur, None, last.clone(), target);
entry
}
fn suffix_actions(
a: &mut ir::Automaton,
exits: Vec<ThreadStateId>,
actions: Vec<Transition>,
) -> Vec<ThreadStateId> {
if actions.is_empty() || exits.is_empty() {
return exits;
}
let head = a.new_state();
for &e in &exits {
a.add_edge(e, None, Transition::Epsilon, head);
}
let mut cur = head;
for t in actions {
let next = a.new_state();
a.add_edge(cur, None, t, next);
cur = next;
}
vec![cur]
}
fn build_threads<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
kind: ProductKind,
what: &str,
scope: &Symbol<'d>,
first: &mut dyn FnMut(
&mut ir::Automaton,
&mut LeafTable<'d>,
) -> Result<Fragment, LoweringError>,
second: &mut dyn FnMut(
&mut ir::Automaton,
&mut LeafTable<'d>,
) -> Result<Fragment, LoweringError>,
) -> Result<Fragment, LoweringError> {
let mark = leaves.touched.len();
let l = first(a, leaves)?;
let outer_touched: BTreeSet<LocalVarId> = leaves.touched[mark..].iter().copied().collect();
leaves.shadows.push(ShadowCtx {
outer_touched,
made: Vec::new(),
});
let r = second(a, leaves);
let ctx = leaves.shadows.pop().expect("pushed above");
let r = r?;
let clock = join_clocks(leaves, &[&l, &r], what, scope)?;
let flow = l.flow.intersect(&r.flow);
let copy_in: Vec<Transition> = ctx
.made
.iter()
.map(|&(_, outer, shadow)| Transition::LocalVarCopy {
dst: shadow,
src: outer,
})
.collect();
let copy_out: Vec<Transition> = ctx
.made
.iter()
.filter(|(canon, _, _)| r.flow.sample.contains(canon) && !l.flow.sample.contains(canon))
.map(|&(_, outer, shadow)| Transition::LocalVarCopy {
dst: outer,
src: shadow,
})
.collect();
let mut p = build_product(a, l, r, kind, scope)?;
p.entry = prefix_actions(a, copy_in, p.entry);
p.exits = suffix_actions(a, p.exits, copy_out);
p.flow = flow;
p.clock = clock;
Ok(p)
}
fn build_first_match<'d>(
a: &mut ir::Automaton,
leaves: &mut LeafTable<'d>,
expr: AssertionExpr<'d>,
tree: Trees<'_>,
scope: &Symbol<'d>,
) -> Result<Fragment, LoweringError> {
let kids = expr.children();
let Some((seq, items)) = kids.split_first() else {
return Err(LoweringError::unsupported_at(
"sva automaton builder: a first_match node has no sequence operand",
scope,
));
};
let x0 = leaves.flow_in.clone();
let r = build_node(a, leaves, *seq, tree, scope)?;
let clock = single_clock(&r, "`first_match`")
.map_err(|msg| LoweringError::unsupported_at(&msg, scope))?;
if r.empty && !items.is_empty() {
return Err(LoweringError::unsupported_at(
"a sequence match item is attached to a first_match of a sequence that admits an \
empty match (LRM 16.11: it shall be an error to attach a match item to such a \
sequence)",
scope,
));
}
if r.empty {
let mut f = empty_fragment(a);
f.flow = r.flow;
f.clock = clock;
return Ok(f);
}
let r = if items.is_empty() {
r
} else {
attach_match_items(a, leaves, r, items, &x0, scope)?
};
if r.exits.is_empty() {
return Ok(r);
}
let group = a.new_first_match_group();
let entry = a.new_state();
let exit = a.new_state();
a.add_edge(entry, None, Transition::FirstMatchBegin { group }, r.entry);
for &e in &r.exits {
a.add_edge(e, None, Transition::FirstMatchEnd { group }, exit);
}
Ok(Fragment {
entry,
exits: vec![exit],
empty: false,
flow: r.flow,
clock,
})
}
#[cfg(test)]
mod tests {
use super::*;
use std::collections::{BTreeMap, BTreeSet, HashSet};
use sv_lang::kinds::ExpressionKind;
use sv_lang::{AnalysisFlags, Compilation, Session, SyntaxTree};
use sv_sim_sim::sva::trace;
fn automaton_of<R>(
extra_decls: &str,
property_body: &str,
f: impl FnOnce(ir::Automaton, LeafTable<'_>) -> R,
) -> R {
let src = format!(
"module m;\n\
{extra_decls}\n\
logic clk, a, b, c;\n\
int cnt;\n\
always_ff @(posedge clk) begin\n\
assert property (@(posedge clk) {property_body});\n\
end\n\
endmodule\n"
);
let session = Session::new();
let mut comp = Compilation::new(&session).unwrap();
comp.add_source(&src).unwrap();
let design = comp.compile().unwrap();
assert!(
!design.has_fatal_errors(),
"fixture failed to compile: {src}"
);
let body = design
.top_instances()
.next()
.unwrap()
.instance_body()
.unwrap();
let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
let proc = analysis.procedures(body).next().unwrap();
let assertion = analysis.assertions(proc.symbol()).next().unwrap();
let tree = design.syntax_trees().into_iter().next().unwrap();
let clocking = assertion.root().as_assertion_expr().unwrap();
assert_eq!(clocking.kind(), AssertionExprKind::Clocking);
let root = clocking.children()[1].as_assertion_expr().unwrap();
let (automaton, leaves) =
build_automaton(root, Some(clocking.children()[0]), (&tree).into(), &body).unwrap();
f(automaton, leaves)
}
fn automaton_err(extra_decls: &str, property_body: &str) -> LoweringError {
let src = format!(
"module m;\n\
{extra_decls}\n\
logic clk, a, b, c;\n\
int cnt;\n\
always_ff @(posedge clk) begin\n\
assert property (@(posedge clk) {property_body});\n\
end\n\
endmodule\n"
);
let session = Session::new();
let mut comp = Compilation::new(&session).unwrap();
comp.add_source(&src).unwrap();
let design = comp.compile().unwrap();
assert!(
!design.has_fatal_errors(),
"fixture failed to compile: {src}"
);
let body = design
.top_instances()
.next()
.unwrap()
.instance_body()
.unwrap();
let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
let proc = analysis.procedures(body).next().unwrap();
let assertion = analysis.assertions(proc.symbol()).next().unwrap();
let tree = design.syntax_trees().into_iter().next().unwrap();
let clocking = assertion.root().as_assertion_expr().unwrap();
let root = clocking.children()[1].as_assertion_expr().unwrap();
build_automaton(root, Some(clocking.children()[0]), (&tree).into(), &body)
.expect_err("expected build_automaton to reject this")
}
fn reachable_lengths(automaton: &ir::Automaton, bound: u32) -> BTreeSet<u32> {
let mut out = BTreeSet::new();
let mut seen: HashSet<(u32, u32)> = HashSet::new();
let mut stack = vec![(automaton.start, 0u32)];
while let Some((state_id, ticks)) = stack.pop() {
if ticks > bound || !seen.insert((state_id.0, ticks)) {
continue;
}
let state = automaton.state(state_id);
if state.is_accepting() {
out.insert(ticks);
}
for edge in &state.edges {
match &edge.label {
ir::Transition::Delay { min, max } => {
let hi = max.unwrap_or(bound);
let mut k = *min;
while k <= hi {
let t = ticks + k;
if t > bound {
break;
}
stack.push((edge.target, t));
k += 1;
}
}
ir::Transition::Epsilon => stack.push((edge.target, ticks)),
ir::Transition::LocalVarWrite { .. }
| ir::Transition::LocalVarCopy { .. }
| ir::Transition::LocalVarStep { .. }
| ir::Transition::SubroutineCall { .. } => stack.push((edge.target, ticks)),
ir::Transition::EndPoint { .. } => {
panic!("a length walk cannot decide an EndPoint edge")
}
ir::Transition::ClockSync { .. } => {
panic!("a length walk cannot decide a ClockSync edge")
}
ir::Transition::Match { .. } => {
}
ir::Transition::Abort { .. }
| ir::Transition::FirstMatchBegin { .. }
| ir::Transition::FirstMatchEnd { .. } => {
}
}
}
}
out
}
#[test]
fn a_star_3_equiv_a_hash1_a_hash1_a() {
let lhs = automaton_of("", "a[*3]", |au, _| reachable_lengths(&au, 10));
let rhs = automaton_of("", "a ##1 a ##1 a", |au, _| reachable_lengths(&au, 10));
assert_eq!(lhs, rhs);
assert_eq!(lhs, BTreeSet::from([2]));
}
#[test]
fn parenthesized_concat_repeated_fixed_count() {
automaton_of("", "(a ##2 b)[*3]", |au, _| {
assert_eq!(reachable_lengths(&au, 20), BTreeSet::from([8]));
});
}
#[test]
fn parenthesized_concat_repeated_range_enumerates_five_lengths() {
automaton_of("", "(a ##2 b)[*1:5]", |au, _| {
assert_eq!(
reachable_lengths(&au, 20),
BTreeSet::from([2, 5, 8, 11, 14])
);
});
}
#[test]
fn simple_repeated_range_zero_to_three_then_concat_enumerates_four_lengths() {
automaton_of("", "a[*0:3] ##1 b ##1 c", |au, _| {
assert_eq!(reachable_lengths(&au, 20), BTreeSet::from([1, 2, 3, 4]));
});
}
#[test]
fn goto_repetition_on_sequence_with_match_item_is_rejected() {
let err = automaton_err("", "(b, cnt = cnt + 1)[->2]");
assert!(
err.message.contains("illegal"),
"error should name the illegal combination: {err}"
);
}
#[test]
fn nonconsecutive_repetition_on_sequence_with_match_item_is_rejected() {
let err = automaton_err("", "(b, cnt = cnt + 1)[=2]");
assert!(
err.message.contains("illegal"),
"error should name the illegal combination: {err}"
);
}
#[test]
fn consecutive_repetition_on_sequence_with_match_item_is_not_the_illegal_case() {
let err = automaton_err("", "(b, cnt = cnt + 1)[*2]");
assert!(
!err.message.contains("illegal"),
"consecutive repetition + match item is LRM-legal (lowered; see the probe fixture \
sva_match_item_assignments): only the module-variable target is refused: {err}"
);
assert!(err.message.contains("match item"), "error was: {err}");
}
#[test]
fn bare_leaf_has_single_tick_zero_length() {
automaton_of("", "a", |au, _| {
assert_eq!(reachable_lengths(&au, 5), BTreeSet::from([0]));
});
}
#[test]
fn consecutive_range_two_to_seven() {
automaton_of("", "a[*2:7]", |au, _| {
assert_eq!(
reachable_lengths(&au, 10),
BTreeSet::from([1, 2, 3, 4, 5, 6])
);
});
}
#[test]
fn goto_repetition_on_bare_leaf_allows_a_gap_between_matches() {
automaton_of("", "a[->2]", |au, _| {
let lengths = reachable_lengths(&au, 6);
assert!(lengths.contains(&1), "lengths were: {lengths:?}");
assert!(
lengths.iter().any(|&t| t >= 3),
"a true multi-tick gap must be reachable via goto repetition: {lengths:?}"
);
});
}
#[test]
fn goto_repetition_is_exact() {
let (a, na) = ("a", "!a");
assert_eq!(
lang_of("a[->1]", 2),
Lang::from([
word(&[&[a]]),
word(&[&[na], &[a]]),
word(&[&[na], &[na], &[a]]),
])
);
assert_eq!(
lang_of("a[->2]", 3),
Lang::from([
word(&[&[a], &[a]]),
word(&[&[a], &[na], &[a]]),
word(&[&[na], &[a], &[a]]),
word(&[&[a], &[na], &[na], &[a]]),
word(&[&[na], &[a], &[na], &[a]]),
word(&[&[na], &[na], &[a], &[a]]),
])
);
assert_eq!(lang_of("a[->0]", 3), Lang::from([Word::new()]));
for (goto, rewrite) in [
("a[->1]", "(!a[*0:$] ##1 a)[*1]"),
("a[->3]", "(!a[*0:$] ##1 a)[*3]"),
("a[->1:2]", "(!a[*0:$] ##1 a)[*1:2]"),
("a[->2:3]", "(!a[*0:$] ##1 a)[*2:3]"),
("a[->0:2]", "(!a[*0:$] ##1 a)[*0:2]"),
("a[->2:$]", "(!a[*0:$] ##1 a)[*2:$]"),
] {
assert_eq!(lang_of(goto, 5), lang_of(rewrite, 5), "`{goto}`");
}
}
#[test]
fn nonconsecutive_repetition_is_exact() {
let (a, na) = ("a", "!a");
assert_eq!(
lang_of("a[=1]", 2),
Lang::from([
word(&[&[a]]),
word(&[&[a], &[na]]),
word(&[&[na], &[a]]),
word(&[&[a], &[na], &[na]]),
word(&[&[na], &[a], &[na]]),
word(&[&[na], &[na], &[a]]),
])
);
assert_eq!(
lang_of("a[=2]", 2),
Lang::from([
word(&[&[a], &[a]]),
word(&[&[a], &[a], &[na]]),
word(&[&[a], &[na], &[a]]),
word(&[&[na], &[a], &[a]]),
])
);
for (nonconsecutive, rewrite) in [
("a[=1]", "a[->1] ##1 !a[*0:$]"),
("a[=2]", "a[->2] ##1 !a[*0:$]"),
("a[=1:2]", "a[->1:2] ##1 !a[*0:$]"),
("a[=2:$]", "a[->2:$] ##1 !a[*0:$]"),
] {
assert_eq!(
lang_of(nonconsecutive, 5),
lang_of(rewrite, 5),
"`{nonconsecutive}`"
);
}
assert_eq!(lang_of("a[=0]", 4), lang_of("!a[*0:$]", 4));
assert_ne!(lang_of("a[=2]", 4), lang_of("a[->2]", 4));
}
#[test]
fn goto_repetition_runs_on_traces() {
for (bits, want) in [
("1100", set(&[1])),
("0101", set(&[3])),
("1001", set(&[3])),
("1111", set(&[1])),
("0001", set(&[])),
("0000", set(&[])),
] {
let tr = Trace::new(&[("a", bits)]);
assert_eq!(ends_at("a[->2]", &tr, 0), want, "a[->2] on {bits}");
}
for (bits, want) in [
("1100", set(&[1, 2, 3])),
("0101", set(&[3])),
("1011", set(&[2])),
("1010", set(&[2, 3])),
("0001", set(&[])),
] {
let tr = Trace::new(&[("a", bits)]);
assert_eq!(ends_at("a[=2]", &tr, 0), want, "a[=2] on {bits}");
}
}
#[test]
fn goto_repetition_does_not_cross_an_x_tick() {
automaton_of("", "a[->1]", |_, leaves| {
let negated: Vec<bool> = (0..leaves.len() as u32)
.map(|i| leaves.is_negated(LeafId(i)))
.collect();
assert_eq!(negated.iter().filter(|n| !**n).count(), 1, "{negated:?}");
assert!(negated.iter().any(|n| *n), "{negated:?}");
});
for (bits, want) in [
("01x1", set(&[1])),
("0x01", set(&[])),
("x1", set(&[])),
("001x", set(&[2])),
("1xxx", set(&[0])),
("0011", set(&[2])),
] {
let tr = Trace::new(&[("a", bits)]);
assert_eq!(ends_at("a[->1]", &tr, 0), want, "a[->1] on {bits}");
assert_eq!(
ends_at("!a[*0:$] ##1 a", &tr, 0),
want,
"!a[*0:$] ##1 a on {bits}"
);
}
for (bits, want) in [
("10x0", set(&[0, 1])),
("1x", set(&[0])),
("0100", set(&[1, 2, 3])),
("01x0", set(&[1])),
] {
let tr = Trace::new(&[("a", bits)]);
let hand = "!a[*0:$] ##1 a ##1 !a[*0:$]";
assert_eq!(ends_at("a[=1]", &tr, 0), ends_at(hand, &tr, 0), "{bits}");
assert_eq!(ends_at("a[=1]", &tr, 0), want, "a[=1] on {bits}");
}
}
#[test]
fn unbounded_consecutive_repetition_is_a_true_cycle() {
automaton_of("", "a[*2:$]", |au, _| {
let lengths = reachable_lengths(&au, 8);
assert_eq!(lengths, BTreeSet::from([1, 2, 3, 4, 5, 6, 7, 8]));
});
}
#[test]
fn unsupported_assertion_expr_kind_is_a_named_error() {
let err = automaton_err("", "a |-> b");
assert!(err.message.contains("Binary"), "error was: {err}");
assert!(
err.message.contains("OverlappedImplication"),
"error should name the operator: {err}"
);
}
type Letter = BTreeSet<String>;
type Word = Vec<Letter>;
type Lang = BTreeSet<Word>;
fn word(letters: &[&[&str]]) -> Word {
letters
.iter()
.map(|l| l.iter().map(|s| s.to_string()).collect())
.collect()
}
fn norm_leaf(text: &str) -> String {
let mut s: String = text.chars().filter(|c| !c.is_whitespace()).collect();
loop {
let b = s.as_bytes();
if b.first() != Some(&b'(') || b.last() != Some(&b')') {
return s;
}
let mut depth = 0i32;
let mut closes_at_end = false;
for (i, &c) in b.iter().enumerate() {
match c {
b'(' => depth += 1,
b')' => {
depth -= 1;
if depth == 0 {
closes_at_end = i == b.len() - 1;
break;
}
}
_ => {}
}
}
if !closes_at_end {
return s;
}
s = s[1..s.len() - 1].to_string();
}
}
fn leaf_texts(leaves: &LeafTable<'_>, tree: &SyntaxTree) -> Vec<String> {
(0..leaves.len() as u32)
.map(|i| {
let e = leaves.get(LeafId(i));
let text = if e.kind() == ExpressionKind::NamedValue
&& let Some(sym) = e.referenced_symbol()
{
sym.name().to_string()
} else {
match e.syntax(tree) {
Some(node) => norm_leaf(&node.text()),
None => format!("<{:?}>", e.kind()),
}
};
if leaves.is_negated(LeafId(i)) {
assert!(
text.chars().all(|c| c.is_alphanumeric() || c == '_'),
"a negated leaf over `{text}` has no source-text spelling here"
);
return format!("!{text}");
}
text
})
.collect()
}
fn accepted_lang(
au: &ir::Automaton,
leaves: &LeafTable<'_>,
tree: &SyntaxTree,
bound: u32,
) -> Lang {
let mut out = Lang::new();
if au.admits_empty {
out.insert(Vec::new());
}
let mut steps = 0u64;
type Walk = (ThreadStateId, u32, Vec<(u32, String)>);
let texts = leaf_texts(leaves, tree);
type Seen = (u32, u32, Vec<(u32, String)>);
let mut seen: HashSet<Seen> = HashSet::new();
let mut stack: Vec<Walk> = vec![(au.start, 0, Vec::new())];
while let Some((state_id, ticks, cons)) = stack.pop() {
let mut key = cons.clone();
key.sort();
key.dedup();
if !seen.insert((state_id.0, ticks, key)) {
continue;
}
steps += 1;
assert!(steps < 5_000_000, "automaton walk did not terminate");
let state = au.state(state_id);
if state.is_accepting() {
let mut w: Word = vec![Letter::new(); ticks as usize + 1];
for (t, name) in &cons {
w[*t as usize].insert(name.clone());
}
out.insert(w);
}
for edge in &state.edges {
let mut cons2 = cons.clone();
if let Some(g) = edge.guard {
let text = &texts[g.0 as usize];
if text != "1" {
cons2.push((ticks, text.clone()));
}
}
match &edge.label {
ir::Transition::Epsilon => stack.push((edge.target, ticks, cons2)),
ir::Transition::Delay { min, max } => {
let hi = max.unwrap_or(bound).min(bound);
for k in *min..=hi {
if ticks + k <= bound {
stack.push((edge.target, ticks + k, cons2.clone()));
}
}
}
ir::Transition::Match { .. } => {}
ir::Transition::LocalVarWrite { .. }
| ir::Transition::LocalVarCopy { .. }
| ir::Transition::LocalVarStep { .. }
| ir::Transition::SubroutineCall { .. } => {
stack.push((edge.target, ticks, cons2))
}
ir::Transition::Abort { .. } => {
panic!("T10 builds no Abort edges")
}
ir::Transition::EndPoint { .. } => {
panic!("a word-language walk cannot decide an EndPoint edge")
}
ir::Transition::ClockSync { .. } => {
panic!("a word-language walk cannot decide a ClockSync edge")
}
ir::Transition::FirstMatchBegin { .. }
| ir::Transition::FirstMatchEnd { .. } => {
panic!("accepted_lang cannot interpret first_match markers")
}
}
}
}
out
}
fn try_lang_of(body: &str, bound: u32) -> Option<Lang> {
with_built(body, |au, leaves, tree| {
accepted_lang(au, leaves, tree, bound)
})
}
fn with_built<R>(
body: &str,
f: impl FnOnce(&ir::Automaton, &LeafTable<'_>, &SyntaxTree) -> R,
) -> Option<R> {
with_built_in("", body, f)
}
fn with_built_in<R>(
extra_decls: &str,
body: &str,
f: impl FnOnce(&ir::Automaton, &LeafTable<'_>, &SyntaxTree) -> R,
) -> Option<R> {
let src = format!(
"module m;\n\
{extra_decls}\n\
logic clk, a, b, c, d, e;\n\
always_ff @(posedge clk) begin\n\
assert property (@(posedge clk) {body} |-> 1);\n\
end\n\
endmodule\n"
);
let session = Session::new();
let mut comp = Compilation::new(&session).unwrap();
comp.add_source(&src).unwrap();
let design = comp.compile().unwrap();
if design.has_fatal_errors() {
return None;
}
let m = design
.top_instances()
.next()
.unwrap()
.instance_body()
.unwrap();
let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
let proc = analysis.procedures(m).next().unwrap();
let assertion = analysis.assertions(proc.symbol()).next().unwrap();
let tree = design.syntax_trees().into_iter().next().unwrap();
let clocking = assertion.root().as_assertion_expr().unwrap();
let implication = clocking.children()[1].as_assertion_expr().unwrap();
assert_eq!(implication.kind(), AssertionExprKind::Binary);
let root = implication.children()[0].as_assertion_expr().unwrap();
let (au, leaves) = build_automaton(root, Some(clocking.children()[0]), (&tree).into(), &m)
.unwrap_or_else(|e| panic!("build_automaton failed for `{body}`: {e}"));
Some(f(&au, &leaves, &tree))
}
fn lang_of(body: &str, bound: u32) -> Lang {
try_lang_of(body, bound).unwrap_or_else(|| panic!("`{body}` failed to compile"))
}
#[test]
fn lrm_empty_hash0_b_never_matches_but_true_hash0_b_matches_whenever_b() {
assert_eq!(lang_of("a[*0] ##0 b", 8), Lang::new());
assert_eq!(lang_of("1 ##0 b", 8), Lang::from([word(&[&["b"]])]));
}
#[test]
fn seq_hash0_empty_never_matches() {
assert_eq!(lang_of("b ##0 a[*0]", 8), Lang::new());
}
#[test]
fn empty_hash_n_seq_is_delay_n_minus_1_seq() {
assert_eq!(lang_of("a[*0] ##1 b", 8), Lang::from([word(&[&["b"]])]));
assert_eq!(lang_of("a[*0] ##1 b", 8), lang_of("##0 b", 8));
assert_eq!(
lang_of("a[*0] ##2 b", 8),
Lang::from([word(&[&[], &["b"]])])
);
assert_eq!(lang_of("a[*0] ##2 b", 8), lang_of("##1 b", 8));
assert_eq!(
lang_of("a[*0] ##4 (b ##1 c)", 12),
lang_of("##3 (b ##1 c)", 12)
);
}
#[test]
fn seq_hash_n_empty_is_seq_delay_n_minus_1_true() {
assert_eq!(lang_of("b ##1 a[*0]", 8), Lang::from([word(&[&["b"]])]));
assert_eq!(
lang_of("b ##2 a[*0]", 8),
Lang::from([word(&[&["b"], &[]])])
);
assert_eq!(lang_of("b ##2 a[*0]", 8), lang_of("b ##1 1", 8));
assert_eq!(lang_of("b ##3 a[*0]", 8), lang_of("b ##2 1", 8));
}
#[test]
fn lrm_multiple_concatenation_example_matches_its_stated_simplification() {
let got = lang_of("b ##1 a[*0:1] ##2 c", 10);
let want_b2c = lang_of("b ##2 c", 10);
let want_b1a2c = lang_of("b ##1 a ##2 c", 10);
assert_eq!(want_b2c, Lang::from([word(&[&["b"], &[], &["c"]])]));
assert_eq!(
want_b1a2c,
Lang::from([word(&[&["b"], &["a"], &[], &["c"]])])
);
let expected: Lang = want_b2c.union(&want_b1a2c).cloned().collect();
assert_eq!(got, expected);
assert_eq!(got.len(), 2);
}
#[test]
fn empty_hash_n_empty() {
let none = try_lang_of("a[*0] ##0 b[*0]", 8).unwrap();
assert_eq!(none, Lang::new());
let one = lang_of("a[*0] ##1 b[*0]", 8);
assert_eq!(one, Lang::from([Vec::new()]), "empty ##1 empty = empty");
let three = lang_of("a[*0] ##3 b[*0]", 8);
assert_eq!(three, Lang::from([word(&[&[], &[]])]), "two vacuous ticks");
}
#[test]
fn both_operands_admit_empty_and_nonempty() {
assert_eq!(
lang_of("a[*0:1] ##0 b[*0:1]", 8),
Lang::from([word(&[&["a", "b"]])]),
"##0 needs both operands nonempty (rules 1-2), fusing a and b into one tick"
);
assert_eq!(
lang_of("a[*0:1] ##1 b[*0:1]", 8),
Lang::from([
Vec::new(), word(&[&["b"]]), word(&[&["a"]]), word(&[&["a"], &["b"]]), ])
);
assert_eq!(
lang_of("a[*0:1] ##2 b[*0:1]", 8),
Lang::from([
word(&[&[]]), word(&[&[], &["b"]]), word(&[&["a"], &[]]), word(&[&["a"], &[], &["b"]]), ])
);
}
#[test]
fn repetition_of_a_unit_that_admits_empty() {
assert_eq!(
lang_of("(a[*0:1])[*2]", 8),
Lang::from([Vec::new(), word(&[&["a"]]), word(&[&["a"], &["a"]])])
);
}
#[test]
fn leading_cycle_delay() {
assert_eq!(lang_of("##2 b", 8), Lang::from([word(&[&[], &[], &["b"]])]));
assert_eq!(lang_of("##0 b", 8), Lang::from([word(&[&["b"]])]));
assert_eq!(
lang_of("##[1:3] a ##1 b", 8),
Lang::from([
word(&[&[], &["a"], &["b"]]),
word(&[&[], &[], &["a"], &["b"]]),
word(&[&[], &[], &[], &["a"], &["b"]]),
])
);
}
#[test]
fn ranged_delay_includes_zero_as_fusion() {
assert_eq!(
lang_of("a ##[0:2] b", 8),
Lang::from([
word(&[&["a", "b"]]),
word(&[&["a"], &["b"]]),
word(&[&["a"], &[], &["b"]]),
])
);
}
#[test]
fn star_and_plus_delay_are_zero_and_one_to_dollar() {
assert_eq!(lang_of("a ##[*] b", 6), lang_of("a ##[0:$] b", 6));
assert_eq!(lang_of("a ##[+] b", 6), lang_of("a ##[1:$] b", 6));
assert_eq!(lang_of("##[*] b", 6), lang_of("##[0:$] b", 6));
assert_eq!(lang_of("##[+] b", 6), lang_of("##[1:$] b", 6));
assert!(lang_of("a ##[*] b", 6).contains(&word(&[&["a", "b"]])));
assert!(!lang_of("a ##[+] b", 6).contains(&word(&[&["a", "b"]])));
assert_eq!(lang_of("a ##[+] b", 6).len(), 6);
assert_eq!(lang_of("a ##[*] b", 6).len(), 7);
}
#[test]
fn fused_chain() {
assert_eq!(
lang_of("a ##0 b ##0 c", 4),
Lang::from([word(&[&["a", "b", "c"]])])
);
}
#[test]
fn parenthesized_concat_operands() {
let want = Lang::from([word(&[&["a"], &["b"], &[], &["c"]])]);
assert_eq!(lang_of("(a ##1 b) ##2 c", 8), want);
assert_eq!(lang_of("((a ##1 b)) ##2 c", 8), want);
assert_eq!(lang_of("a ##1 (b ##2 c)", 8), lang_of("a ##1 b ##2 c", 8));
assert_eq!(lang_of("(a ##1 b)", 8), lang_of("a ##1 b", 8));
assert_eq!(
lang_of("a ##1 (b[*0:1]) ##1 c", 8),
lang_of("a ##1 b[*0:1] ##1 c", 8)
);
assert_eq!(
lang_of("a ##1 ((b ##1 c)[*0:1]) ##1 a", 8),
lang_of("a ##1 (b ##1 c)[*0:1] ##1 a", 8)
);
}
#[test]
fn reversed_delay_range_is_a_named_error_or_a_slang_error() {
let src = "module m;\nlogic clk, a, b;\nalways_ff @(posedge clk) begin\n \
assert property (@(posedge clk) a ##[3:1] b);\nend\nendmodule\n";
let session = Session::new();
let mut comp = Compilation::new(&session).unwrap();
comp.add_source(src).unwrap();
let design = comp.compile().unwrap();
if design.has_fatal_errors() {
return; }
let err = automaton_err("", "a ##[3:1] b");
assert!(err.message.contains("min"), "error was: {err}");
}
#[derive(Clone, Debug)]
enum Rx {
Leaf(&'static str),
Cat(Box<Rx>, Dl, Box<Rx>),
Lead(Dl, Box<Rx>),
Rep(Box<Rx>, Rp),
Paren(Box<Rx>),
Bin(Box<Rx>, SeqOp, Box<Rx>),
Thr(&'static str, Box<Rx>),
First(Box<Rx>),
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
enum SeqOp {
And,
Or,
Intersect,
Within,
}
impl SeqOp {
fn text(self) -> &'static str {
match self {
SeqOp::And => "and",
SeqOp::Or => "or",
SeqOp::Intersect => "intersect",
SeqOp::Within => "within",
}
}
}
#[derive(Clone, Copy, Debug)]
struct Dl {
min: u32,
max: Option<u32>,
text: &'static str,
}
#[derive(Clone, Copy, Debug)]
struct Rp {
min: u32,
max: Option<u32>,
text: &'static str,
}
const DELAYS: &[Dl] = &[
Dl {
min: 0,
max: Some(0),
text: "##0",
},
Dl {
min: 1,
max: Some(1),
text: "##1",
},
Dl {
min: 2,
max: Some(2),
text: "##2",
},
Dl {
min: 3,
max: Some(3),
text: "##3",
},
Dl {
min: 0,
max: Some(2),
text: "##[0:2]",
},
Dl {
min: 1,
max: Some(3),
text: "##[1:3]",
},
Dl {
min: 2,
max: None,
text: "##[2:$]",
},
Dl {
min: 0,
max: None,
text: "##[*]",
},
Dl {
min: 1,
max: None,
text: "##[+]",
},
];
const REPS: &[Rp] = &[
Rp {
min: 0,
max: Some(0),
text: "[*0]",
},
Rp {
min: 1,
max: Some(1),
text: "[*1]",
},
Rp {
min: 2,
max: Some(2),
text: "[*2]",
},
Rp {
min: 0,
max: Some(1),
text: "[*0:1]",
},
Rp {
min: 0,
max: Some(2),
text: "[*0:2]",
},
Rp {
min: 1,
max: Some(3),
text: "[*1:3]",
},
Rp {
min: 0,
max: None,
text: "[*]",
},
Rp {
min: 1,
max: None,
text: "[+]",
},
Rp {
min: 2,
max: None,
text: "[*2:$]",
},
];
fn render(rx: &Rx) -> String {
match rx {
Rx::Leaf(n) => n.to_string(),
Rx::Paren(r) => format!("({})", render(r)),
Rx::Lead(d, r) => format!("{} {}", d.text, render_operand(r)),
Rx::Cat(l, d, r) => format!("{} {} {}", render_left(l), d.text, render_operand(r)),
Rx::Rep(r, p) => match **r {
Rx::Leaf(_) => format!("{}{}", render(r), p.text),
_ => format!("({}){}", render(r), p.text),
},
Rx::Bin(l, op, r) => format!("(({}) {} ({}))", render(l), op.text(), render(r)),
Rx::Thr(c, r) => format!("(({c}) throughout ({}))", render(r)),
Rx::First(r) => format!("first_match({})", render(r)),
}
}
fn render_left(rx: &Rx) -> String {
render(rx)
}
fn render_operand(rx: &Rx) -> String {
match rx {
Rx::Cat(..) | Rx::Lead(..) => format!("({})", render(rx)),
_ => render(rx),
}
}
fn cat_words(l1: &Lang, d: Dl, l2: &Lang, cap: usize) -> Lang {
let mut out = Lang::new();
let hi = d.max.unwrap_or(cap as u32 + 1).min(cap as u32 + 1);
for x in l1 {
for y in l2 {
for k in d.min..=hi {
let w: Word = if k == 0 {
if x.is_empty() || y.is_empty() {
continue;
}
let mut w = x[..x.len() - 1].to_vec();
let fused: Letter = x[x.len() - 1].union(&y[0]).cloned().collect();
w.push(fused);
w.extend_from_slice(&y[1..]);
w
} else {
let mut w = x.clone();
w.extend(std::iter::repeat_n(Letter::new(), (k - 1) as usize));
w.extend_from_slice(y);
w
};
if w.len() <= cap {
out.insert(w);
}
}
}
}
out
}
fn lang_ref(rx: &Rx, cap: usize) -> Lang {
match rx {
Rx::Leaf("1") => Lang::from([vec![Letter::new()]]),
Rx::Leaf(n) => Lang::from([vec![Letter::from([n.to_string()])]]),
Rx::Paren(r) => lang_ref(r, cap),
Rx::Cat(l, d, r) => cat_words(&lang_ref(l, cap), *d, &lang_ref(r, cap), cap),
Rx::Lead(d, r) => {
let r = lang_ref(r, cap);
let mut out = Lang::new();
let hi = d.max.unwrap_or(cap as u32).min(cap as u32);
for k in d.min..=hi {
for y in &r {
let mut w: Word = vec![Letter::new(); k as usize];
w.extend_from_slice(y);
if w.len() <= cap {
out.insert(w);
}
}
}
out
}
Rx::Rep(r, p) => {
let unit = lang_ref(r, cap);
let one = Dl {
min: 1,
max: Some(1),
text: "##1",
};
let mut pow = Lang::from([Vec::new()]);
let mut out = Lang::new();
let top = p.max.unwrap_or(cap as u32 + 1).min(cap as u32 + 1);
if p.min == 0 {
out.extend(pow.iter().cloned());
}
for k in 1..=top {
pow = cat_words(&pow, one, &unit, cap);
if k >= p.min {
out.extend(pow.iter().cloned());
}
}
out
}
Rx::Bin(l, op, r) => {
let (l, r) = (lang_ref(l, cap), lang_ref(r, cap));
let one = Dl {
min: 1,
max: Some(1),
text: "##1",
};
match op {
SeqOp::Or => l.union(&r).cloned().collect(),
SeqOp::Intersect => intersect_words(&l, &r),
SeqOp::And => {
let pad = true_run_words(cap);
let first = intersect_words(&cat_words(&l, one, &pad, cap), &r);
let second = intersect_words(&l, &cat_words(&r, one, &pad, cap));
first.union(&second).cloned().collect()
}
SeqOp::Within => {
let pad = true_run_words(cap);
let wrapped = cat_words(&cat_words(&pad, one, &l, cap), one, &pad, cap);
intersect_words(&wrapped, &r)
}
}
}
Rx::Thr(c, r) => {
let run: Lang = (0..=cap)
.map(|k| vec![Letter::from([c.to_string()]); k])
.collect();
intersect_words(&run, &lang_ref(r, cap))
}
Rx::First(_) => panic!(
"first_match is a filter over match END TICKS of an attempt, which a word \
language cannot express; it is checked against concrete traces"
),
}
}
fn true_run_words(cap: usize) -> Lang {
(0..=cap).map(|k| vec![Letter::new(); k]).collect()
}
fn intersect_words(l: &Lang, r: &Lang) -> Lang {
let mut out = Lang::new();
for x in l {
for y in r {
if x.len() == y.len() {
out.insert(
x.iter()
.zip(y)
.map(|(p, q)| p.union(q).cloned().collect())
.collect(),
);
}
}
}
out
}
struct Lcg(u64);
impl Lcg {
fn next(&mut self, n: usize) -> usize {
self.0 = self
.0
.wrapping_mul(6364136223846793005)
.wrapping_add(1442695040888963407);
((self.0 >> 33) as usize) % n
}
}
fn gen_rx(g: &mut Lcg, depth: u32) -> Rx {
const LEAVES: &[&str] = &["a", "b", "c", "1"];
let leaf = |g: &mut Lcg| Rx::Leaf(LEAVES[g.next(LEAVES.len())]);
if depth == 0 {
return leaf(g);
}
match g.next(10) {
0..=1 => leaf(g),
2..=5 => {
let mut acc = gen_rx(g, depth - 1);
for _ in 0..(1 + g.next(2)) {
let d = DELAYS[g.next(DELAYS.len())];
let rhs = gen_rx(g, depth - 1);
acc = Rx::Cat(Box::new(acc), d, Box::new(rhs));
}
acc
}
6 => Rx::Lead(DELAYS[g.next(DELAYS.len())], Box::new(gen_rx(g, depth - 1))),
7..=8 => Rx::Rep(Box::new(gen_rx(g, depth - 1)), REPS[g.next(REPS.len())]),
_ => Rx::Paren(Box::new(gen_rx(g, depth - 1))),
}
}
fn concats_with_empty_operand(rx: &Rx, cap: usize) -> usize {
let admits_empty = |r: &Rx| lang_ref(r, cap).contains(&Vec::new());
match rx {
Rx::Leaf(_) => 0,
Rx::Paren(r) | Rx::Rep(r, _) | Rx::Thr(_, r) | Rx::First(r) => {
concats_with_empty_operand(r, cap)
}
Rx::Lead(_, r) => concats_with_empty_operand(r, cap),
Rx::Bin(l, _, r) => {
concats_with_empty_operand(l, cap) + concats_with_empty_operand(r, cap)
}
Rx::Cat(l, _, r) => {
usize::from(admits_empty(l) || admits_empty(r))
+ concats_with_empty_operand(l, cap)
+ concats_with_empty_operand(r, cap)
}
}
}
#[test]
fn generated_sequences_match_the_annex_f_reference() {
const BOUND: u32 = 6;
let mut g = Lcg(0x5eed_5eed_5eed_5eed);
let (mut compared, mut skipped, mut with_empty, mut empty_sites) = (0usize, 0, 0, 0);
for _ in 0..1000 {
let rx = gen_rx(&mut g, 3);
let src = render(&rx);
let want = lang_ref(&rx, BOUND as usize + 1);
match try_lang_of(&src, BOUND) {
None => skipped += 1,
Some(got) => {
assert_eq!(got, want, "automaton vs Annex F reference for `{src}`");
compared += 1;
with_empty += usize::from(want.contains(&Vec::new()));
empty_sites += concats_with_empty_operand(&rx, BOUND as usize + 1);
}
}
}
assert!(
compared >= 700,
"only {compared} compared, {skipped} skipped"
);
assert!(
with_empty >= 40,
"only {with_empty} sequences admit an empty match"
);
assert!(
empty_sites >= 150,
"only {empty_sites} concatenations had an empty-admitting operand"
);
}
#[test]
fn or_is_the_union_of_the_operands_matches() {
assert_eq!(
lang_of("(a or b)", 8),
Lang::from([word(&[&["a"]]), word(&[&["b"]])])
);
assert_eq!(
lang_of("((a ##1 b) or (c ##2 a))", 8),
Lang::from([word(&[&["a"], &["b"]]), word(&[&["c"], &[], &["a"]])])
);
assert_eq!(
lang_of("(a[*0] or b)", 8),
Lang::from([Vec::new(), word(&[&["b"]])])
);
assert_eq!(lang_of("(a or a)", 8), lang_of("a", 8));
assert_eq!(
lang_of("(a or b) ##1 c", 8),
Lang::from([word(&[&["a"], &["c"]]), word(&[&["b"], &["c"]])])
);
assert_eq!(
lang_of("c ##1 (a or (b ##1 b))", 8),
Lang::from([word(&[&["c"], &["a"]]), word(&[&["c"], &["b"], &["b"]])])
);
}
#[test]
fn intersect_pairs_matches_of_the_same_length() {
assert_eq!(
lang_of("((a ##[1:3] b) intersect (c ##2 d))", 8),
Lang::from([word(&[&["a", "c"], &[], &["b", "d"]])])
);
assert_eq!(
lang_of("(a[*1:3] intersect b[*2])", 8),
Lang::from([word(&[&["a", "b"], &["a", "b"]])])
);
assert_eq!(lang_of("(a[*2] intersect b[*3])", 8), Lang::new());
assert_eq!(lang_of("(a intersect (b ##1 c))", 8), Lang::new());
assert_eq!(
lang_of("(a[*] intersect b[*2:3])", 8),
Lang::from([
word(&[&["a", "b"], &["a", "b"]]),
word(&[&["a", "b"], &["a", "b"], &["a", "b"]])
])
);
assert_eq!(
lang_of("((a ##1 b) intersect (a ##1 b))", 8),
lang_of("a ##1 b", 8)
);
}
#[test]
fn intersect_of_empty_matches() {
assert_eq!(
lang_of("(a[*0] intersect b[*0])", 8),
Lang::from([Vec::new()])
);
assert_eq!(lang_of("(a[*0] intersect b)", 8), Lang::new());
assert_eq!(lang_of("(a[*0:2] intersect b[*0:1])", 8), {
Lang::from([Vec::new(), word(&[&["a", "b"]])])
});
}
#[test]
fn and_ends_where_the_later_operand_ends() {
assert_eq!(lang_of("(a and b)", 8), Lang::from([word(&[&["a", "b"]])]));
assert_eq!(
lang_of("((a ##1 b) and (c ##2 d))", 8),
Lang::from([word(&[&["a", "c"], &["b"], &["d"]])])
);
assert_eq!(
lang_of("((c ##2 d) and (a ##1 b))", 8),
Lang::from([word(&[&["a", "c"], &["b"], &["d"]])])
);
assert_eq!(
lang_of("(a and (b ##[1:2] c))", 8),
Lang::from([
word(&[&["a", "b"], &["c"]]),
word(&[&["a", "b"], &[], &["c"]])
])
);
}
#[test]
fn and_with_an_empty_operand() {
assert_eq!(lang_of("(a[*0] and b)", 8), Lang::from([word(&[&["b"]])]));
assert_eq!(
lang_of("(a[*0] and (b ##1 c))", 8),
Lang::from([word(&[&["b"], &["c"]])])
);
assert_eq!(lang_of("(a[*0] and b[*0])", 8), Lang::from([Vec::new()]));
assert_eq!(
lang_of("(a[*0:1] and b[*0:1])", 8),
Lang::from([
Vec::new(),
word(&[&["a"]]),
word(&[&["b"]]),
word(&[&["a", "b"]])
])
);
}
#[test]
fn and_equals_its_annex_f_rewrite() {
let operands = [
"a",
"a ##2 b",
"a ##[1:3] b",
"a[*0:2]",
"(a ##1 b)[*1:2]",
"a[*0] ##[0:2] b",
"a ##[2:$] b",
];
for r1 in operands {
for r2 in ["c", "c ##1 d", "c[*0:1]", "(c ##2 d)[*1:2]", "c ##[1:3] d"] {
let and = lang_of(&format!("(({r1}) and ({r2}))"), 7);
let rewrite = lang_of(
&format!(
"((({r1}) ##1 1[*0:$]) intersect ({r2})) or \
(({r1}) intersect (({r2}) ##1 1[*0:$]))"
),
7,
);
assert_eq!(and, rewrite, "`({r1}) and ({r2})`");
}
}
}
#[test]
fn throughout_holds_the_condition_on_every_tick() {
assert_eq!(
lang_of("(a throughout (b ##2 c))", 8),
Lang::from([word(&[&["a", "b"], &["a"], &["a", "c"]])])
);
assert_eq!(
lang_of("(a throughout b[*0:2])", 8),
Lang::from([
Vec::new(),
word(&[&["a", "b"]]),
word(&[&["a", "b"], &["a", "b"]])
])
);
assert_eq!(lang_of("(a throughout b[*0])", 8), Lang::from([Vec::new()]));
assert_eq!(
lang_of("a throughout b ##1 c", 8),
lang_of("(a throughout (b ##1 c))", 8)
);
}
#[test]
fn throughout_equals_its_rewrite() {
for s in [
"b",
"b ##2 c",
"b[*0:2]",
"(b ##1 c)[*1:3]",
"b ##[1:3] c",
"b ##[2:$] c",
] {
assert_eq!(
lang_of(&format!("(a throughout ({s}))"), 8),
lang_of(&format!("(a[*0:$] intersect ({s}))"), 8),
"`a throughout ({s})`"
);
}
}
#[test]
fn within_places_the_left_operand_inside_the_right() {
assert_eq!(
lang_of("(a within (b ##3 c))", 8),
Lang::from([
word(&[&["a", "b"], &[], &[], &["c"]]),
word(&[&["b"], &["a"], &[], &["c"]]),
word(&[&["b"], &[], &["a"], &["c"]]),
word(&[&["b"], &[], &[], &["a", "c"]]),
])
);
assert_eq!(lang_of("((b ##3 c) within a)", 8), Lang::new());
assert_eq!(
lang_of("((a ##1 b) within (c ##1 d))", 8),
Lang::from([word(&[&["a", "c"], &["b", "d"]])])
);
assert_eq!(
lang_of("(a[*0] within b[*0:1])", 8),
Lang::from([Vec::new(), word(&[&["b"]])])
);
}
#[test]
fn within_equals_its_rewrite() {
for s1 in ["a", "a ##1 b", "a[*0:2]", "a ##[1:2] b"] {
for s2 in ["c", "c ##3 d", "c[*0:3]", "c ##[1:4] d", "(c ##1 d)[*1:3]"] {
assert_eq!(
lang_of(&format!("(({s1}) within ({s2}))"), 7),
lang_of(
&format!("((1[*0:$] ##1 ({s1}) ##1 1[*0:$]) intersect ({s2}))"),
7
),
"`({s1}) within ({s2})`"
);
}
}
}
fn gen_rx11(g: &mut Lcg, depth: u32, first: bool) -> Rx {
const LEAVES: &[&str] = &["a", "b", "c", "1"];
const CONDS: &[&str] = &["a", "b", "c"];
const OPS: &[SeqOp] = &[SeqOp::And, SeqOp::Or, SeqOp::Intersect, SeqOp::Within];
let leaf = |g: &mut Lcg| Rx::Leaf(LEAVES[g.next(LEAVES.len())]);
if depth == 0 {
return leaf(g);
}
match g.next(14) {
0..=1 => leaf(g),
2..=3 => {
let mut acc = gen_rx11(g, depth - 1, first);
for _ in 0..(1 + g.next(2)) {
let d = DELAYS[g.next(DELAYS.len())];
let rhs = gen_rx11(g, depth - 1, first);
acc = Rx::Cat(Box::new(acc), d, Box::new(rhs));
}
acc
}
4 => Rx::Lead(
DELAYS[g.next(DELAYS.len())],
Box::new(gen_rx11(g, depth - 1, first)),
),
5 => {
let zero: Vec<Rp> = REPS.iter().copied().filter(|r| r.min == 0).collect();
let rep = if g.next(2) == 0 {
zero[g.next(zero.len())]
} else {
REPS[g.next(REPS.len())]
};
Rx::Rep(Box::new(gen_rx11(g, depth - 1, first)), rep)
}
6 => Rx::Paren(Box::new(gen_rx11(g, depth - 1, first))),
7..=10 => Rx::Bin(
Box::new(gen_rx11(g, depth - 1, first)),
OPS[g.next(OPS.len())],
Box::new(gen_rx11(g, depth - 1, first)),
),
11 => Rx::Thr(
CONDS[g.next(CONDS.len())],
Box::new(gen_rx11(g, depth - 1, first)),
),
_ if first => Rx::First(Box::new(gen_rx11(g, depth - 1, first))),
_ => Rx::Bin(
Box::new(gen_rx11(g, depth - 1, first)),
OPS[g.next(OPS.len())],
Box::new(gen_rx11(g, depth - 1, first)),
),
}
}
fn op_census(rx: &Rx, c: &mut [usize; 6]) {
match rx {
Rx::Leaf(_) => {}
Rx::Paren(r) | Rx::Rep(r, _) | Rx::Lead(_, r) => op_census(r, c),
Rx::Cat(l, _, r) => {
op_census(l, c);
op_census(r, c);
}
Rx::Bin(l, op, r) => {
c[match op {
SeqOp::And => 0,
SeqOp::Or => 1,
SeqOp::Intersect => 2,
SeqOp::Within => 3,
}] += 1;
op_census(l, c);
op_census(r, c);
}
Rx::Thr(_, r) => {
c[4] += 1;
op_census(r, c);
}
Rx::First(r) => {
c[5] += 1;
op_census(r, c);
}
}
}
#[test]
fn generated_sequence_operators_match_the_annex_f_reference() {
const BOUND: u32 = 6;
let mut g = Lcg(0x0711_0711_a5a5_5a5a);
let (mut compared, mut skipped, mut with_empty) = (0usize, 0, 0);
let mut census = [0usize; 6];
for _ in 0..600 {
let rx = gen_rx11(&mut g, 3, false);
let src = render(&rx);
let want = lang_ref(&rx, BOUND as usize + 1);
match try_lang_of(&src, BOUND) {
None => skipped += 1,
Some(got) => {
assert_eq!(got, want, "automaton vs Annex F reference for `{src}`");
compared += 1;
with_empty += usize::from(want.contains(&Vec::new()));
op_census(&rx, &mut census);
}
}
}
assert!(
compared >= 450,
"only {compared} compared, {skipped} skipped"
);
assert!(with_empty >= 40, "only {with_empty} admit an empty match");
for (name, n) in ["and", "or", "intersect", "within", "throughout"]
.iter()
.zip(census)
{
assert!(n >= 60, "only {n} `{name}` operators exercised");
}
}
struct Trace {
rows: BTreeMap<String, Vec<Option<bool>>>,
len: u32,
}
impl Trace {
fn new(rows: &[(&str, &str)]) -> Trace {
let mut map = BTreeMap::new();
let mut len = None;
for (name, bits) in rows {
let row: Vec<Option<bool>> = bits
.chars()
.filter(|c| !c.is_whitespace())
.map(|c| match c {
'0' => Some(false),
'1' => Some(true),
'x' => None,
other => panic!("trace row `{name}`: bad digit {other:?}"),
})
.collect();
assert_eq!(*len.get_or_insert(row.len()), row.len(), "row `{name}`");
map.insert(norm_leaf(name), row);
}
Trace {
rows: map,
len: len.expect("a trace needs at least one row") as u32,
}
}
fn lrm(rows: &[(&str, &str)]) -> Trace {
let padded: Vec<(&str, String)> =
rows.iter().map(|(n, b)| (*n, format!("0{b}"))).collect();
let borrowed: Vec<(&str, &str)> =
padded.iter().map(|(n, b)| (*n, b.as_str())).collect();
Trace::new(&borrowed)
}
fn value(&self, text: &str, tick: u32) -> bool {
if text == "1" {
return true;
}
let (name, negated) = match text.strip_prefix('!') {
Some(inner) if !self.rows.contains_key(text) => (inner, true),
_ => (text, false),
};
let row = self
.rows
.get(name)
.unwrap_or_else(|| panic!("trace has no row for leaf `{name}`"));
match row.get(tick as usize).copied().flatten() {
Some(known) => known != negated,
None => false,
}
}
}
fn run_attempt(
au: &ir::Automaton,
texts: &[String],
tr: &Trace,
start: u32,
) -> (bool, BTreeSet<u32>) {
let r = trace::attempt(au, start, tr.len, &|id, t| {
tr.value(&texts[id.0 as usize], t)
})
.unwrap_or_else(|e| panic!("trace interpreter: {e}"));
(r.admits_empty, r.ends)
}
fn attempts_of(
extra_decls: &str,
body: &str,
tr: &Trace,
starts: &[u32],
) -> Vec<(bool, BTreeSet<u32>)> {
with_built_in(extra_decls, body, |au, leaves, tree| {
let texts = leaf_texts(leaves, tree);
starts
.iter()
.map(|&s| run_attempt(au, &texts, tr, s))
.collect()
})
.unwrap_or_else(|| panic!("`{body}` failed to compile"))
}
fn ends_at(body: &str, tr: &Trace, start: u32) -> BTreeSet<u32> {
attempts_of("", body, tr, &[start]).remove(0).1
}
fn set(v: &[u32]) -> BTreeSet<u32> {
v.iter().copied().collect()
}
const TE: &str = "logic te1, te2, te3, te4, te5;";
fn fig_trace() -> Trace {
Trace::lrm(&[
("te1", "00000001000000"),
("te2", "00000000111110"),
("te3", "00000001000000"),
("te4", "00000000110000"),
("te5", "00000000001110"),
])
}
fn fig_ends(body: &str) -> BTreeSet<u32> {
attempts_of(TE, body, &fig_trace(), &[8]).remove(0).1
}
#[test]
fn lrm_figure_16_5_and_of_two_sequences() {
assert_eq!(fig_ends("te1 ##2 te2"), set(&[10]));
assert_eq!(fig_ends("te3 ##2 te4 ##2 te5"), set(&[12]));
assert_eq!(
fig_ends("(te1 ##2 te2) and (te3 ##2 te4 ##2 te5)"),
set(&[12])
);
}
#[test]
fn lrm_figure_16_6_and_with_a_time_range() {
assert_eq!(fig_ends("te1 ##[1:5] te2"), set(&[9, 10, 11, 12, 13]));
assert_eq!(
fig_ends("(te1 ##[1:5] te2) and (te3 ##2 te4 ##2 te5)"),
set(&[12, 13])
);
}
#[test]
fn lrm_figure_16_7_and_of_two_booleans() {
let tr = Trace::lrm(&[("te1", "11101011010111"), ("te2", "10110001100001")]);
let starts: Vec<u32> = (1..=14).collect();
let got = attempts_of(TE, "te1 and te2", &tr, &starts);
for (s, (empty, ends)) in starts.iter().zip(got) {
assert!(!empty);
let both = tr.value("te1", *s) && tr.value("te2", *s);
assert_eq!(ends, if both { set(&[*s]) } else { set(&[]) }, "tick {s}");
}
let matching: Vec<u32> = starts
.iter()
.copied()
.filter(|&s| !ends_at_in("te1 and te2", &tr, s).is_empty())
.collect();
assert_eq!(matching, vec![1, 3, 8, 14]);
}
fn ends_at_in(body: &str, tr: &Trace, s: u32) -> BTreeSet<u32> {
attempts_of(TE, body, tr, &[s]).remove(0).1
}
#[test]
fn lrm_figure_16_8_intersect() {
assert_eq!(
fig_ends("(te1 ##[1:5] te2) intersect (te3 ##2 te4 ##2 te5)"),
set(&[12])
);
}
#[test]
fn lrm_figure_16_9_or_of_two_booleans() {
let tr = Trace::lrm(&[("te1", "11010101100101"), ("te2", "00101000111000")]);
let starts: Vec<u32> = (1..=14).collect();
let got = attempts_of(TE, "te1 or te2", &tr, &starts);
let failed: Vec<u32> = starts
.iter()
.zip(got)
.filter(|(_, (_, ends))| ends.is_empty())
.map(|(s, _)| *s)
.collect();
assert_eq!(failed, vec![7, 13]);
}
#[test]
fn lrm_figure_16_10_or_of_two_sequences() {
assert_eq!(
fig_ends("(te1 ##2 te2) or (te3 ##2 te4 ##2 te5)"),
set(&[10, 12])
);
}
#[test]
fn lrm_figure_16_11_or_with_a_time_range() {
assert_eq!(
fig_ends("(te1 ##[1:5] te2) or (te3 ##2 te4 ##2 te5)"),
set(&[9, 10, 11, 12, 13])
);
}
const BURST: &str = "logic mclk, burst_mode, irdy, trdy;";
const BURST_RULE1: &str = "$fell(burst_mode) ##0 \
((!burst_mode) throughout (##2 ((trdy==0)&&(irdy==0))[*7]))";
fn burst_trace(not_burst_mode: &str) -> Trace {
Trace::lrm(&[
("$fell(burst_mode)", "01000000000000"),
("!burst_mode", not_burst_mode),
("(trdy==0)&&(irdy==0)", "00011111110000"),
])
}
#[test]
fn lrm_figure_16_12_throughout_restriction_fails() {
let tr = burst_trace("01111111000000");
assert_eq!(
attempts_of(BURST, BURST_RULE1, &tr, &[2]).remove(0).1,
set(&[])
);
assert_eq!(
attempts_of(
BURST,
"$fell(burst_mode) ##0 (##2 ((trdy==0)&&(irdy==0))[*7])",
&tr,
&[2]
)
.remove(0)
.1,
set(&[10])
);
}
#[test]
fn lrm_figure_16_13_throughout_restriction_succeeds() {
let tr = burst_trace("01111111111111");
assert_eq!(
attempts_of(BURST, BURST_RULE1, &tr, &[2]).remove(0).1,
set(&[10])
);
let tr = burst_trace("01111111100000");
assert_eq!(
attempts_of(BURST, BURST_RULE1, &tr, &[2]).remove(0).1,
set(&[])
);
}
#[test]
fn lrm_within_example_matches_from_tick_3_to_11() {
let tr = Trace::lrm(&[
("!trdy", "00011111110000"),
("$fell(irdy)", "00100000000000"),
("!irdy", "00011111111000"),
]);
let body = "!trdy[*7] within ($fell(irdy) ##1 !irdy[*8])";
assert_eq!(attempts_of(BURST, body, &tr, &[3]).remove(0).1, set(&[11]));
let swapped = "($fell(irdy) ##1 !irdy[*8]) within !trdy[*7]";
assert_eq!(attempts_of(BURST, swapped, &tr, &[3]).remove(0).1, set(&[]));
}
#[test]
fn first_match_keeps_the_earliest_ending_match() {
let tr = Trace::new(&[("a", "10000000"), ("b", "01111110")]);
assert_eq!(ends_at("a ##[2:5] b", &tr, 0), set(&[2, 3, 4, 5]));
assert_eq!(ends_at("first_match(a ##[2:5] b)", &tr, 0), set(&[2]));
assert_eq!(ends_at("first_match(a ##[2:5] b)", &tr, 1), set(&[]));
}
#[test]
fn first_match_of_an_or_picks_the_earliest_across_both_arms() {
let body = "first_match((a ##[2:3] b) or (c ##[1:2] d))";
let tr = Trace::new(&[
("a", "10000"),
("b", "00110"),
("c", "10000"),
("d", "00100"),
]);
assert_eq!(
ends_at("(a ##[2:3] b) or (c ##[1:2] d)", &tr, 0),
set(&[2, 3])
);
assert_eq!(ends_at(body, &tr, 0), set(&[2]));
let tr = Trace::new(&[
("a", "10000"),
("b", "00110"),
("c", "10000"),
("d", "01100"),
]);
assert_eq!(
ends_at("(a ##[2:3] b) or (c ##[1:2] d)", &tr, 0),
set(&[1, 2, 3])
);
assert_eq!(ends_at(body, &tr, 0), set(&[1]));
}
#[test]
fn first_match_inside_a_larger_sequence_discards_the_later_matches() {
let plain = "(a ##[1:3] b) ##1 c";
let first = "first_match(a ##[1:3] b) ##1 c";
let tr = Trace::new(&[("a", "1000000"), ("b", "0110000"), ("c", "0001000")]);
assert_eq!(ends_at(plain, &tr, 0), set(&[3]));
assert_eq!(ends_at(first, &tr, 0), set(&[]));
let tr = Trace::new(&[("a", "1000000"), ("b", "0110000"), ("c", "0010000")]);
assert_eq!(ends_at(plain, &tr, 0), set(&[2]));
assert_eq!(ends_at(first, &tr, 0), set(&[2]));
}
#[test]
fn first_match_under_a_product_records_its_end_even_when_the_other_side_disagrees() {
let tr = Trace::new(&[("a", "100000"), ("b", "011000")]);
assert_eq!(
ends_at("(a ##[1:2] b) intersect (a ##2 b)", &tr, 0),
set(&[2])
);
assert_eq!(
ends_at("first_match(a ##[1:2] b) intersect (a ##2 b)", &tr, 0),
set(&[])
);
assert_eq!(
ends_at("first_match(a ##[1:2] b) and (a ##2 b)", &tr, 0),
set(&[2])
);
assert_eq!(
ends_at("first_match(a ##[1:2] b) intersect (a ##1 b)", &tr, 0),
set(&[1])
);
}
#[test]
fn first_match_of_an_empty_admitting_sequence_is_the_empty_match() {
let tr = Trace::new(&[("a", "1111"), ("b", "1100")]);
assert_eq!(
attempts_of("", "first_match(a[*0:2])", &tr, &[0])[0],
(true, set(&[]))
);
assert_eq!(
attempts_of("", "a[*0:2]", &tr, &[0])[0],
(true, set(&[0, 1]))
);
assert_eq!(ends_at("a[*0:2] ##1 b", &tr, 0), set(&[0, 1]));
assert_eq!(ends_at("first_match(a[*0:2]) ##1 b", &tr, 0), set(&[0]));
}
#[test]
fn repeated_first_match_is_one_region_per_repeat() {
let mut g = Lcg(0xfeed_0011);
let (mut compared, mut nonempty) = (0, 0);
for _ in 0..60 {
let tr = random_trace(&mut g, 12);
let rep = attempts_of(
"",
"(first_match(a ##[1:2] b))[*2]",
&tr,
&(0..12).collect::<Vec<_>>(),
);
let unrolled = attempts_of(
"",
"first_match(a ##[1:2] b) ##1 first_match(a ##[1:2] b)",
&tr,
&(0..12).collect::<Vec<_>>(),
);
assert_eq!(rep, unrolled);
compared += rep.len();
nonempty += rep.iter().filter(|(_, e)| !e.is_empty()).count();
}
assert_eq!(compared, 720);
assert!(nonempty >= 40, "only {nonempty} attempts matched");
}
#[test]
fn repetition_of_a_parenthesized_binary_operator() {
assert_eq!(
lang_of("(a and b)[*2]", 8),
Lang::from([word(&[&["a", "b"], &["a", "b"]])])
);
assert_eq!(
lang_of("(a or b)[*1:2]", 8),
Lang::from([
word(&[&["a"]]),
word(&[&["b"]]),
word(&[&["a"], &["a"]]),
word(&[&["a"], &["b"]]),
word(&[&["b"], &["a"]]),
word(&[&["b"], &["b"]]),
])
);
assert_eq!(
lang_of("(a intersect b[*0:1])[*0:1]", 8),
Lang::from([Vec::new(), word(&[&["a", "b"]])])
);
}
fn reachable_states(au: &ir::Automaton) -> usize {
let mut seen = vec![false; au.states.len()];
let mut stack = vec![au.start];
while let Some(s) = stack.pop() {
if std::mem::replace(&mut seen[s.0 as usize], true) {
continue;
}
stack.extend(au.state(s).edges.iter().map(|e| e.target));
}
seen.iter().filter(|&&r| r).count()
}
const OPERATOR_SOURCES: &[&str] = &[
"a ##1 b",
"(a ##[1:3] b) intersect (c ##2 d)",
"(a ##1 b) and (c ##2 d ##1 e)",
"(a ##[1:2] b) or (c[*2] ##1 d)",
"first_match(a ##[1:3] b) ##1 c",
"a throughout (b ##2 c)",
"a within (b ##4 c)",
"(first_match(a ##[1:2] b))[*1:$]",
"((a ##[0:2] b) and (c[*0:2])) within (d ##[2:$] e)",
];
#[test]
fn every_state_of_a_built_automaton_is_reachable() {
for src in OPERATOR_SOURCES {
with_built(src, |au, _, _| {
assert_eq!(
reachable_states(au),
au.states.len(),
"dead states left in the automaton for `{src}`"
);
assert_eq!(au.start, ThreadStateId(0), "`{src}`");
})
.unwrap_or_else(|| panic!("`{src}` failed to compile"));
}
}
#[test]
fn builds_are_deterministic() {
for src in OPERATOR_SOURCES {
let dump = || {
with_built(src, |au, _, _| format!("{au:?}"))
.unwrap_or_else(|| panic!("`{src}` failed to compile"))
};
let first = dump();
for _ in 0..3 {
assert_eq!(first, dump(), "`{src}`");
}
}
}
#[test]
fn first_match_groups_are_one_per_region() {
let groups = |src: &str| {
with_built(src, |au, _, _| {
let (mut begins, mut ends) = (BTreeSet::new(), BTreeSet::new());
for st in &au.states {
for e in &st.edges {
match &e.label {
ir::Transition::FirstMatchBegin { group } => {
begins.insert(group.0);
}
ir::Transition::FirstMatchEnd { group } => {
ends.insert(group.0);
}
_ => {}
}
}
}
assert_eq!(begins, ends, "`{src}`: Begin/End groups differ");
assert_eq!(
begins,
(0..au.first_match_groups).collect::<BTreeSet<_>>(),
"`{src}`"
);
au.first_match_groups
})
.unwrap_or_else(|| panic!("`{src}` failed to compile"))
};
assert_eq!(groups("a ##1 b"), 0);
assert_eq!(groups("first_match(a ##1 b)"), 1);
assert_eq!(groups("first_match(a ##1 b) ##1 first_match(c)"), 2);
assert_eq!(groups("first_match(first_match(a ##[1:2] b))"), 2);
assert_eq!(groups("(first_match(a ##[1:2] b))[*3]"), 3);
assert_eq!(groups("first_match(a[*0:2])"), 0);
assert_eq!(
groups("first_match(a ##[1:2] b) intersect (c ##[1:2] d)"),
1
);
}
#[test]
fn a_runaway_product_is_a_named_error() {
let err = automaton_err("", "(a ##100000 b) intersect (c ##100000 a)");
assert!(err.message.contains("intersect"), "error was: {err}");
assert!(err.message.contains("states"), "error was: {err}");
let err = automaton_err("", "(a ##100000 b) and (c ##100000 a)");
assert!(err.message.contains("`and`"), "error was: {err}");
}
#[test]
fn unimplemented_neighbours_of_the_new_operators_stay_loud() {
let err = automaton_err("", "first_match(a, cnt = cnt + 1)");
assert!(err.message.contains("match item"), "error was: {err}");
assert!(err.message.contains("local variable"), "error was: {err}");
let err = automaton_err("", "a until b");
assert!(err.message.contains("Until"), "error was: {err}");
let err = automaton_err("", "(a |-> b) and c");
assert!(
err.message.contains("OverlappedImplication"),
"error was: {err}"
);
}
fn ref_lens(rx: &Rx, tr: &Trace, s: u32, first: bool) -> BTreeSet<u32> {
let n = tr.len;
let rec = |r: &Rx, st: u32| ref_lens(r, tr, st, first);
match rx {
Rx::Leaf(t) => {
if s < n && tr.value(t, s) {
set(&[1])
} else {
set(&[])
}
}
Rx::Paren(r) => rec(r, s),
Rx::Cat(l, d, r) => {
let mut out = BTreeSet::new();
let hi = d.max.unwrap_or(n + 1).min(n + 1);
for ln in rec(l, s) {
for k in d.min..=hi {
if k == 0 {
if ln == 0 {
continue;
}
for rn in rec(r, s + ln - 1) {
if rn >= 1 {
out.insert(ln - 1 + rn);
}
}
} else {
for rn in rec(r, s + ln + k - 1) {
out.insert(ln + k - 1 + rn);
}
}
}
}
out
}
Rx::Lead(d, r) => {
let mut out = BTreeSet::new();
let hi = d.max.unwrap_or(n).min(n);
for k in d.min..=hi {
for rn in rec(r, s + k) {
out.insert(k + rn);
}
}
out
}
Rx::Rep(r, p) => {
let top = p.max.unwrap_or(n + 2).min(n + 2);
let mut pow = set(&[0]);
let mut out = BTreeSet::new();
if p.min == 0 {
out.insert(0);
}
for k in 1..=top {
let mut next = BTreeSet::new();
for &l in &pow {
for u in rec(r, s + l) {
next.insert(l + u);
}
}
pow = next;
if k >= p.min {
out.extend(pow.iter().copied());
}
}
out
}
Rx::Bin(l, op, r) => {
let ll = rec(l, s);
let rl = rec(r, s);
match op {
SeqOp::Or => ll.union(&rl).copied().collect(),
SeqOp::Intersect => ll.intersection(&rl).copied().collect(),
SeqOp::And => ll
.iter()
.flat_map(|&x| rl.iter().map(move |&y| x.max(y)))
.collect(),
SeqOp::Within => rl
.into_iter()
.filter(|&rn| {
(0..=rn).any(|i| rec(l, s + i).iter().any(|&ln| i + ln <= rn))
})
.collect(),
}
}
Rx::Thr(c, r) => rec(r, s)
.into_iter()
.filter(|&ln| (0..ln).all(|i| tr.value(c, s + i)))
.collect(),
Rx::First(r) => {
let all = rec(r, s);
match all.first() {
Some(&min) if first => set(&[min]),
_ => all,
}
}
}
}
fn ref_attempt(rx: &Rx, tr: &Trace, s: u32, first: bool) -> (bool, BTreeSet<u32>) {
let lens = ref_lens(rx, tr, s, first);
let ends = lens
.iter()
.filter(|&&l| l >= 1 && s + l - 1 < tr.len)
.map(|&l| s + l - 1)
.collect();
(lens.contains(&0), ends)
}
fn random_trace(g: &mut Lcg, len: usize) -> Trace {
let mut rows = Vec::new();
for name in ["a", "b", "c"] {
let bits: String = (0..len)
.map(|_| if g.next(5) < 3 { '1' } else { '0' })
.collect();
rows.push((name, bits));
}
let borrowed: Vec<(&str, &str)> = rows.iter().map(|(n, b)| (*n, b.as_str())).collect();
Trace::new(&borrowed)
}
#[test]
fn the_trace_reference_agrees_with_the_lrm_examples() {
let leaf = |n| Box::new(Rx::Leaf(n));
let d = |min, max, text| Dl { min, max, text };
let a_b = Rx::Cat(leaf("a"), d(2, Some(5), "##[2:5]"), leaf("b"));
let tr = Trace::new(&[("a", "10000000"), ("b", "01111110")]);
assert_eq!(ref_attempt(&a_b, &tr, 0, true).1, set(&[2, 3, 4, 5]));
let fm = Rx::First(Box::new(a_b));
assert_eq!(ref_attempt(&fm, &tr, 0, true).1, set(&[2]));
assert_eq!(ref_attempt(&fm, &tr, 0, false).1, set(&[2, 3, 4, 5]));
let ab_and = Rx::Bin(
Box::new(Rx::Cat(leaf("a"), d(1, Some(1), "##1"), leaf("b"))),
SeqOp::And,
Box::new(Rx::Cat(leaf("a"), d(2, Some(2), "##2"), leaf("b"))),
);
let tr = Trace::new(&[("a", "111000"), ("b", "011100")]);
assert_eq!(ref_attempt(&ab_and, &tr, 0, true).1, set(&[2]));
}
#[test]
fn generated_sequences_match_the_trace_reference() {
const LEN: u32 = 9;
let mut g = Lcg(0xd1ff_e2e1_7ace_0011);
let (mut compared, mut skipped, mut attempts) = (0usize, 0, 0usize);
let (mut first_matters, mut with_matches) = (0usize, 0usize);
let mut census = [0usize; 6];
for _ in 0..500 {
let rx = gen_rx11(&mut g, 3, true);
let src = render(&rx);
let traces: Vec<Trace> = (0..4).map(|_| random_trace(&mut g, LEN as usize)).collect();
let ok = with_built(&src, |au, leaves, tree| {
let texts = leaf_texts(leaves, tree);
for tr in &traces {
for s in 0..LEN {
let got = run_attempt(au, &texts, tr, s);
let want = ref_attempt(&rx, tr, s, true);
assert_eq!(got, want, "`{src}` from tick {s} over {:?}", tr.rows);
attempts += 1;
with_matches += usize::from(!want.1.is_empty());
first_matters += usize::from(want != ref_attempt(&rx, tr, s, false));
}
}
});
match ok {
Some(()) => {
compared += 1;
op_census(&rx, &mut census);
}
None => skipped += 1,
}
}
assert!(
compared >= 380,
"only {compared} compared, {skipped} skipped"
);
assert!(
with_matches >= 2000,
"only {with_matches} of {attempts} attempts matched"
);
assert!(
first_matters >= 150,
"first_match changed the result in only {first_matters} attempts"
);
for (name, n) in [
"and",
"or",
"intersect",
"within",
"throughout",
"first_match",
]
.iter()
.zip(census)
{
assert!(n >= 40, "only {n} `{name}` operators exercised");
}
}
fn with_assertion<R>(
decls: &str,
stmt: &str,
allow_errors: bool,
f: impl FnOnce(
Result<(ir::Automaton, LeafTable<'_>), LoweringError>,
&SyntaxTree,
&sv_lang::Diagnostics,
) -> R,
) -> R {
let src = format!(
"module m;\n\
logic clk, sysclk, a, b, c, d, e, x, y, z;\n\
logic [7:0] bb;\n\
int n;\n\
parameter my_delay = 2;\n\
{decls}\n\
always_ff @(posedge clk) begin\n\
{stmt}\n\
end\n\
endmodule\n"
);
let session = Session::new();
let mut comp = Compilation::new(&session).unwrap();
comp.add_source(&src).unwrap();
let design = comp.compile().unwrap();
let diags = design.diagnostics();
if !allow_errors {
assert!(
!diags.has_errors(),
"fixture has compile errors:\n{}\n{src}",
diags.rendered()
);
}
let m = design
.top_instances()
.next()
.unwrap()
.instance_body()
.unwrap();
let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
let proc = analysis.procedures(m).next().unwrap();
let Some(assertion) = analysis.assertions(proc.symbol()).next() else {
panic!(
"slang dropped the assertion; analysis diagnostics:\n{}",
analysis.diagnostics().rendered()
);
};
let tree = design.syntax_trees().into_iter().next().unwrap();
let root = assertion.root().as_assertion_expr().unwrap();
let (root, root_clock) = if root.kind() == AssertionExprKind::Clocking {
let kids = root.children();
(kids[1].as_assertion_expr().unwrap(), Some(kids[0]))
} else {
(root, None)
};
f(
build_automaton(root, root_clock, (&tree).into(), &m),
&tree,
&diags,
)
}
struct Built {
debug: String,
leaves: Vec<String>,
lang: Lang,
}
fn built(decls: &str, stmt: &str, bound: u32) -> Built {
with_assertion(decls, stmt, false, |r, tree, _| {
let (au, leaves) = r.unwrap_or_else(|e| panic!("`{stmt}` failed to build: {e}"));
Built {
debug: format!("{au:?}"),
leaves: leaf_texts(&leaves, tree),
lang: accepted_lang(&au, &leaves, tree, bound),
}
})
}
fn built_err(decls: &str, stmt: &str) -> LoweringError {
with_assertion(decls, stmt, false, |r, _, _| {
r.err()
.unwrap_or_else(|| panic!("`{stmt}` was expected to be rejected"))
})
}
fn built_err_lenient(decls: &str, stmt: &str) -> LoweringError {
with_assertion(decls, stmt, true, |r, _, _| {
r.err()
.unwrap_or_else(|| panic!("`{stmt}` was expected to be rejected"))
})
}
#[test]
fn s1_rule_instantiation_equivalent_to_inline() {
let decls = "sequence s; a ##1 b ##1 c; endsequence\n\
sequence rule; @(posedge clk) x ##1 y ##1 s ##1 z; endsequence";
let inst = built(decls, "assert property (rule);", 8);
let inline = built(
"",
"assert property (@(posedge clk) x ##1 y ##1 (a ##1 b ##1 c) ##1 z);",
8,
);
assert_eq!(inst.leaves, ["x", "y", "a", "b", "c", "z"]);
assert_eq!(
inst.lang,
Lang::from([word(&[&["x"], &["y"], &["a"], &["b"], &["c"], &["z"]])])
);
assert_eq!(inst.lang, inline.lang);
assert_eq!(inst.leaves, inline.leaves);
assert_eq!(inst.debug, inline.debug);
}
#[test]
fn untyped_formals_substitute_boolean_and_sequence_actuals() {
let decls = "sequence s(p, q); p ##2 q; endsequence";
let b = built(decls, "assert property (@(posedge clk) s(a ##1 b, c));", 8);
assert_eq!(b.leaves, ["a", "b", "c"]);
assert_eq!(b.lang, Lang::from([word(&[&["a"], &["b"], &[], &["c"]])]));
let b = built(decls, "assert property (@(posedge clk) s(a, b));", 8);
assert_eq!(b.lang, Lang::from([word(&[&["a"], &[], &["b"]])]));
}
#[test]
fn default_actuals_are_used_overridden_and_bound_by_name() {
let decls = "sequence s(p, q = c, int k = 2); p ##k q; endsequence";
let w = |stmt: &str| built(decls, stmt, 8).lang;
assert_eq!(
w("assert property (@(posedge clk) s(a));"),
Lang::from([word(&[&["a"], &[], &["c"]])])
);
assert_eq!(
w("assert property (@(posedge clk) s(a, b, 3));"),
Lang::from([word(&[&["a"], &[], &[], &["b"]])])
);
assert_eq!(
w("assert property (@(posedge clk) s(.p(a), .k(1)));"),
Lang::from([word(&[&["a"], &["c"]])])
);
}
#[test]
fn typed_formal_bit_truncates_wider_actual() {
let decls = "sequence s1(w, x, y); w ##1 x ##[2:10] y; endsequence\n\
sequence s2(w, y, bit x); w ##1 x ##[2:10] y; endsequence";
let x_leaf = |stmt: &str| {
with_assertion(decls, stmt, false, |r, _, _| {
let (au, leaves) = r.unwrap();
let x = leaves.get(LeafId(1));
(
x.kind() == ExpressionKind::Conversion,
x.expr_type().unwrap().bit_width(),
reachable_lengths(&au, 20),
format!("{au:?}"),
)
})
};
let (typed_conv, typed_width, typed_lens, typed_au) =
x_leaf("assert property (@(posedge clk) s2(.w(a), .x(bb), .y(c)));");
let (_, cast_width, _, cast_au) =
x_leaf("assert property (@(posedge clk) s1(.w(a), .x(bit'(bb)), .y(c)));");
let (untyped_conv, untyped_width, _, _) =
x_leaf("assert property (@(posedge clk) s1(.w(a), .x(bb), .y(c)));");
assert!(typed_conv, "the typed formal must cast the 8-bit actual");
assert_eq!(typed_width, 1, "cast to bit = truncation to 1 bit");
assert_eq!(cast_width, 1);
assert!(!untyped_conv, "an untyped formal keeps the actual as is");
assert_eq!(untyped_width, 8);
assert_eq!(typed_lens, (3..=11).collect::<BTreeSet<u32>>());
assert_eq!(typed_au, cast_au);
}
#[test]
fn typed_delay_formal_is_cast_to_its_type() {
let b = built(
"sequence s(shortint k, untyped p); p ##k b; endsequence",
"assert property (@(posedge clk) s(65537, a));",
8,
);
assert_eq!(b.lang, Lang::from([word(&[&["a"], &["b"]])]));
}
#[test]
fn dollar_actual_requires_untyped_formal_used_as_upper_bound() {
let dollar = |decls: &str, stmt: &str| built(decls, stmt, 5);
let d = dollar(
"sequence s(max, p); p ##[1:max] b; endsequence",
"assert property (@(posedge clk) s($, a));",
);
assert_eq!(
d.debug,
built("", "assert property (@(posedge clk) a ##[1:$] b);", 5).debug
);
assert_eq!(d.lang.len(), 5, "b may follow a 1..=5 ticks later");
let r = dollar(
"sequence s(max, p); p[*2:max]; endsequence",
"assert property (@(posedge clk) s($, a) ##1 b);",
);
assert_eq!(
r.debug,
built("", "assert property (@(posedge clk) a[*2:$] ##1 b);", 5).debug
);
let fwd = dollar(
"sequence inner(m, p); p ##[1:m] b; endsequence\n\
sequence outer(m2, p); inner(m2, p); endsequence",
"assert property (@(posedge clk) outer($, a));",
);
assert_eq!(d.debug, fwd.debug);
let decls = "sequence s(k, p); p ##[k:5] b; endsequence";
let stmt = "assert property (@(posedge clk) s($, a));";
let e = built_err_lenient(decls, stmt);
assert!(e.message.contains("upper bound"), "{e}");
with_assertion(decls, stmt, true, |_, _, diags| {
let e = crate::sva::named::check_formal_argument_rules(diags)
.expect_err("`$` into a lower bound is a diagnosed error");
assert!(e.message.contains("`$`"), "{e}");
});
}
#[test]
fn lrm_delay_arg_example_equals_its_inline_form() {
let decls = "sequence delay_arg_example (max, shortint delay1, delay2, min);\n\
x ##delay1 y[*min:max] ##delay2 z;\n\
endsequence";
let inst = built(
decls,
"cover property (delay_arg_example($, my_delay, my_delay-1, 3));",
10,
);
let inline = built("", "cover property (x ##2 y[*3:$] ##1 z);", 10);
assert_eq!(inst.debug, inline.debug);
assert_eq!(inst.leaves, inline.leaves);
assert_eq!(inst.lang, inline.lang);
assert!(!inst.lang.is_empty());
}
#[test]
fn lrm_delay_example_legal_builds_and_illegal_is_diagnosed() {
let decls = "int zz, dd;\n\
sequence delay_example(x, y, min, max, delay1);\n\
x ##delay1 y[*min:max];\n\
endsequence";
let ok = built(
decls,
"assert property (@(posedge clk) delay_example(x, y, 3, $, 2));",
8,
);
assert_eq!(
ok.debug,
built("", "assert property (@(posedge clk) x ##2 y[*3:$]);", 8).debug
);
with_assertion(
decls,
"assert property (@(posedge clk) delay_example(x, y, zz, $, dd));",
true,
|r, _, diags| {
crate::sva::named::check_formal_argument_rules(diags)
.expect_err("non-constant actuals in a delay/repetition are illegal");
assert!(r.is_err(), "a non-constant bound is not buildable");
},
);
}
#[test]
fn lrm_event_arg_examples_equal_the_inline_clocked_sequence() {
let inline = built("", "cover property (@(posedge clk) x ##1 y);", 4);
let ev = built(
"sequence event_arg_example (event ev); @(ev) x ##1 y; endsequence",
"cover property (event_arg_example(posedge clk));",
4,
);
let ev2 = built(
"sequence event_arg_example2 (reg sig); @(posedge sig) x ##1 y; endsequence",
"cover property (event_arg_example2(clk));",
4,
);
assert_eq!(inline.lang, Lang::from([word(&[&["x"], &["y"]])]));
for got in [&ev, &ev2] {
assert_eq!(got.debug, inline.debug);
assert_eq!(got.leaves, inline.leaves);
}
}
#[test]
fn a_callers_formal_passed_as_a_delay_is_resolved_in_the_callers_frame() {
let b = built(
"sequence inner(p, int k); p ##k b; endsequence\n\
sequence outer(w, int d); inner(w, d) ##1 c; endsequence",
"assert property (@(posedge clk) outer(a, my_delay+1));",
8,
);
assert_eq!(
b.lang,
Lang::from([word(&[&["a"], &[], &[], &["b"], &["c"]])])
);
}
#[test]
fn a_sequence_actual_is_resolved_in_the_call_site_frame() {
let b = built(
"sequence q(sequence s, int k); s ##k b; endsequence\n\
sequence outer(int d); q(a ##d c, 2); endsequence",
"assert property (@(posedge clk) outer(3));",
10,
);
assert_eq!(
b.lang,
Lang::from([word(&[&["a"], &[], &[], &["c"], &[], &["b"]])])
);
}
#[test]
fn a_formal_shadows_a_module_constant_of_the_same_name() {
let b = built(
"parameter k = 5;\n\
sequence s(k, p); p ##k b; endsequence",
"assert property (@(posedge clk) s(2, a));",
8,
);
assert_eq!(b.lang, Lang::from([word(&[&["a"], &[], &["b"]])]));
}
#[test]
fn a_repeated_instance_expands_the_body_per_repeat() {
let b = built(
"sequence s(p); p ##1 b; endsequence",
"assert property (@(posedge clk) s(a)[*2] ##1 c);",
8,
);
assert_eq!(
b.lang,
Lang::from([word(&[&["a"], &["b"], &["a"], &["b"], &["c"]])])
);
assert_eq!(b.leaves, ["a", "b", "a", "b", "c"]);
}
#[test]
fn typed_formal_cast_incompatible_and_event_actuals_are_rejected() {
let e = built_err_lenient(
"int arr[2]; sequence s(int k, p); p ##1 (k == 1); endsequence",
"assert property (@(posedge clk) s(arr, a));",
);
assert!(e.message.contains("slang could not bind"), "{e}");
let e = built_err_lenient(
"sequence s(sequence q); q; endsequence",
"assert property (@(posedge clk) s(posedge clk));",
);
assert!(e.message.contains("slang could not bind"), "{e}");
}
#[test]
fn goto_repetition_on_an_instance_is_rejected() {
let e = built_err_lenient(
"sequence s(p); p ##1 b; endsequence",
"assert property (@(posedge clk) s(a)[->2]);",
);
assert!(e.message.contains("named sequence instance"), "{e}");
let e = built_err_lenient(
"sequence s(p); p ##1 b; endsequence",
"assert property (@(posedge clk) s(a)[=2]);",
);
assert!(e.message.contains("named sequence instance"), "{e}");
}
#[test]
fn actual_argument_cycle_through_another_sequence_is_rejected() {
let e = built_err(
"sequence s(p); p ##1 b; endsequence\n\
sequence user; s(s(a)); endsequence",
"assert property (@(posedge clk) user);",
);
assert!(e.message.contains("cyclic dependency"), "{e}");
assert!(e.message.contains("`s`"), "{e}");
with_assertion(
"sequence s(p); p ##1 b; endsequence",
"assert property (@(posedge clk) s(s(a)));",
true,
|r, _, diags| {
let e = crate::sva::named::check_named_sequence_cycles(diags)
.expect_err("slang reports s(s(a)) as a cycle");
assert!(e.message.contains("cyclic dependency"), "{e}");
assert!(r.is_err(), "the builder must not build a cyclic instance");
},
);
}
#[test]
fn an_actual_that_instantiates_a_sequence_the_callee_also_instantiates_is_legal() {
let decls = "sequence inner(p); p ##1 b; endsequence\n\
sequence outer(w); inner(w) ##1 c; endsequence";
let nested = built(
decls,
"assert property (@(posedge clk) outer(inner(a)));",
8,
);
let inline = built(
"",
"assert property (@(posedge clk) a ##1 b ##1 b ##1 c);",
8,
);
assert_eq!(
nested.lang,
Lang::from([word(&[&["a"], &["b"], &["b"], &["c"]])])
);
assert_eq!(nested.lang, inline.lang);
assert_eq!(nested.leaves, inline.leaves);
let via_user = built(
"sequence inner(p); p ##1 b; endsequence\n\
sequence outer(w); inner(w) ##1 c; endsequence\n\
sequence user; outer(inner(a)); endsequence",
"assert property (@(posedge clk) user);",
8,
);
assert_eq!(via_user.lang, nested.lang);
let deep = built(
"sequence inner(p); p ##1 b; endsequence\n\
sequence mid(q); inner(q) ##1 d; endsequence\n\
sequence outer(w); mid(w) ##1 c; endsequence",
"assert property (@(posedge clk) outer(mid(inner(a))));",
12,
);
let deep_inline = built(
"",
"assert property (@(posedge clk) a ##1 b ##1 b ##1 d ##1 b ##1 d ##1 c);",
12,
);
assert_eq!(deep.lang, deep_inline.lang);
assert_eq!(deep.leaves, deep_inline.leaves);
let bound = built(
"sequence inner(p, int k); p ##k b; endsequence\n\
sequence outer(w); inner(w, 1) ##1 c; endsequence",
"assert property (@(posedge clk) outer(inner(a, 3)));",
12,
);
assert_eq!(
bound.lang,
Lang::from([word(&[&["a"], &[], &[], &["b"], &["b"], &["c"]])])
);
let twice = built(
"sequence inner(p); p ##1 b; endsequence\n\
sequence outer(w); w ##1 w; endsequence",
"assert property (@(posedge clk) outer(inner(a)));",
8,
);
assert_eq!(
twice.lang,
Lang::from([word(&[&["a"], &["b"], &["a"], &["b"]])])
);
let zero = built(
"sequence inner(p); p ##1 b; endsequence\n\
sequence zs; inner(a); endsequence\n\
sequence outer(w); inner(w) ##1 c; endsequence",
"assert property (@(posedge clk) outer(zs));",
8,
);
assert_eq!(
zero.lang,
Lang::from([word(&[&["a"], &["b"], &["b"], &["c"]])])
);
}
#[test]
fn a_real_body_cycle_is_still_rejected_after_the_actual_argument_fix() {
let e = built_err(
"sequence s(p); p ##1 b; endsequence\n\
sequence user; s(s(a)); endsequence",
"assert property (@(posedge clk) user);",
);
assert!(e.message.contains("cyclic dependency"), "{e}");
let e = built_err(
"sequence s(p); p ##1 b; endsequence\n\
sequence wrap(w); s(w); endsequence\n\
sequence user; s(wrap(a)); endsequence",
"assert property (@(posedge clk) user);",
);
assert!(e.message.contains("cyclic dependency"), "{e}");
assert!(
e.message.contains("`s`") && e.message.contains("`wrap`"),
"{e}"
);
let e = built_err(
"sequence fc(p); p; endsequence\n\
sequence fa(w); fc(w); endsequence\n\
sequence bb2(q); fa(q); endsequence\n\
sequence user; fa(bb2(a)); endsequence",
"assert property (@(posedge clk) user);",
);
assert!(e.message.contains("cyclic dependency"), "{e}");
assert!(
e.message.contains("`fa`") && e.message.contains("`bb2`"),
"{e}"
);
}
#[test]
fn property_instance_is_a_loud_error_in_the_sequence_builder() {
let e = built_err(
"property p0(q); q ##1 b; endproperty",
"assert property (@(posedge clk) p0(a));",
);
assert!(e.message.contains("property instance"), "{e}");
assert!(e.message.contains("build_property"), "{e}");
}
#[test]
fn local_variables_in_a_sequence_build() {
let with_formal = built(
"sequence s(p, local logic v); p ##1 b; endsequence",
"assert property (@(posedge clk) s(a, 1'b1));",
6,
);
let with_local = built(
"sequence s; logic v; a ##1 b; endsequence",
"assert property (@(posedge clk) s);",
6,
);
let plain = built("", "assert property (@(posedge clk) a ##1 b);", 6);
assert_eq!(with_formal.lang, plain.lang);
assert_eq!(with_local.lang, plain.lang);
}
fn clock_info(decls: &str, stmt: &str) -> (usize, ClockId, Vec<(u32, bool)>) {
with_assertion(decls, stmt, false, |r, _, _| {
let (au, leaves) = r.unwrap_or_else(|e| panic!("`{stmt}` failed to build: {e}"));
let syncs = au
.states
.iter()
.flat_map(|st| &st.edges)
.filter_map(|e| match &e.label {
Transition::ClockSync { to, strict } => Some((to.0, *strict)),
_ => None,
})
.collect();
(leaves.clock_count(), au.entry_clock, syncs)
})
}
#[test]
fn a_second_clocking_event_is_a_second_clock() {
let decls = "sequence sa; @(posedge clk) a ##1 b; endsequence\n\
sequence sb; @(negedge clk) c ##1 d; endsequence";
let (clocks, entry, syncs) = clock_info(decls, "assert property (sa ##1 sb);");
assert_eq!(clocks, 2);
assert_eq!(entry, ClockId(0));
assert_eq!(syncs, [(1, true)]);
let (_, _, syncs) = clock_info(decls, "assert property (sa ##0 sb);");
assert_eq!(syncs, [(1, false)]);
}
#[test]
fn a_root_clock_differing_from_an_instances_clock_leads_with_the_instance() {
let decls = "sequence s; @(posedge sysclk) a ##1 b; endsequence";
for (root, differs) in [
("@(negedge clk)", true),
("@(posedge clk)", true),
("@(posedge sysclk)", false),
] {
let stmt = format!("assert property ({root} s);");
if differs {
let (clocks, entry, syncs) = clock_info(decls, &stmt);
assert!(syncs.is_empty(), "{root}: nothing changes clock inside s");
assert_eq!(clocks, 2, "{root}");
assert_eq!(entry, ClockId(1), "{root}: s runs on its own clock");
} else {
let b = built(decls, &stmt, 4);
let inline = built("", "assert property (@(posedge sysclk) a ##1 b);", 4);
assert_eq!(b.debug, inline.debug, "{root}");
assert_eq!(b.lang, Lang::from([word(&[&["a"], &["b"]])]));
}
}
let ev = "sequence es(event ev); @(ev) a ##1 b; endsequence";
let ok = built(ev, "assert property (@(posedge clk) es(posedge clk));", 4);
assert_eq!(ok.lang, Lang::from([word(&[&["a"], &["b"]])]));
let (clocks, entry, _) =
clock_info(ev, "assert property (@(posedge clk) es(negedge clk));");
assert_eq!((clocks, entry), (2, ClockId(1)));
let plain = built(
"sequence u; a ##1 b; endsequence",
"assert property (@(negedge clk) u);",
4,
);
assert_eq!(plain.lang, Lang::from([word(&[&["a"], &["b"]])]));
let (clocks, entry, _) = clock_info(
"sequence u; a ##1 b; endsequence",
"assert property (@(negedge clk) u);",
);
assert_eq!((clocks, entry), (1, ClockId(0)));
}
#[test]
fn clocking_events_differing_only_in_operator_index_or_iff_are_different_clocks() {
let pairs: &[(&str, &str)] = &[
("@(posedge (a | b))", "@(posedge (a & b))"),
("@(posedge (a ^ b))", "@(posedge (a & b))"),
("@(posedge bb[1])", "@(posedge bb[0])"),
("@(posedge clk iff (n == 2))", "@(posedge clk iff (n == 1))"),
("@(posedge clk iff (n == 1))", "@(posedge clk)"),
("@(posedge clk or posedge a)", "@(posedge clk or negedge a)"),
("@(posedge clk or posedge a)", "@(posedge clk)"),
("@(posedge ~a)", "@(posedge !a)"),
];
for (inst_ev, root_ev) in pairs {
for (decl_ev, root) in [(inst_ev, root_ev), (root_ev, inst_ev)] {
let decls = format!("sequence s; {decl_ev} c ##1 d; endsequence");
let (clocks, _, _) = clock_info(&decls, &format!("assert property ({root} s);"));
assert_eq!(clocks, 2, "{decl_ev} vs {root}");
}
let decls = format!("sequence s; {inst_ev} c ##1 d; endsequence");
let stmt = format!("assert property ({inst_ev} s);");
let (clocks, _, _) = clock_info(&decls, &stmt);
assert_eq!(clocks, 1, "{inst_ev}");
let b = built(&decls, &stmt, 4);
assert_eq!(b.lang, Lang::from([word(&[&["c"], &["d"]])]), "{inst_ev}");
}
let (clocks, _, syncs) = clock_info(
"sequence sa; @(posedge (a | b)) c ##1 d; endsequence\n\
sequence sb; @(posedge (a & b)) c ##1 d; endsequence",
"assert property (sa ##1 sb);",
);
assert_eq!((clocks, syncs), (2, vec![(1, true)]));
}
#[test]
fn instance_expansion_is_deterministic() {
let decls = "sequence inner(p, int k); p ##k b; endsequence\n\
sequence outer(w, int d); inner(w, d)[*1:2] ##1 c; endsequence";
let stmt = "assert property (@(posedge clk) outer(a, 2) ##1 outer(b, 1));";
let first = built(decls, stmt, 10);
let second = built(decls, stmt, 10);
assert_eq!(first.debug, second.debug);
assert_eq!(first.leaves, second.leaves);
assert!(!first.lang.is_empty());
}
const LV: &str = "`define true 1\nint data, data1, data2, data_in, data_out, do1;\n";
fn lv(decls: &str) -> String {
format!("{LV}{decls}")
}
fn builds(decls: &str, stmt: &str) -> Result<(), LoweringError> {
with_assertion(decls, stmt, false, |r, _, _| r.map(|_| ()))
}
#[test]
fn t13_s4_a_sibling_thread_read_does_not_flow() {
let e = built_err(
&lv("sequence s4;\n\
int x;\n\
(a ##1 (b, x = data) ##1 c) or (d ##1 (e==x)); // illegal\n\
endsequence"),
"assert property (@(posedge clk) s4);",
);
assert!(
e.message.contains("does not flow out") && e.message.contains("`x`"),
"{e}"
);
}
#[test]
fn t13_s5_a_variable_assigned_on_one_or_branch_does_not_flow_out() {
let e = built_err(
&lv("sequence s5;\n\
int x,y;\n\
((a ##1 (b, x = data, y = data1) ##1 c)\n\
or (d ##1 (`true, x = data) ##0 (e==x))) ##1 (y==data2);\n\
// illegal because y is not in the intersection\n\
endsequence"),
"assert property (@(posedge clk) s5);",
);
assert!(
e.message.contains("does not flow out") && e.message.contains("`y`"),
"{e}"
);
}
#[test]
fn t13_s6_a_variable_assigned_on_both_or_branches_flows_out() {
builds(
&lv("sequence s6;\n\
int x,y;\n\
((a ##1 (b, x = data, y = data1) ##1 c)\n\
or (d ##1 (`true, x = data) ##0 (e==x))) ##1 (x==data2);\n\
// legal because x is in the intersection\n\
endsequence"),
"assert property (@(posedge clk) s6);",
)
.unwrap();
}
#[test]
fn t13_s7_a_variable_assigned_in_both_and_operands_is_blocked() {
let e = built_err(
&lv("sequence s7;\n\
int x,y;\n\
((a ##1 (b, x = data, y = data1) ##1 c)\n\
and (d ##1 (`true, x = data) ##0 (e==x))) ##1 (x==data2);\n\
// illegal because x is common to both threads\n\
endsequence"),
"assert property (@(posedge clk) s7);",
);
assert!(
e.message.contains("does not flow out") && e.message.contains("`x`"),
"{e}"
);
}
#[test]
fn t13_s8_a_variable_in_the_and_difference_flows_out() {
builds(
&lv("sequence s8;\n\
int x,y;\n\
((a ##1 (b, x = data, y = data1) ##1 c)\n\
and (d ##1 (`true, x = data) ##0 (e==x))) ##1 (y==data2);\n\
// legal because y is in the difference\n\
endsequence"),
"assert property (@(posedge clk) s8);",
)
.unwrap();
}
fn eval_leaf_expr<'d>(
e: Expression<'d>,
locals: &LeafLocals<'d>,
frame: &[Option<i64>],
tick: u32,
sig: &dyn Fn(&str, u32) -> i64,
) -> Result<i64, trace::TraceError> {
eval_leaf_node(e, locals, frame, tick, sig, &std::cell::Cell::new(0))
}
fn eval_leaf_id<'d>(
leaves: &LeafTable<'d>,
id: LeafId,
frame: &[Option<i64>],
tick: u32,
sig: &dyn Fn(&str, u32) -> i64,
) -> Result<i64, trace::TraceError> {
let v = eval_leaf_expr(leaves.get(id), leaves.locals_of(id), frame, tick, sig)?;
Ok(if leaves.is_negated(id) {
i64::from(v == 0)
} else {
v
})
}
fn eval_leaf_node<'d>(
e: Expression<'d>,
locals: &LeafLocals<'d>,
frame: &[Option<i64>],
tick: u32,
sig: &dyn Fn(&str, u32) -> i64,
next_flag: &std::cell::Cell<usize>,
) -> Result<i64, trace::TraceError> {
let kids = e.as_sem_node().children();
let sub = |i: usize| -> Result<i64, trace::TraceError> {
let k = kids[i]
.as_expression()
.expect("an operand of a leaf expression is an expression");
eval_leaf_node(k, locals, frame, tick, sig, next_flag)
};
if end_point_call(e).is_some() {
let n = next_flag.get();
next_flag.set(n + 1);
return trace::read_local(frame, locals.end_flags[n]);
}
match e.kind() {
ExpressionKind::IntegerLiteral => Ok(e
.integer_literal_value()
.and_then(|v| v.as_i64())
.expect("an integer literal fits an i64")),
ExpressionKind::NamedValue => {
let sym = e.referenced_symbol().expect("a named value has a symbol");
match locals.reads.iter().find(|(s, _)| *s == sym) {
Some((_, slot)) => trace::read_local(frame, *slot),
None => Ok(sig(sym.name(), tick)),
}
}
ExpressionKind::LValueReference => trace::read_local(
frame,
locals
.lvalue
.expect("an LValueReference leaf has an lvalue"),
),
ExpressionKind::Conversion => sub(0),
ExpressionKind::UnaryOp => match e.unary_op() {
Some(sv_lang::UnaryOp::LogicalNot) => Ok(i64::from(sub(0)? == 0)),
other => panic!("test evaluator: unary operator {other:?}"),
},
ExpressionKind::BinaryOp => {
let (l, r) = (sub(0)?, sub(1)?);
match e.binary_op() {
Some(sv_lang::BinaryOp::Add) => Ok(l + r),
Some(sv_lang::BinaryOp::Subtract) => Ok(l - r),
Some(sv_lang::BinaryOp::Equality) => Ok(i64::from(l == r)),
Some(sv_lang::BinaryOp::LessThanEqual) => Ok(i64::from(l <= r)),
Some(sv_lang::BinaryOp::LogicalAnd) => Ok(i64::from(l != 0 && r != 0)),
Some(sv_lang::BinaryOp::LogicalOr) => Ok(i64::from(l != 0 || r != 0)),
other => panic!("test evaluator: binary operator {other:?}"),
}
}
other => panic!("test evaluator: expression kind {other:?}"),
}
}
struct Ran {
attempts: Vec<trace::LocalAttempt>,
slots: BTreeMap<String, LocalVarId>,
}
fn attempts_on(
au: &ir::Automaton,
leaves: &LeafTable<'_>,
signals: &[(&str, &[i64])],
starts: &[u32],
) -> Vec<trace::LocalAttempt> {
let len = signals[0].1.len() as u32;
assert!(signals.iter().all(|(_, row)| row.len() as u32 == len));
let sig = |name: &str, t: u32| -> i64 {
signals
.iter()
.find(|(n, _)| *n == name)
.unwrap_or_else(|| panic!("the trace has no signal `{name}`"))
.1[t as usize]
};
starts
.iter()
.map(|&s| {
trace::attempt_with_locals(au, s, len, &|id, tick, frame| {
eval_leaf_id(leaves, id, frame, tick, &sig)
})
.unwrap_or_else(|e| panic!("trace interpreter: {e}"))
})
.collect()
}
fn local_run(decls: &str, stmt: &str, signals: &[(&str, &[i64])], starts: &[u32]) -> Ran {
with_assertion(&lv(decls), stmt, false, |r, _, _| {
let (au, leaves) = r.unwrap_or_else(|e| panic!("`{stmt}` failed to build: {e}"));
let attempts = attempts_on(&au, &leaves, signals, starts);
let mut slots = BTreeMap::new();
for i in 0..leaves.len() as u32 {
for (sym, slot) in &leaves.locals_of(LeafId(i)).reads {
slots.insert(sym.name().to_string(), *slot);
}
}
Ran { attempts, slots }
})
}
fn ends_with(ran: &Ran, i: usize, var: &str) -> BTreeSet<(u32, Option<i64>)> {
let slot = ran.slots[var].0 as usize;
ran.attempts[i]
.matches
.iter()
.map(|(t, f)| (*t, f[slot]))
.collect()
}
fn init_writes(au: &ir::Automaton) -> Vec<(LocalVarId, LeafId)> {
let mut writes = Vec::new();
let mut st = au.start;
while let [edge] = au.state(st).edges.as_slice() {
if edge.guard.is_some() {
break;
}
match &edge.label {
Transition::LocalVarWrite { var, value } => writes.push((*var, *value)),
Transition::Epsilon => {}
_ => break,
}
st = edge.target;
}
writes
}
#[test]
fn t13_input_formals_are_initialised_before_declared_locals() {
let decls = "sequence q(local input int f); int v = f + 1; a ##1 (v == 8); endsequence";
let stmt = "assert property (@(posedge clk) q(7));";
with_assertion(&lv(decls), stmt, false, |r, tree, _| {
let (au, leaves) = r.unwrap();
let texts = leaf_texts(&leaves, tree);
let writes = init_writes(&au);
assert_eq!(writes.len(), 2, "one write per formal and per initialiser");
assert_eq!(texts[writes[0].1.0 as usize], "7");
assert_eq!(texts[writes[1].1.0 as usize], "f+1");
});
let sigs: [(&str, &[i64]); 1] = [("a", &[1, 0, 0])];
let ran = local_run(decls, stmt, &sigs, &[0]);
assert_eq!(ran.attempts[0].ends(), BTreeSet::from([1]), "7 + 1 == 8");
let ran = local_run(decls, "assert property (@(posedge clk) q(6));", &sigs, &[0]);
assert!(ran.attempts[0].matches.is_empty(), "6 + 1 != 8");
}
#[test]
fn t13_the_input_actual_is_cast_to_the_formals_type() {
let decls = "sequence q(local input logic [3:0] r); a ##1 (r == 3); endsequence";
let sigs: [(&str, &[i64]); 1] = [("a", &[1, 0])];
let ran = local_run(
decls,
"assert property (@(posedge clk) q(19));",
&sigs,
&[0],
);
assert_eq!(ran.attempts[0].ends(), BTreeSet::from([1]));
let ran = local_run(
decls,
"assert property (@(posedge clk) q(18));",
&sigs,
&[0],
);
assert!(ran.attempts[0].matches.is_empty());
}
#[test]
fn t13_declared_initialisers_run_in_declaration_order() {
let decls = "sequence w; int v = data + 1, t = v + 1; int u; (a, u = v) ##1 (u + 1 == t); endsequence";
let stmt = "assert property (@(posedge clk) w);";
let sigs: [(&str, &[i64]); 2] = [("a", &[1, 0]), ("data", &[4, 0])];
let ran = local_run(decls, stmt, &sigs, &[0]);
assert_eq!(ran.attempts[0].ends(), BTreeSet::from([1]));
with_assertion(&lv(decls), stmt, false, |r, _, _| {
let (au, leaves) = r.unwrap();
let writes = init_writes(&au);
assert_eq!(writes.len(), 2);
let reads: Vec<LocalVarId> = leaves
.locals_of(writes[1].1)
.reads
.iter()
.map(|(_, s)| *s)
.collect();
assert_eq!(reads, [writes[0].0]);
});
}
#[test]
fn t13_an_output_formal_flows_back_to_the_callers_variable() {
let decls = "sequence o(local output int q, local input logic [3:0] r);\n\
(a, q = r) ##1 b;\n\
endsequence\n\
sequence seven; int g; o(g, 4'd7) ##1 (g == 7); endsequence\n\
sequence eight; int g; o(g, 4'd7) ##1 (g == 8); endsequence";
let sigs: [(&str, &[i64]); 2] = [("a", &[1, 0, 0]), ("b", &[0, 1, 0])];
let ran = local_run(
decls,
"assert property (@(posedge clk) seven);",
&sigs,
&[0],
);
assert_eq!(ends_with(&ran, 0, "g"), BTreeSet::from([(2, Some(7))]));
let ran = local_run(
decls,
"assert property (@(posedge clk) eight);",
&sigs,
&[0],
);
assert!(ran.attempts[0].matches.is_empty());
}
#[test]
fn t13_sub_seq2_matches_like_seq2_inlined() {
let decls = "sequence sub_seq2(local inout int lv);\n\
(a ##1 !a, lv += data_in) ##1 !b[*0:$] ##1 b && (data_out == lv);\n\
endsequence\n\
sequence seq2; int v1; (c, v1 = data) ##1 sub_seq2(v1) ##1 (do1 == v1); endsequence\n\
sequence seq2_inlined;\n\
int v1, lv;\n\
(c, v1 = data) ##1\n\
((1, lv = v1) ##0 (a ##1 !a, lv += data_in)\n\
##1 (!b[*0:$] ##1 b && (data_out == lv), v1 = lv))\n\
##1 (do1 == v1);\n\
endsequence";
let (s2, inl) = (
"assert property (@(posedge clk) seq2);",
"assert property (@(posedge clk) seq2_inlined);",
);
let row = |data_out: i64, do1: i64| -> [(&'static str, Vec<i64>); 7] {
[
("a", vec![0, 1, 0, 0, 0, 0]),
("b", vec![0, 0, 0, 1, 0, 0]),
("c", vec![1, 0, 0, 0, 0, 0]),
("data", vec![3, 0, 0, 0, 0, 0]),
("data_in", vec![0, 0, 4, 0, 0, 0]),
("data_out", vec![0, 0, 0, data_out, 0, 0]),
("do1", vec![0, 0, 0, 0, do1, 0]),
]
};
for (data_out, do1, want) in [
(7, 7, Some(4)),
(7, 3, None), (3, 7, None), ] {
let r = row(data_out, do1);
let sigs: Vec<(&str, &[i64])> = r.iter().map(|(n, v)| (*n, v.as_slice())).collect();
for stmt in [s2, inl] {
let ran = local_run(decls, stmt, &sigs, &[0]);
assert_eq!(
ran.attempts[0].ends(),
want.into_iter().collect::<BTreeSet<u32>>(),
"{stmt} with data_out={data_out} do1={do1}"
);
}
}
let mut seed = 0x2545_f491_4f6c_dd1du64;
let mut next = move |m: u64| {
seed = seed
.wrapping_mul(6364136223846793005)
.wrapping_add(1442695040888963407);
((seed >> 33) % m) as i64
};
let build = |stmt: &str, f: &mut dyn FnMut(&ir::Automaton, &LeafTable<'_>)| {
with_assertion(&lv(decls), stmt, false, |r, _, _| {
let (au, leaves) = r.unwrap_or_else(|e| panic!("`{stmt}` failed to build: {e}"));
f(&au, &leaves);
});
};
let traces: Vec<Vec<(&str, Vec<i64>)>> = (0..4000)
.map(|_| {
[
("a", 2),
("b", 2),
("c", 2),
("data", 2),
("data_in", 2),
("data_out", 3),
("do1", 3),
]
.iter()
.map(|&(name, m)| (name, (0..8).map(|_| next(m)).collect()))
.collect()
})
.collect();
let starts: Vec<u32> = (0..8).collect();
let mut ends: Vec<Vec<BTreeSet<u32>>> = Vec::new();
for stmt in [s2, inl] {
let mut per_trace = Vec::new();
build(stmt, &mut |au, leaves| {
for rows in &traces {
let sigs: Vec<(&str, &[i64])> =
rows.iter().map(|(n, v)| (*n, v.as_slice())).collect();
for at in attempts_on(au, leaves, &sigs, &starts) {
per_trace.push(at.ends());
}
}
});
ends.push(per_trace);
}
assert_eq!(ends[0], ends[1], "seq2 and seq2_inlined disagree");
let matched = ends[0].iter().filter(|e| !e.is_empty()).count();
assert!(
matched >= 100,
"only {matched} attempts matched; the sweep is vacuous"
);
}
#[test]
fn t13_and_operands_own_their_copies_and_the_difference_flows_out() {
let decls = "sequence s; int x = 5; (((a, x = 9) ##1 b) and (c ##1 (x == 5))) ##1 (x == 9); endsequence";
let sigs: [(&str, &[i64]); 3] = [("a", &[1, 0, 0]), ("b", &[0, 1, 0]), ("c", &[1, 0, 0])];
let ran = local_run(decls, "assert property (@(posedge clk) s);", &sigs, &[0]);
assert_eq!(ends_with(&ran, 0, "x"), BTreeSet::from([(2, Some(9))]));
}
#[test]
fn t13_a_variable_only_the_second_and_operand_assigns_is_copied_out() {
let decls = "sequence s; int x, y = 0; ((a ##1 (b, x = data) ##0 (y == 0)) and (c ##1 (d, y = data1))) ##1 (x == 1 && y == 2); endsequence";
let sigs = |data1: i64| -> [(&'static str, Vec<i64>); 6] {
[
("a", vec![1, 0, 0]),
("b", vec![0, 1, 0]),
("c", vec![1, 0, 0]),
("d", vec![0, 1, 0]),
("data", vec![0, 1, 0]),
("data1", vec![0, data1, 0]),
]
};
let r = sigs(2);
let view: Vec<(&str, &[i64])> = r.iter().map(|(n, v)| (*n, v.as_slice())).collect();
let ran = local_run(decls, "assert property (@(posedge clk) s);", &view, &[0]);
assert_eq!(ran.attempts[0].ends(), BTreeSet::from([2]));
let r = sigs(3);
let view: Vec<(&str, &[i64])> = r.iter().map(|(n, v)| (*n, v.as_slice())).collect();
let ran = local_run(decls, "assert property (@(posedge clk) s);", &view, &[0]);
assert!(ran.attempts[0].matches.is_empty());
}
#[test]
fn t13_or_flows_the_value_of_the_matching_branch() {
let decls = "sequence s; int x; ((a ##1 (b, x = data)) or (c ##1 (d, x = data1))) ##1 (x == 5); endsequence";
let first: [(&str, &[i64]); 6] = [
("a", &[1, 0, 0]),
("b", &[0, 1, 0]),
("c", &[0, 0, 0]),
("d", &[0, 0, 0]),
("data", &[0, 5, 0]),
("data1", &[0, 9, 0]),
];
let ran = local_run(decls, "assert property (@(posedge clk) s);", &first, &[0]);
assert_eq!(ran.attempts[0].ends(), BTreeSet::from([2]));
let second: [(&str, &[i64]); 6] = [
("a", &[0, 0, 0]),
("b", &[0, 0, 0]),
("c", &[1, 0, 0]),
("d", &[0, 1, 0]),
("data", &[0, 9, 0]),
("data1", &[0, 5, 0]),
];
let ran = local_run(decls, "assert property (@(posedge clk) s);", &second, &[0]);
assert_eq!(ran.attempts[0].ends(), BTreeSet::from([2]));
}
#[test]
fn t13_a_compound_match_item_accumulates() {
let decls =
"sequence s; int t = 1; (a, t += data) ##1 (b, t += data) ##1 (t == 8); endsequence";
let sigs: [(&str, &[i64]); 3] =
[("a", &[1, 0, 0]), ("b", &[0, 1, 0]), ("data", &[3, 4, 0])];
let ran = local_run(decls, "assert property (@(posedge clk) s);", &sigs, &[0]);
assert_eq!(ran.attempts[0].ends(), BTreeSet::from([2]));
}
#[test]
fn t13_a_repetition_flows_out_only_if_it_runs_at_least_once() {
builds(
&lv("sequence s; int v; ((a, v = data) ##1 b)[*1:$] ##1 (v == 1); endsequence"),
"assert property (@(posedge clk) s);",
)
.unwrap();
let e = built_err(
&lv("sequence s; int v; ((a, v = data) ##1 b)[*0:$] ##1 (v == 1); endsequence"),
"assert property (@(posedge clk) s);",
);
assert!(
e.message.contains("does not flow out") && e.message.contains("`v`"),
"{e}"
);
}
#[test]
fn t13_intersect_blocks_the_common_variable_and_flows_the_difference() {
let e = built_err(
&lv(
"sequence s; int x; ((a ##1 (b, x = data)) intersect (c ##1 (d, x = data1))) ##1 (x == 1); endsequence",
),
"assert property (@(posedge clk) s);",
);
assert!(
e.message.contains("does not flow out") && e.message.contains("`x`"),
"{e}"
);
builds(
&lv("sequence s; int x; ((a ##1 (b, x = data)) intersect (c ##1 d)) ##1 (x == 1); endsequence"),
"assert property (@(posedge clk) s);",
)
.unwrap();
}
#[test]
fn t13_an_output_formal_must_flow_out_of_its_body() {
let e = built_err_lenient(
&lv(
"sequence o(local output int q); (a, q = data) or (b ##1 c); endsequence\n\
sequence s; int g; o(g) ##1 (g == 1); endsequence",
),
"assert property (@(posedge clk) s);",
);
assert!(
e.message.contains("does not flow out") && e.message.contains("`q`"),
"{e}"
);
}
#[test]
fn t13_an_inout_instance_that_admits_an_empty_match_is_rejected() {
let e = built_err_lenient(
&lv(
"sequence o(local inout int q); (a ##1 b)[*0:1]; endsequence\n\
sequence s; int g = 0; o(g) ##1 b; endsequence",
),
"assert property (@(posedge clk) s);",
);
assert!(e.message.contains("empty match"), "{e}");
}
#[test]
fn t13_one_local_bound_to_two_output_formals_is_rejected() {
let e = built_err_lenient(
&lv("sequence o(local output int p, local output int q);\n\
(a, p = data, q = data) ##1 b;\n\
endsequence\n\
sequence s; int g; o(g, g) ##1 (g == 1); endsequence"),
"assert property (@(posedge clk) s);",
);
assert!(
e.message.contains("`g`")
&& e.message.contains("two or more")
&& e.message.contains("16.8.2"),
"{e}"
);
let e = built_err_lenient(
&lv("sequence o(local inout int p, local output int q);\n\
(a, p = data, q = data) ##1 b;\n\
endsequence\n\
sequence s; int g = 0; o(g, g) ##1 (g == 1); endsequence"),
"assert property (@(posedge clk) s);",
);
assert!(
e.message.contains("`g`") && e.message.contains("two or more"),
"{e}"
);
}
#[test]
fn t13_distinct_or_per_instance_output_bindings_build() {
builds(
&lv("sequence o(local output int p, local output int q);\n\
(a, p = data, q = data) ##1 b;\n\
endsequence\n\
sequence s; int g, h; o(g, h) ##1 (g == 1); endsequence"),
"assert property (@(posedge clk) s);",
)
.unwrap();
builds(
&lv(
"sequence o(local output int p); (a, p = data) ##1 b; endsequence\n\
sequence s; int g; o(g) ##1 o(g) ##1 (g == 1); endsequence",
),
"assert property (@(posedge clk) s);",
)
.unwrap();
}
#[test]
fn t13_a_read_of_an_unassigned_local_is_rejected() {
let e = built_err_lenient(
&lv("sequence s; int v; a ##1 (v == 1); endsequence"),
"assert property (@(posedge clk) s);",
);
assert!(
e.message.contains("does not flow out") && e.message.contains("`v`"),
"{e}"
);
let e = built_err_lenient(
&lv(
"sequence o(local input int f); a ##1 (f == 1); endsequence\n\
sequence s; int g; o(g); endsequence",
),
"assert property (@(posedge clk) s);",
);
assert!(
e.message.contains("does not flow out") && e.message.contains("`g`"),
"{e}"
);
}
#[test]
fn t13_a_wide_local_variable_has_a_slot_and_a_leaf_per_limb() {
with_assertion(
&lv("sequence s; logic [99:0] v = 0; a ##1 (v == 0); endsequence"),
"assert property (@(posedge clk) s);",
false,
|r, _, _| {
let (au, leaves) = r.unwrap();
assert_eq!(au.local_vars.len(), 4, "100 bits = 2 limbs = 4 slots");
assert_eq!(au.local_vars[0].width, 100);
let mut writes = Vec::new();
for e in au.states.iter().flat_map(|s| &s.edges) {
if let Transition::LocalVarWrite { var, value } = &e.label {
writes.push((var.0, leaves.limb_of(*value), value.0));
}
}
let group = writes[0].2;
let sel = |unknown, index| {
Some(LimbSel {
width: 100,
unknown,
index,
group,
})
};
assert_eq!(
writes.iter().map(|w| (w.0, w.1)).collect::<Vec<_>>(),
[
(0, sel(false, 0)),
(1, sel(false, 1)),
(2, sel(true, 0)),
(3, sel(true, 1))
]
);
},
);
}
#[test]
fn t13_a_wide_self_assignment_goes_through_a_temporary() {
with_assertion(
&lv(
"sequence s; logic [99:0] v = 0; (a, v = {v[98:0], 1'b1}) ##1 (v != 0); \
endsequence",
),
"assert property (@(posedge clk) s);",
false,
|r, _, _| {
let (au, _) = r.unwrap();
assert_eq!(au.local_vars.len(), 8, "v and its temporary");
let copies: Vec<_> = au
.states
.iter()
.flat_map(|s| &s.edges)
.filter_map(|e| match &e.label {
Transition::LocalVarCopy { dst, src } => Some((dst.0, src.0)),
_ => None,
})
.collect();
assert_eq!(copies, [(0, 4)], "the temporary is copied back to `v`");
},
);
with_assertion(
&lv("sequence s; int v = 0; (a, v = v + 1) ##1 (v != 0); endsequence"),
"assert property (@(posedge clk) s);",
false,
|r, _, _| {
let (au, _) = r.unwrap();
assert_eq!(au.local_vars.len(), 1);
},
);
}
#[test]
fn t13_an_unrepresentable_local_variable_is_a_loud_error() {
let e = built_err(
&lv("sequence s; logic [1999999:0] v = 0; a ##1 (v == 0); endsequence"),
"assert property (@(posedge clk) s);",
);
assert!(e.message.contains("1048576"), "{e}");
}
#[test]
fn t13_a_match_item_must_assign_a_local_variable() {
let e = built_err_lenient(
&lv("sequence s; (a, n = 1) ##1 b; endsequence"),
"assert property (@(posedge clk) s);",
);
assert!(e.message.contains("local variable"), "{e}");
}
#[test]
fn t13_every_instance_gets_its_own_variables() {
let decls = "sequence s(local input int f); int v = f; a ##1 (v == f); endsequence";
with_assertion(
&lv(decls),
"assert property (@(posedge clk) s(1) ##1 s(2));",
false,
|r, _, _| {
let (au, _) = r.unwrap();
assert_eq!(au.local_vars.len(), 4, "f and v, once per instance");
},
);
}
const S: &str = "assert property (@(posedge clk) s);";
#[test]
fn t14_a_match_item_on_a_subsequence_that_admits_an_empty_match_is_illegal() {
let e = built_err_lenient(
&lv("sequence s;\n\
int x;\n\
a ##1 (b[*0:1], x = e) ##1 c[*2]; // illegal\n\
endsequence"),
S,
);
assert!(
e.message.contains("empty match") && e.message.contains("16.11"),
"{e}"
);
}
#[test]
fn t14_a_match_item_on_a_concatenation_that_cannot_be_empty_is_legal() {
builds(
&lv("sequence s;\n\
int x;\n\
(a ##1 b[*0:1], x = e) ##1 c[*2]; // legal\n\
endsequence"),
S,
)
.unwrap();
}
#[test]
fn t14_every_kind_of_match_item_needs_a_nonempty_subsequence() {
for item in [
"x++",
"--x",
"x = 1",
"x += 1",
"$display(\"%d\", x)",
"tk(x)",
] {
let e = built_err_lenient(
&lv(&format!(
"task tk(int v); endtask\n\
sequence s; int x = 0; a ##1 (b[*0:1], {item}) ##1 c; endsequence"
)),
S,
);
assert!(e.message.contains("empty match"), "`{item}`: {e}");
}
let e = built_err_lenient(
&lv("sequence s; int x = 0; a ##1 (b[*0:1], x++)[*2] ##1 c; endsequence"),
S,
);
assert!(e.message.contains("empty match"), "{e}");
}
#[test]
fn t14_increment_and_decrement_update_the_local_variable() {
let sig: [(&str, &[i64]); 2] = [("a", &[1, 0, 0]), ("b", &[0, 1, 0])];
let up = local_run(
"sequence s; int x; (a, x = 10) ##1 (b, x++, x++, x++, --x) ##1 (x == 12); endsequence",
S,
&sig,
&[0],
);
assert_eq!(ends_with(&up, 0, "x"), BTreeSet::from([(2, Some(12))]));
let down = local_run(
"sequence s; int x; (a, x = 10) ##1 (b, x--, x--, ++x) ##1 (x == 9); endsequence",
S,
&sig,
&[0],
);
assert_eq!(ends_with(&down, 0, "x"), BTreeSet::from([(2, Some(9))]));
let wrap = local_run(
"sequence s; bit [1:0] y; (a, y = 3) ##1 (b, y++) ##1 (y == 0); endsequence",
S,
&sig,
&[0],
);
assert_eq!(ends_with(&wrap, 0, "y"), BTreeSet::from([(2, Some(0))]));
}
#[test]
fn t14_increment_of_an_unassigned_local_variable_is_rejected() {
for item in ["x++", "x--", "++x", "--x"] {
let e = built_err(
&lv(&format!(
"sequence s; int x; (a, {item}) ##1 b; endsequence"
)),
S,
);
assert!(
e.message.contains("does not flow out") && e.message.contains("`x`"),
"`{item}`: {e}"
);
}
}
#[test]
fn t14_increment_must_name_a_local_variable() {
let e = built_err_lenient(&lv("sequence s; (a, n++) ##1 b; endsequence"), S);
assert!(e.message.contains("local variable"), "{e}");
}
#[test]
fn t14_rep_v_accumulates_over_a_repetition() {
let decls = "sequence s;\n\
int x = 0;\n\
(a[->1], x += data)[*4] ##1 b ##1 c && (data_out == x);\n\
endsequence";
let row = |v: &[i64]| -> Vec<i64> { v.to_vec() };
let run = |out: i64| {
let (a, b, c) = (
row(&[1, 1, 1, 1, 0, 0]),
row(&[0, 0, 0, 0, 1, 0]),
row(&[0, 0, 0, 0, 0, 1]),
);
let (data, data_out) = (row(&[1, 2, 3, 4, 0, 0]), row(&[0, 0, 0, 0, 0, out]));
local_run(
decls,
S,
&[
("a", &a),
("b", &b),
("c", &c),
("data", &data),
("data_out", &data_out),
],
&[0],
)
};
assert_eq!(ends_with(&run(10), 0, "x"), BTreeSet::from([(5, Some(10))]));
assert!(run(9).attempts[0].matches.is_empty());
}
#[test]
fn t14_count_a_cycles_counts_with_an_increment() {
let decls = "parameter MAX = 3;\n\
sequence s;\n\
int x;\n\
(a, x = 1)\n\
##1 (a, x++)[*0:$]\n\
##1 !a && (x <= MAX);\n\
endsequence";
let run = |max: i64| local_run(decls, S, &[("a", &[1, 1, 1, 0]), ("MAX", &[max; 4])], &[0]);
assert_eq!(ends_with(&run(3), 0, "x"), BTreeSet::from([(3, Some(3))]));
assert!(run(2).attempts[0].matches.is_empty());
}
#[test]
fn t14_count_a_cycles_verbatim_builds() {
builds(
&lv("parameter MAX = 3;\n\
sequence s;\n\
int x;\n\
($rose(a), x = 1)\n\
##1 (a, x++)[*0:$]\n\
##1 !a && (x <= MAX);\n\
endsequence"),
S,
)
.unwrap();
}
#[test]
fn t14_first_match_with_a_match_item() {
let sig: [(&str, &[i64]); 3] = [
("a", &[1, 0, 0, 0]),
("b", &[0, 1, 1, 0]),
("data", &[0, 5, 7, 0]),
];
let seq = |fm: &str, want: i64| {
local_run(
&format!("sequence s; int x; {fm} ##1 (x == {want}); endsequence"),
S,
&sig,
&[0],
)
};
for fm in [
"first_match(a ##[1:2] b, x = data)",
"first_match((a ##[1:2] b, x = data))",
] {
assert_eq!(
ends_with(&seq(fm, 5), 0, "x"),
BTreeSet::from([(2, Some(5))]),
"{fm}"
);
assert!(seq(fm, 7).attempts[0].matches.is_empty(), "{fm}");
}
let all = seq("(a ##[1:2] b, x = data)", 7);
assert_eq!(ends_with(&all, 0, "x"), BTreeSet::from([(3, Some(7))]));
}
#[test]
fn t14_first_match_match_item_needs_a_nonempty_sequence() {
let e = built_err_lenient(
&lv("sequence s; int x; first_match(a[*0:1], x = data) ##1 b; endsequence"),
S,
);
assert!(e.message.contains("empty match"), "{e}");
}
#[test]
fn t14_first_match_calls_fire_at_every_end_point_whichever_way_it_is_written() {
let sigs: [(&str, &[i64]); 3] = [
("a", &[1, 0, 0, 0]),
("b", &[0, 1, 1, 0]),
("data", &[0, 5, 7, 0]),
];
type Calls = BTreeSet<(u32, Vec<Option<i64>>)>;
let calls_of = |body: &str| -> (Calls, BTreeSet<u32>) {
call_run(
&format!("task tk(int n); endtask\nsequence s; {body}; endsequence"),
&sigs,
|leaves, got| {
assert_eq!(leaves.call_count(), 1, "`{body}`");
(
got.calls.iter().map(|c| (c.tick, c.args.clone())).collect(),
got.attempt.ends(),
)
},
)
};
let both = BTreeSet::from([(1, vec![Some(5)]), (2, vec![Some(7)])]);
let (plain, plain_ends) = calls_of("(a ##[1:2] b, tk(data))");
assert_eq!(plain, both);
assert_eq!(plain_ends, BTreeSet::from([1, 2]));
for fm in [
"first_match(a ##[1:2] b, tk(data))",
"first_match((a ##[1:2] b, tk(data)))",
] {
let (calls, ends) = calls_of(fm);
assert_eq!(calls, both, "{fm}: the call fires at both end points");
assert_eq!(ends, BTreeSet::from([1]), "{fm}");
}
}
#[test]
fn t14_first_match_mixed_items_run_in_list_order() {
let sigs: [(&str, &[i64]); 3] = [
("a", &[1, 0, 0, 0]),
("b", &[0, 1, 1, 0]),
("data", &[0, 5, 7, 0]),
];
call_run(
"task tk(int n); endtask\n\
sequence s; int x; first_match(a ##[1:2] b, x = data, tk(x), x++) ##1 (x == 6); endsequence",
&sigs,
|_, got| {
let calls: Vec<_> = got.calls.iter().map(|c| (c.tick, c.args.clone())).collect();
assert_eq!(calls, vec![(1, vec![Some(5)]), (2, vec![Some(7)])]);
assert_eq!(got.attempt.ends(), BTreeSet::from([2]));
},
);
}
#[test]
fn t14_first_match_items_are_validated_when_the_operand_never_matches() {
for item in ["x++", "x += 1"] {
let e = built_err_lenient(
&lv(&format!(
"sequence s; int x; first_match((a ##1 b) intersect (a ##2 b), {item}); \
endsequence"
)),
S,
);
assert!(
e.message.contains("does not flow out") && e.message.contains("`x`"),
"`{item}`: {e}"
);
}
}
#[test]
fn t14_s1_from_16_11_builds() {
builds(
&lv("logic f;\n\
sequence s;\n\
logic v, w;\n\
(a, v = e) ##1\n\
(b[->1], w = f, $display(\"b after a with v = %h, w = %h\\n\", v, w));\n\
endsequence"),
S,
)
.unwrap();
}
#[test]
fn t14_a_non_void_function_is_not_a_match_item() {
let e = built_err_lenient(
&lv("function int fn(int v); return v; endfunction\n\
sequence s; int x; (a, x = 1) ##1 (b, fn(x)); endsequence"),
S,
);
assert!(e.message.contains("void"), "{e}");
}
#[test]
fn t14_output_and_inout_formals_are_rejected() {
for dir in ["output", "inout"] {
let e = built_err_lenient(
&lv(&format!(
"task tk({dir} int o); endtask\n\
sequence s; (a, tk(data)) ##1 b; endsequence"
)),
S,
);
assert!(e.message.contains(dir), "{dir}: {e}");
}
}
#[test]
fn t14_a_local_variable_cannot_be_passed_by_reference() {
let e = built_err_lenient(
&lv("task tk(ref int r); endtask\n\
sequence s; int x; (a, x = 1) ##1 (b, tk(x)); endsequence"),
S,
);
assert!(
e.message.contains("local variable") && e.message.contains("by value"),
"{e}"
);
}
#[test]
fn t14_input_ref_and_const_ref_arguments_are_legal() {
for call in [
"tk(data, 1)",
"tk(.n(data), .m(2))",
"tk(x, x + 1)",
"tk(data)",
] {
builds(
&lv(&format!(
"task tk(int n, int m = 0); endtask\n\
sequence s; int x = 1; (a, {call}) ##1 b; endsequence"
)),
S,
)
.unwrap_or_else(|e| panic!("`{call}`: {e}"));
}
for decl in ["task tk(ref int r);", "task tk(const ref int r);"] {
builds(
&lv(&format!(
"{decl} endtask\nsequence s; (a, tk(data)) ##1 b; endsequence"
)),
S,
)
.unwrap_or_else(|e| panic!("`{decl}`: {e}"));
}
}
fn call_run<R>(
decls: &str,
signals: &[(&str, &[i64])],
f: impl FnOnce(&LeafTable<'_>, &trace::CallAttempt) -> R,
) -> R {
with_assertion(&lv(decls), S, false, |r, _, _| {
let (au, leaves) = r.unwrap_or_else(|e| panic!("failed to build: {e}"));
let len = signals[0].1.len() as u32;
let sig = |name: &str, t: u32| -> i64 {
signals
.iter()
.find(|(n, _)| *n == name)
.unwrap_or_else(|| panic!("the trace has no signal `{name}`"))
.1[t as usize]
};
let got = trace::attempt_with_calls(&au, 0, len, &|id, tick, frame| {
eval_leaf_id(&leaves, id, frame, tick, &sig)
})
.unwrap_or_else(|e| panic!("trace interpreter: {e}"));
f(&leaves, &got)
})
}
#[test]
fn t14_calls_and_writes_run_in_list_order() {
let sigs: [(&str, &[i64]); 3] = [("a", &[1, 0, 0]), ("b", &[0, 1, 0]), ("c", &[0, 0, 1])];
call_run(
"task tk(int n); endtask\n\
sequence s; int x; (a, x = 1) ##1 (b, tk(x), x = 5, tk(x)) ##1 c; endsequence",
&sigs,
|leaves, got| {
assert_eq!(leaves.call_count(), 2);
let calls: Vec<_> = got
.calls
.iter()
.map(|c| (c.tick, c.call.0, c.args.clone()))
.collect();
assert_eq!(
calls,
vec![(1, 0, vec![Some(1)]), (1, 1, vec![Some(5)])],
"the first call sees x == 1, the second the x = 5 written between them"
);
assert_eq!(got.attempt.ends(), BTreeSet::from([2]));
},
);
}
#[test]
fn t14_a_call_fires_even_if_the_longer_sequence_fails() {
let sigs: [(&str, &[i64]); 3] = [("a", &[1, 0, 0]), ("b", &[0, 1, 0]), ("c", &[0, 0, 0])];
call_run(
"task tk(int n); endtask\n\
sequence s; int x; (a, x = 1) ##1 (b, tk(x)) ##1 c; endsequence",
&sigs,
|_, got| {
assert!(got.attempt.matches.is_empty());
assert_eq!(got.calls.len(), 1, "the call at tick 1 still fired");
},
);
}
#[test]
fn t14_the_call_table_records_how_each_argument_is_passed() {
call_run(
"task tk(int n, ref int r); endtask\n\
sequence s; (a, tk(data, data2)) ##1 b; endsequence",
&[("a", &[1, 0]), ("b", &[0, 1]), ("data", &[7, 0])],
|leaves, got| {
assert_eq!(leaves.call_count(), 1);
let site = leaves.call_site(ir::CallId(0));
assert_eq!(site.args.len(), 2);
assert!(matches!(site.args[0].0, ir::CallArg::Value(_)));
assert!(matches!(site.args[1].0, ir::CallArg::Ref));
let event = got.calls.iter().next().expect("the call fired");
assert_eq!(event.args, vec![Some(7), None], "ref has no sampled value");
},
);
}
#[test]
fn t14_a_call_inside_an_and_or_intersect_operand_is_a_loud_error() {
for op in ["and", "intersect"] {
let e = built_err(
&lv(&format!(
"task tk(int n); endtask\n\
sequence s; ((a, tk(data)) ##1 b) {op} (c ##1 d); endsequence"
)),
S,
);
assert!(
e.message.contains("SubroutineCall") && e.message.contains(op),
"{op}: {e}"
);
}
}
const EP: &str = "logic reset, inst, branch_back, ready, proc1, proc2, reset1, branch_back1, \
req, w;\n";
fn ep(decls: &str) -> String {
format!("{EP}{}", lv(decls))
}
fn clock_run<R>(
decls: &str,
stmt: &str,
(dest, source): (&[u64], &[u64]),
sigs: &[(&str, &[i64])],
starts: &[u32],
f: impl FnOnce(&ir::Automaton, &LeafTable<'_>, Vec<trace::CallAttempt>) -> R,
) -> R {
with_assertion(&ep(decls), stmt, false, |r, _, _| {
let (au, leaves) = r.unwrap_or_else(|e| panic!("`{stmt}` failed to build: {e}"));
let sig = |name: &str, t: u32| -> i64 {
sigs.iter()
.find(|(n, _)| *n == name)
.unwrap_or_else(|| panic!("the trace has no signal `{name}`"))
.1[t as usize]
};
let clocks = trace::TraceClocks {
dest: dest.to_vec(),
source: source.to_vec(),
};
let got = starts
.iter()
.map(|&s| {
trace::attempt_with_clocks(&au, s, &clocks, &|id, tick, frame| {
eval_leaf_id(&leaves, id, frame, tick, &sig)
})
.unwrap_or_else(|e| panic!("trace interpreter: {e}"))
})
.collect();
f(&au, &leaves, got)
})
}
fn one_clock(n: u64) -> Vec<u64> {
(0..n).map(|t| (t + 1) * 10).collect()
}
fn ends_of(got: &[trace::CallAttempt]) -> Vec<BTreeSet<u32>> {
got.iter().map(|g| g.attempt.ends()).collect()
}
#[test]
fn t15_an_empty_match_never_fires_triggered() {
let decls = "sequence zero_or_one_req; (req==1'b1)[*0:1]; endsequence";
let stmt = "assert property (@(posedge clk) a ##1 zero_or_one_req.triggered);";
let t = one_clock(5);
let sigs: [(&str, &[i64]); 2] = [("a", &[1, 1, 1, 1, 1]), ("req", &[0, 1, 0, 1, 0])];
clock_run(
decls,
stmt,
(&t, &t),
&sigs,
&[0, 1, 2, 3],
|au, leaves, got| {
assert_eq!(au.end_points.len(), 1);
assert!(
au.end_point(ir::EndPointId(0)).automaton.admits_empty,
"the instance admits the empty match; that is the point of the test"
);
assert_eq!(leaves.end_site_count(), 1);
assert_eq!(
ends_of(&got),
vec![
BTreeSet::from([1]),
BTreeSet::new(),
BTreeSet::from([3]),
BTreeSet::new()
]
);
},
);
}
#[test]
fn t15_e1_e2_from_16_13_6_build_one_triggered_end_point() {
let decls = "sequence e1;\n\
@(posedge sysclk) $rose(a) ##1 b ##1 c;\n\
endsequence\n\
sequence e2;\n\
@(posedge sysclk) reset ##1 inst ##1 e1.triggered ##1 branch_back;\n\
endsequence";
with_assertion(&ep(decls), "assert property (e2);", false, |r, _, _| {
let (au, leaves) = r.unwrap();
assert_eq!(au.end_points.len(), 1);
let point = au.end_point(ir::EndPointId(0));
assert_eq!(point.method, ir::EndMethod::Triggered);
assert_eq!(point.site, 0);
assert!(point.flow_out.is_empty());
assert_eq!(leaves.end_site(0).method, ir::EndMethod::Triggered);
assert!(leaves.end_site(0).clock.is_some(), "e1 has its own clock");
});
}
#[test]
fn t15_triggered_tests_the_end_point_and_not_the_start() {
let decls = "sequence e1x; @(posedge sysclk) a ##1 b ##1 c; endsequence\n\
sequence e2x;\n\
@(posedge sysclk) reset ##1 inst ##1 e1x.triggered ##1 branch_back;\n\
endsequence\n\
sequence e2i;\n\
@(posedge sysclk) reset ##1 inst ##1 e1x ##1 branch_back;\n\
endsequence";
let t = one_clock(8);
let sigs: [(&str, &[i64]); 6] = [
("reset", &[1, 0, 0, 0, 0, 0, 0, 0]),
("inst", &[0, 1, 0, 0, 0, 0, 0, 0]),
("a", &[1, 0, 0, 0, 0, 0, 0, 0]),
("b", &[0, 1, 0, 0, 0, 0, 0, 0]),
("c", &[0, 0, 1, 0, 0, 0, 0, 0]),
("branch_back", &[0, 0, 0, 1, 0, 0, 0, 0]),
];
clock_run(
decls,
"assert property (e2x);",
(&t, &t),
&sigs,
&[0],
|_, _, got| {
assert_eq!(ends_of(&got), vec![BTreeSet::from([3])]);
},
);
clock_run(
decls,
"assert property (e2i);",
(&t, &t),
&sigs,
&[0],
|_, _, got| {
assert_eq!(ends_of(&got), vec![BTreeSet::new()]);
},
);
let mut c_low = sigs.to_vec();
c_low[4] = ("c", &[0, 0, 0, 0, 0, 0, 0, 0]);
clock_run(
decls,
"assert property (e2x);",
(&t, &t),
&c_low,
&[0],
|_, _, got| {
assert_eq!(ends_of(&got), vec![BTreeSet::new()]);
},
);
}
#[test]
fn t15_triggered_on_an_instance_with_arguments_and_through_a_name() {
let decls = "sequence e2p(p,q,r); @(posedge sysclk) p ##1 q ##1 r; endsequence\n\
sequence rule2;\n\
@(posedge sysclk) reset ##1 inst ##1 e2p(ready,proc1,proc2).triggered\n\
##1 branch_back;\n\
endsequence\n\
sequence e2_instantiated; e2p(ready,proc1,proc2); endsequence\n\
sequence rule2a;\n\
@(posedge sysclk) reset ##1 inst ##1 e2_instantiated.triggered ##1 branch_back;\n\
endsequence";
let t = one_clock(6);
let sigs: [(&str, &[i64]); 6] = [
("reset", &[1, 0, 0, 0, 0, 0]),
("inst", &[0, 1, 0, 0, 0, 0]),
("ready", &[1, 0, 0, 0, 0, 0]),
("proc1", &[0, 1, 0, 0, 0, 0]),
("proc2", &[0, 0, 1, 0, 0, 0]),
("branch_back", &[0, 0, 0, 1, 0, 0]),
];
for rule in ["rule2", "rule2a"] {
let stmt = format!("assert property ({rule});");
clock_run(decls, &stmt, (&t, &t), &sigs, &[0], |_, _, got| {
assert_eq!(ends_of(&got), vec![BTreeSet::from([3])], "{rule}");
});
}
}
#[test]
fn t15_triggered_on_a_sequence_formal_argument() {
let decls = "sequence e3f(sequence s, untyped t);\n\
@(posedge sysclk) s.triggered ##1 t;\n\
endsequence\n\
sequence rule3;\n\
@(posedge sysclk) reset ##1 e3f(ready ##1 proc1, proc2) ##1 branch_back;\n\
endsequence";
let t = one_clock(5);
let sigs: [(&str, &[i64]); 5] = [
("reset", &[1, 0, 0, 0, 0]),
("ready", &[1, 0, 0, 0, 0]),
("proc1", &[0, 1, 0, 0, 0]),
("proc2", &[0, 0, 1, 0, 0]),
("branch_back", &[0, 0, 0, 1, 0]),
];
clock_run(
decls,
"assert property (rule3);",
(&t, &t),
&sigs,
&[0],
|au, _, got| {
assert_eq!(au.end_points.len(), 1);
assert_eq!(ends_of(&got), vec![BTreeSet::from([3])]);
},
);
}
#[test]
fn t15_e2_with_arg_and_e4_from_16_13_6() {
let decls = "sequence e2_with_arg(sequence subseq);\n\
@(posedge sysclk) reset ##1 inst ##1 subseq.triggered ##1 branch_back;\n\
endsequence\n\
sequence e4;\n\
e2_with_arg(@(posedge sysclk) a ##1 b ##1 c);\n\
endsequence";
let t = one_clock(8);
let sigs: [(&str, &[i64]); 6] = [
("reset", &[1, 0, 0, 0, 0, 0, 0, 0]),
("inst", &[0, 1, 0, 0, 0, 0, 0, 0]),
("a", &[1, 0, 0, 0, 0, 0, 0, 0]),
("b", &[0, 1, 0, 0, 0, 0, 0, 0]),
("c", &[0, 0, 1, 0, 0, 0, 0, 0]),
("branch_back", &[0, 0, 0, 1, 0, 0, 0, 0]),
];
clock_run(
decls,
"assert property (e4);",
(&t, &t),
&sigs,
&[0],
|au, leaves, got| {
assert_eq!(au.end_points.len(), 1);
assert!(leaves.end_site(0).clock.is_some());
assert_eq!(ends_of(&got), vec![BTreeSet::from([3])]);
},
);
}
#[test]
fn t15_matched_synchronises_two_clocks_and_triggered_does_not() {
let decls = "sequence e1x; @(posedge sysclk) a ##1 b ##1 c; endsequence\n\
sequence e3m; @(posedge clk) reset1 ##1 e1x.matched ##1 branch_back1; endsequence\n\
sequence e3t; @(posedge clk) reset1 ##1 e1x.triggered ##1 branch_back1; endsequence";
let source: Vec<u64> = (0..9).map(|k| 5 + 10 * k).collect();
let dest: Vec<u64> = (1..=9).map(|k| 10 * k).collect();
let sigs: [(&str, &[i64]); 5] = [
("a", &[1, 0, 0, 0, 0, 0, 0, 0, 0]),
("b", &[0, 1, 0, 0, 0, 0, 0, 0, 0]),
("c", &[0, 0, 1, 0, 0, 0, 0, 0, 0]),
("reset1", &[0, 1, 0, 0, 0, 0, 0, 0, 0]),
("branch_back1", &[0, 0, 0, 1, 0, 0, 0, 0, 0]),
];
clock_run(
decls,
"assert property (e3m);",
(&dest, &source),
&sigs,
&[1],
|au, leaves, got| {
assert_eq!(
au.end_point(ir::EndPointId(0)).method,
ir::EndMethod::Matched
);
assert!(leaves.end_site(0).clock.is_some());
assert_eq!(ends_of(&got), vec![BTreeSet::from([3])]);
},
);
let mut late = sigs.to_vec();
late[3] = ("reset1", &[0, 0, 1, 0, 0, 0, 0, 0, 0]);
late[4] = ("branch_back1", &[0, 0, 0, 0, 1, 0, 0, 0, 0]);
clock_run(
decls,
"assert property (e3m);",
(&dest, &source),
&late,
&[2],
|_, _, got| {
assert_eq!(ends_of(&got), vec![BTreeSet::new()]);
},
);
let e = built_err(&ep(decls), "assert property (e3t);");
assert!(
e.message.contains("`.triggered`") && e.message.contains("different clock"),
"{e}"
);
}
#[test]
fn t15_matched_with_goto_repetition() {
let decls = "sequence e1p(p,q,r); @(posedge sysclk) p ##1 q ##1 r; endsequence\n\
sequence e2g;\n\
@(posedge clk) reset ##1 inst ##1 e1p(ready,proc1,proc2).matched [->1]\n\
##1 branch_back;\n\
endsequence";
let source: Vec<u64> = (0..9).map(|k| 5 + 10 * k).collect();
let dest: Vec<u64> = (1..=9).map(|k| 10 * k).collect();
let sigs: [(&str, &[i64]); 6] = [
("ready", &[1, 0, 0, 0, 0, 0, 0, 0, 0]),
("proc1", &[0, 1, 0, 0, 0, 0, 0, 0, 0]),
("proc2", &[0, 0, 1, 0, 0, 0, 0, 0, 0]),
("reset", &[1, 0, 0, 0, 0, 0, 0, 0, 0]),
("inst", &[0, 1, 0, 0, 0, 0, 0, 0, 0]),
("branch_back", &[0, 0, 0, 1, 0, 0, 0, 0, 0]),
];
clock_run(
decls,
"assert property (e2g);",
(&dest, &source),
&sigs,
&[0],
|au, _, got| {
assert_eq!(au.end_points.len(), 3);
assert_eq!(ends_of(&got), vec![BTreeSet::from([3])]);
},
);
}
#[test]
fn t15_matched_holds_on_one_destination_tick_per_match() {
let decls = "sequence e1x; @(posedge sysclk) a ##1 b; endsequence\n\
sequence mm; @(posedge clk) inst ##1 e1x.matched; endsequence";
let source: Vec<u64> = (0..9).map(|k| 5 + 10 * k).collect();
let dest: Vec<u64> = (1..=9).map(|k| 10 * k).collect();
let sigs: [(&str, &[i64]); 3] = [
("a", &[0, 0, 1, 0, 0, 0, 0, 0, 0]),
("b", &[0, 0, 0, 1, 0, 0, 0, 0, 0]),
("inst", &[1, 1, 1, 1, 1, 1, 1, 1, 1]),
];
let starts: Vec<u32> = (0..9).collect();
clock_run(
decls,
"assert property (mm);",
(&dest, &source),
&sigs,
&starts,
|_, _, got| {
let ends = ends_of(&got);
for (start, e) in ends.iter().enumerate() {
let want = if start == 2 {
BTreeSet::from([3])
} else {
BTreeSet::new()
};
assert_eq!(*e, want, "start {start}");
}
},
);
}
#[test]
fn t15_seq2a_a_local_flows_out_of_a_maximal_triggered() {
let decls = "sequence sub_seq2(lv);\n\
(a ##1 !a, lv = data_in) ##1 !b[*0:$] ##1 b && (data_out == lv);\n\
endsequence\n\
sequence seq2a;\n\
int v1; c ##1 sub_seq2(v1).triggered ##1 (do1 == v1);\n\
// v1 is now bound to lv\n\
endsequence";
let t = one_clock(4);
let sigs = |do1: i64| -> Vec<(&'static str, Vec<i64>)> {
vec![
("a", vec![1, 0, 0, 0]),
("b", vec![0, 0, 1, 0]),
("c", vec![0, 1, 0, 0]),
("data_in", vec![0, 5, 0, 0]),
("data_out", vec![0, 0, 5, 0]),
("do1", vec![0, 0, 0, do1]),
]
};
for (do1, want) in [(5, BTreeSet::from([3])), (6, BTreeSet::new())] {
let owned = sigs(do1);
let rows: Vec<(&str, &[i64])> = owned.iter().map(|(n, r)| (*n, r.as_slice())).collect();
clock_run(
decls,
"assert property (@(posedge clk) seq2a);",
(&t, &t),
&rows,
&[1],
|au, _, got| {
assert_eq!(au.end_points.len(), 1);
assert_eq!(
au.end_point(ir::EndPointId(0)).flow_out.len(),
1,
"v1 flows out"
);
assert_eq!(ends_of(&got), vec![want.clone()], "do1 = {do1}");
},
);
}
}
#[test]
fn t15_distinct_flow_out_valuations_fork_the_thread() {
let decls = "sequence two(lv); (a, lv = data_in) or (b, lv = data_out); endsequence\n\
sequence fk; int v1; c ##1 two(v1).triggered ##1 (do1 == v1); endsequence";
let t = one_clock(3);
for (do1, want) in [(3, true), (4, true), (9, false)] {
let sigs: [(&str, &[i64]); 6] = [
("a", &[0, 1, 0]),
("b", &[0, 1, 0]),
("c", &[1, 0, 0]),
("data_in", &[0, 3, 0]),
("data_out", &[0, 4, 0]),
("do1", &[0, 0, do1]),
];
clock_run(
decls,
"assert property (@(posedge clk) fk);",
(&t, &t),
&sigs,
&[0],
|_, _, got| {
let ends = ends_of(&got);
assert_eq!(
ends[0] == BTreeSet::from([2]),
want,
"do1 = {do1}: {ends:?}"
);
},
);
}
}
#[test]
fn t15_seq2b_a_negated_triggered_does_not_flow_a_local_out() {
let decls = "sequence sub_seq2(lv);\n\
(a ##1 !a, lv = data_in) ##1 !b[*0:$] ##1 b && (data_out == lv);\n\
endsequence\n\
sequence seq2b;\n\
int v1; c ##1 !sub_seq2(v1).triggered ##1 (do1 == v1); // v1 unassigned\n\
endsequence";
let e = built_err(&ep(decls), "assert property (@(posedge clk) seq2b);");
assert!(
e.message.contains("does not flow out") && e.message.contains("`v1`"),
"{e}"
);
}
#[test]
fn t15_a_local_input_or_inout_formal_is_an_error() {
for (dir, method) in [
("input", "triggered"),
("inout", "triggered"),
("input", "matched"),
] {
let decls = format!(
"sequence li(local {dir} int f); a ##1 (f == 1); endsequence\n\
sequence u; int k; c ##1 li(k).{method}; endsequence"
);
let e = built_err_lenient(&ep(&decls), "assert property (@(posedge clk) u);");
assert!(
e.message.contains(&format!("`.{method}`"))
&& e.message.contains("local variable formal"),
"{dir}/{method}: {e}"
);
}
}
#[test]
fn t15_an_application_inside_an_expression_is_a_flag_in_preorder() {
let decls = "sequence sa; a; endsequence\n\
sequence sb; b; endsequence";
let t = one_clock(2);
let sigs: [(&str, &[i64]); 3] = [("a", &[1, 0]), ("b", &[0, 1]), ("c", &[1, 1])];
clock_run(
decls,
"assert property (@(posedge clk) c ##1 (!sa.triggered && sb.triggered));",
(&t, &t),
&sigs,
&[0],
|au, leaves, got| {
assert_eq!(au.end_points.len(), 2);
assert_eq!(leaves.end_site_count(), 2);
assert_eq!(leaves.end_site(0).method, ir::EndMethod::Triggered);
let flagged: Vec<_> = (0..leaves.len() as u32)
.filter(|&i| !leaves.locals_of(LeafId(i)).end_flags.is_empty())
.collect();
assert_eq!(flagged.len(), 1);
assert_eq!(leaves.locals_of(LeafId(flagged[0])).end_flags.len(), 2);
assert_eq!(ends_of(&got), vec![BTreeSet::from([1])]);
},
);
clock_run(
decls,
"assert property (@(posedge clk) c ##1 (!sb.triggered && sa.triggered));",
(&t, &t),
&sigs,
&[0],
|_, _, got| {
assert_eq!(
ends_of(&got),
vec![BTreeSet::new()],
"!b && a is false at 1"
)
},
);
}
#[test]
fn t15_an_end_point_inside_a_product_operand() {
let decls = "sequence sc; c ##1 d; endsequence";
let t = one_clock(4);
let sigs: [(&str, &[i64]); 4] = [
("a", &[1, 1, 0, 0]),
("b", &[0, 0, 1, 0]),
("c", &[1, 0, 0, 0]),
("d", &[0, 1, 0, 0]),
];
for (op, want) in [
("and", BTreeSet::from([1])),
("intersect", BTreeSet::from([1])),
] {
let stmt =
format!("assert property (@(posedge clk) (a ##1 sc.triggered) {op} (a ##1 a));");
clock_run(decls, &stmt, (&t, &t), &sigs, &[0], |_, _, got| {
assert_eq!(ends_of(&got), vec![want.clone()], "{op}");
});
}
}
#[test]
fn t15_a_circular_triggered_dependency_is_an_error_not_a_loop() {
let decls = "sequence r1; a ##1 r2.triggered; endsequence\n\
sequence r2; b ##1 r1.triggered; endsequence";
let e = built_err_lenient(&ep(decls), "assert property (@(posedge clk) r1);");
assert!(e.message.contains("slang could not bind"), "{e}");
}
#[test]
fn t15_building_end_points_is_deterministic() {
let decls = ep("sequence e1x; @(posedge sysclk) a ##1 b; endsequence\n\
sequence e2x; @(posedge sysclk) reset ##1 e1x.triggered ##1 c; endsequence");
let render = || {
with_assertion(&decls, "assert property (e2x);", false, |r, _, _| {
let (au, _) = r.unwrap();
format!("{au:?}")
})
};
assert_eq!(render(), render());
}
const GCLK: &str = "logic sig; global clocking gc @(posedge sysclk); endclocking\n";
const S_WITH_MATCH_ITEM: &str =
"sequence s; bit v; (a, v = a) ##1 (b == v)[->1]; endsequence\n";
fn gclk_decls(more: &str) -> String {
format!("{GCLK}{more}")
}
fn uses_future(decls: &str, stmt: &str) -> Result<bool, String> {
with_assertion(decls, stmt, false, |r, _, _| {
r.map(|(_, leaves)| leaves.uses_future_gclk())
.map_err(|e| e.message)
})
}
#[test]
fn t18_future_functions_flag_the_table_and_past_ones_do_not() {
let decls = gclk_decls("");
for f in [
"$future_gclk",
"$rising_gclk",
"$falling_gclk",
"$steady_gclk",
"$changing_gclk",
] {
let stmt = format!("assert property (@(posedge clk) a ##1 {f}(b));");
assert_eq!(uses_future(&decls, &stmt), Ok(true), "{f}");
}
for f in [
"$past_gclk",
"$rose_gclk",
"$fell_gclk",
"$stable_gclk",
"$changed_gclk",
"$rose",
] {
let stmt = format!("assert property (@(posedge clk) a ##1 {f}(b));");
assert_eq!(uses_future(&decls, &stmt), Ok(false), "{f}");
}
assert_eq!(
uses_future(&decls, "assert property (@(posedge clk) a ##1 b);"),
Ok(false)
);
}
fn a2_rejection(decls: &str, stmt: &str) -> String {
let src = format!(
"module m;\nlogic clk, sysclk, a, b, c;\n{decls}\n\
always_ff @(posedge clk) begin\n{stmt}\nend\nendmodule\n"
);
let session = Session::new();
let mut comp = Compilation::new(&session).unwrap();
comp.add_source(&src).unwrap();
let design = comp.compile().unwrap();
assert!(
!design.diagnostics().has_errors(),
"fixture has compile errors:\n{}\n{src}",
design.diagnostics().rendered()
);
let m = design
.top_instances()
.next()
.unwrap()
.instance_body()
.unwrap();
let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
let proc = analysis.procedures(m).next().unwrap();
let Some(assertion) = analysis.assertions(proc.symbol()).next() else {
return analysis.diagnostics().rendered().to_string();
};
let tree = design.syntax_trees().into_iter().next().unwrap();
let root = assertion.root().as_assertion_expr().unwrap();
let (root, root_clock) = if root.kind() == AssertionExprKind::Clocking {
let kids = root.children();
(kids[1].as_assertion_expr().unwrap(), Some(kids[0]))
} else {
(root, None)
};
match build_automaton(root, root_clock, (&tree).into(), &m) {
Ok(_) => panic!("`{stmt}` was accepted"),
Err(e) => e.message,
}
}
#[test]
fn t18_a_future_function_with_sequence_match_items_is_rejected_by_name() {
let decls = gclk_decls(&format!(
"{S_WITH_MATCH_ITEM}\
sequence s2; bit v; (a ##1 $rising_gclk(c), v = 1); endsequence\n\
sequence s3; bit v; first_match(a ##1 b, v = 1); endsequence\n"
));
for stmt in [
"assert property (@(posedge clk) s |=> $future_gclk(c));",
"assert property (@(posedge clk) s ##1 $future_gclk(c));",
"assert property (@(posedge clk) s2 ##1 c);",
"assert property (@(posedge clk) s3 ##1 $steady_gclk(c));",
"assert property (@(posedge clk) c ##1 s ##1 $changing_gclk(c));",
] {
let msg = a2_rejection(&decls, stmt);
assert!(msg.contains("sequence match items"), "{stmt}: {msg}");
}
assert_eq!(
uses_future(&decls, "assert property (@(posedge clk) c ##1 s);"),
Ok(false)
);
assert_eq!(
uses_future(&decls, "assert property (@(posedge clk) s3 ##1 c);"),
Ok(false)
);
assert_eq!(
uses_future(
&decls,
"assert property (@(posedge clk) a ##1 $future_gclk(c));"
),
Ok(true)
);
}
#[test]
fn t18_nested_future_functions_are_rejected_by_slang_and_the_builder() {
let decls = gclk_decls("");
let stmt = "assert property (@(posedge clk) $future_gclk(a || $rising_gclk(b)));";
let (message, rendered) = with_assertion(&decls, stmt, true, |r, _, d| {
let Err(e) = r else {
panic!("nested future functions were accepted")
};
(e.message, d.rendered().to_string())
});
assert!(rendered.contains("may not be nested"), "{rendered}");
assert!(message.contains("shall not be nested"), "{message}");
}
const SIG: &[u8] = b"110000111000";
const CLK: &[u8] = b"110011001100";
fn gclk_fn(f: sv_sim_sim::sva::future::FutureFn, samples: &[u8], i: usize) -> bool {
sv_sim_sim::sva::future::eval_at(f, samples, i) == Some(b'1')
}
fn row_of(len: usize, f: impl Fn(usize) -> bool) -> String {
(0..len).map(|i| if f(i) { '1' } else { '0' }).collect()
}
fn gclk_ends(decls: &str, body: &str, rows: &[(&str, &str)], start: u32) -> BTreeSet<u32> {
let tr = Trace::new(rows);
let stmt = format!("assert property (@(posedge clk) {body});");
with_assertion(decls, &stmt, false, |r, tree, _| {
let (au, leaves) = r.unwrap_or_else(|e| panic!("`{body}` failed to build: {e}"));
let texts = leaf_texts(&leaves, tree);
run_attempt(&au, &texts, &tr, start).1
})
}
#[test]
fn t18_example_4_a4_and_a5_agree_on_every_attempt() {
use sv_sim_sim::sva::future::FutureFn;
let decls = gclk_decls("");
let n = SIG.len() - 1;
let stable = row_of(n + 1, |i| SIG[i] == if i > 0 { SIG[i - 1] } else { b'x' });
let steady = row_of(n + 1, |i| gclk_fn(FutureFn::Steady, SIG, i));
let rows = [
("$stable_gclk(sig)", stable.as_str()),
("$steady_gclk(sig)", steady.as_str()),
];
let (mut matched, mut failed) = (0, 0);
for start in 0..n as u32 {
let a4 = gclk_ends(&decls, "##1 $stable_gclk(sig)", &rows, start);
let a5 = gclk_ends(&decls, "$steady_gclk(sig)", &rows, start);
if a5.is_empty() {
assert!(a4.is_empty(), "attempt at tick {start}: {a4:?} vs {a5:?}");
failed += 1;
} else {
assert_eq!(a4, set(&[start + 1]), "attempt at tick {start}");
assert_eq!(a5, set(&[start]), "attempt at tick {start}");
matched += 1;
}
}
assert!(
matched > 0 && failed > 0,
"{matched} matched, {failed} failed"
);
assert!(gclk_ends(&decls, "$stable_gclk(sig)", &rows, 0).is_empty());
assert!(!gclk_ends(&decls, "$steady_gclk(sig)", &rows, 0).is_empty());
}
#[test]
fn t18_example_2_between_two_falling_edges_sig_may_change_only_at_a_fall() {
use sv_sim_sim::sva::future::FutureFn;
let decls = gclk_decls("");
let n = CLK.len() - 1;
let falling = |i: usize| gclk_fn(FutureFn::Falling, CLK, i);
let fall = row_of(n, falling);
let not_fall = row_of(n, |i| !falling(i));
let rows = [
("$falling_gclk(clk)", fall.as_str()),
("!$falling_gclk(clk)", not_fall.as_str()),
];
let body = "$falling_gclk(clk) ##1 (!$falling_gclk(clk))[*1:$]";
let ends: Vec<BTreeSet<u32>> = (0..n as u32)
.map(|s| gclk_ends(&decls, body, &rows, s))
.collect();
assert_eq!(ends[1], set(&[2, 3, 4]));
assert_eq!(ends[5], set(&[6, 7, 8]));
assert_eq!(ends[9], set(&[10]));
for (s, e) in ends.iter().enumerate() {
if ![1, 5, 9].contains(&s) {
assert!(e.is_empty(), "no attempt at tick {s} may match");
}
}
let violations: Vec<u32> = ends
.iter()
.flatten()
.copied()
.filter(|&e| !gclk_fn(FutureFn::Steady, SIG, e as usize))
.collect();
assert_eq!(violations, [8], "tick 8 is time 80");
}
}