Compare commits

...

10 commits

Author SHA1 Message Date
e3a2ccd41c
properly handle duplicate names in vcd 2025-01-09 22:52:22 -08:00
3771cea78e
Gather the FIFO debug ports in a bundle 2024-12-29 13:17:24 -03:00
dcf865caec
Add assertions and debug ports in order for the FIFO to pass induction
As some proofs involving memories, it is necessary to add more ports to
the queue interface, to sync state. These changes are predicated on the
test environment, so normal use is not affected.

Since some speedup is achieved, use the saved time to test with a deeper
FIFO.
2024-12-29 13:12:58 -03:00
31d01046a8
Initial queue formal proof based on one-entry FIFO equivalence
For now, only check that the basic properties work in bounded model check
mode, leave the induction proof for later.

Partially replace the previously existing proof.

Remove earlier assumptions and bounds that don't apply for this proof.

Use parameterized types instead of hard-coded types.
2024-12-29 13:04:01 -03:00
c16726cee6
fix #[hdl]/#[hdl_module] attributes getting the wrong hygiene when processing #[cfg]s 2024-12-29 00:48:15 -08:00
b63676d0ca
add test for cfgs 2024-12-28 23:39:50 -08:00
7005fa3330
implement handling #[cfg] and #[cfg_attr] in proc macro inputs 2024-12-28 23:39:08 -08:00
2ab8428062
upgrade syn version 2024-12-28 23:39:08 -08:00
9b06019bf5
make sim::Compiler not print things to stdout unless you ask for it 2024-12-18 21:15:09 -08:00
36bad52978
sim: fix sim.write to struct 2024-12-18 20:50:50 -08:00
16 changed files with 3809 additions and 249 deletions

8
Cargo.lock generated
View file

@ -543,9 +543,9 @@ dependencies = [
[[package]]
name = "proc-macro2"
version = "1.0.83"
version = "1.0.92"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b33eb56c327dec362a9e55b3ad14f9d2f0904fb5a5b03b513ab5465399e9f43"
checksum = "37d3544b3f2748c54e147655edb5025752e2303145b5aefb3c3ea2c78b973bb0"
dependencies = [
"unicode-ident",
]
@ -647,9 +647,9 @@ checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"
[[package]]
name = "syn"
version = "2.0.66"
version = "2.0.93"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c42f3f41a2de00b01c0aaad383c5a45241efc8b2d1eda5661812fda5f3cdcff5"
checksum = "9c786062daee0d6db1132800e623df74274a0a87322d8e183338e01b3d98d058"
dependencies = [
"proc-macro2",
"quote",

View file

@ -37,7 +37,7 @@ quote = "1.0.36"
serde = { version = "1.0.202", features = ["derive"] }
serde_json = { version = "1.0.117", features = ["preserve_order"] }
sha2 = "0.10.8"
syn = { version = "2.0.66", features = ["full", "fold", "visit", "extra-traits"] }
syn = { version = "2.0.93", features = ["full", "fold", "visit", "extra-traits"] }
tempfile = "3.10.1"
thiserror = "1.0.61"
trybuild = "1.0"

View file

@ -3,14 +3,20 @@
#![cfg_attr(test, recursion_limit = "512")]
use proc_macro2::{Span, TokenStream};
use quote::{quote, ToTokens};
use std::io::{ErrorKind, Write};
use std::{
collections::{hash_map::Entry, HashMap},
io::{ErrorKind, Write},
};
use syn::{
bracketed, parenthesized,
bracketed,
ext::IdentExt,
parenthesized,
parse::{Parse, ParseStream, Parser},
parse_quote,
punctuated::Pair,
punctuated::{Pair, Punctuated},
spanned::Spanned,
AttrStyle, Attribute, Error, Item, ItemFn, Token,
token::{Bracket, Paren},
AttrStyle, Attribute, Error, Ident, Item, ItemFn, LitBool, LitStr, Meta, Token,
};
mod fold;
@ -19,6 +25,7 @@ mod hdl_enum;
mod hdl_type_alias;
mod hdl_type_common;
mod module;
mod process_cfg;
pub(crate) trait CustomToken:
Copy
@ -59,6 +66,11 @@ mod kw {
};
}
custom_keyword!(__evaluated_cfgs);
custom_keyword!(all);
custom_keyword!(any);
custom_keyword!(cfg);
custom_keyword!(cfg_attr);
custom_keyword!(clock_domain);
custom_keyword!(connect_inexact);
custom_keyword!(custom_bounds);
@ -75,6 +87,7 @@ mod kw {
custom_keyword!(no_reset);
custom_keyword!(no_runtime_generics);
custom_keyword!(no_static);
custom_keyword!(not);
custom_keyword!(outline_generated);
custom_keyword!(output);
custom_keyword!(reg_builder);
@ -901,15 +914,346 @@ fn hdl_module_impl(item: ItemFn) -> syn::Result<TokenStream> {
Ok(contents)
}
pub fn hdl_module(attr: TokenStream, item: TokenStream) -> syn::Result<TokenStream> {
let kw = kw::hdl_module::default();
hdl_module_impl(syn::parse2(quote! { #[#kw(#attr)] #item })?)
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub(crate) enum CfgExpr {
Option {
ident: Ident,
value: Option<(Token![=], LitStr)>,
},
All {
all: kw::all,
paren: Paren,
exprs: Punctuated<CfgExpr, Token![,]>,
},
Any {
any: kw::any,
paren: Paren,
exprs: Punctuated<CfgExpr, Token![,]>,
},
Not {
not: kw::not,
paren: Paren,
expr: Box<CfgExpr>,
trailing_comma: Option<Token![,]>,
},
}
pub fn hdl_attr(attr: TokenStream, item: TokenStream) -> syn::Result<TokenStream> {
let kw = kw::hdl::default();
let item = quote! { #[#kw(#attr)] #item };
let item = syn::parse2::<Item>(item)?;
impl Parse for CfgExpr {
fn parse(input: ParseStream) -> syn::Result<Self> {
match input.cursor().ident() {
Some((_, cursor)) if cursor.eof() => {
return Ok(CfgExpr::Option {
ident: input.call(Ident::parse_any)?,
value: None,
});
}
_ => {}
}
if input.peek(Ident::peek_any) && input.peek2(Token![=]) {
return Ok(CfgExpr::Option {
ident: input.call(Ident::parse_any)?,
value: Some((input.parse()?, input.parse()?)),
});
}
let contents;
if input.peek(kw::all) {
Ok(CfgExpr::All {
all: input.parse()?,
paren: parenthesized!(contents in input),
exprs: contents.call(Punctuated::parse_terminated)?,
})
} else if input.peek(kw::any) {
Ok(CfgExpr::Any {
any: input.parse()?,
paren: parenthesized!(contents in input),
exprs: contents.call(Punctuated::parse_terminated)?,
})
} else if input.peek(kw::not) {
Ok(CfgExpr::Not {
not: input.parse()?,
paren: parenthesized!(contents in input),
expr: contents.parse()?,
trailing_comma: contents.parse()?,
})
} else {
Err(input.error("expected cfg-pattern"))
}
}
}
impl ToTokens for CfgExpr {
fn to_tokens(&self, tokens: &mut TokenStream) {
match self {
CfgExpr::Option { ident, value } => {
ident.to_tokens(tokens);
if let Some((eq, value)) = value {
eq.to_tokens(tokens);
value.to_tokens(tokens);
}
}
CfgExpr::All { all, paren, exprs } => {
all.to_tokens(tokens);
paren.surround(tokens, |tokens| exprs.to_tokens(tokens));
}
CfgExpr::Any { any, paren, exprs } => {
any.to_tokens(tokens);
paren.surround(tokens, |tokens| exprs.to_tokens(tokens));
}
CfgExpr::Not {
not,
paren,
expr,
trailing_comma,
} => {
not.to_tokens(tokens);
paren.surround(tokens, |tokens| {
expr.to_tokens(tokens);
trailing_comma.to_tokens(tokens);
});
}
}
}
}
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub(crate) struct Cfg {
cfg: kw::cfg,
paren: Paren,
expr: CfgExpr,
trailing_comma: Option<Token![,]>,
}
impl Cfg {
fn parse_meta(meta: &Meta) -> syn::Result<Self> {
syn::parse2(meta.to_token_stream())
}
}
impl ToTokens for Cfg {
fn to_tokens(&self, tokens: &mut TokenStream) {
let Self {
cfg,
paren,
expr,
trailing_comma,
} = self;
cfg.to_tokens(tokens);
paren.surround(tokens, |tokens| {
expr.to_tokens(tokens);
trailing_comma.to_tokens(tokens);
});
}
}
impl Parse for Cfg {
fn parse(input: ParseStream) -> syn::Result<Self> {
let contents;
Ok(Self {
cfg: input.parse()?,
paren: parenthesized!(contents in input),
expr: contents.parse()?,
trailing_comma: contents.parse()?,
})
}
}
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub(crate) struct CfgAttr {
cfg_attr: kw::cfg_attr,
paren: Paren,
expr: CfgExpr,
comma: Token![,],
attrs: Punctuated<Meta, Token![,]>,
}
impl CfgAttr {
pub(crate) fn to_cfg(&self) -> Cfg {
Cfg {
cfg: kw::cfg(self.cfg_attr.span),
paren: self.paren,
expr: self.expr.clone(),
trailing_comma: None,
}
}
fn parse_meta(meta: &Meta) -> syn::Result<Self> {
syn::parse2(meta.to_token_stream())
}
}
impl Parse for CfgAttr {
fn parse(input: ParseStream) -> syn::Result<Self> {
let contents;
Ok(Self {
cfg_attr: input.parse()?,
paren: parenthesized!(contents in input),
expr: contents.parse()?,
comma: contents.parse()?,
attrs: contents.call(Punctuated::parse_terminated)?,
})
}
}
pub(crate) struct CfgAndValue {
cfg: Cfg,
eq_token: Token![=],
value: LitBool,
}
impl Parse for CfgAndValue {
fn parse(input: ParseStream) -> syn::Result<Self> {
Ok(Self {
cfg: input.parse()?,
eq_token: input.parse()?,
value: input.parse()?,
})
}
}
pub(crate) struct Cfgs<T> {
pub(crate) bracket: Bracket,
pub(crate) cfgs_map: HashMap<Cfg, T>,
pub(crate) cfgs_list: Vec<Cfg>,
}
impl<T> Default for Cfgs<T> {
fn default() -> Self {
Self {
bracket: Default::default(),
cfgs_map: Default::default(),
cfgs_list: Default::default(),
}
}
}
impl<T> Cfgs<T> {
fn insert_cfg(&mut self, cfg: Cfg, value: T) {
match self.cfgs_map.entry(cfg) {
Entry::Occupied(_) => {}
Entry::Vacant(entry) => {
self.cfgs_list.push(entry.key().clone());
entry.insert(value);
}
}
}
}
impl Parse for Cfgs<bool> {
fn parse(input: ParseStream) -> syn::Result<Self> {
let contents;
let bracket = bracketed!(contents in input);
let mut cfgs_map = HashMap::new();
let mut cfgs_list = Vec::new();
for CfgAndValue {
cfg,
eq_token,
value,
} in contents.call(Punctuated::<CfgAndValue, Token![,]>::parse_terminated)?
{
let _ = eq_token;
match cfgs_map.entry(cfg) {
Entry::Occupied(_) => {}
Entry::Vacant(entry) => {
cfgs_list.push(entry.key().clone());
entry.insert(value.value);
}
}
}
Ok(Self {
bracket,
cfgs_map,
cfgs_list,
})
}
}
impl Parse for Cfgs<()> {
fn parse(input: ParseStream) -> syn::Result<Self> {
let contents;
let bracket = bracketed!(contents in input);
let mut cfgs_map = HashMap::new();
let mut cfgs_list = Vec::new();
for cfg in contents.call(Punctuated::<Cfg, Token![,]>::parse_terminated)? {
match cfgs_map.entry(cfg) {
Entry::Occupied(_) => {}
Entry::Vacant(entry) => {
cfgs_list.push(entry.key().clone());
entry.insert(());
}
}
}
Ok(Self {
bracket,
cfgs_map,
cfgs_list,
})
}
}
impl ToTokens for Cfgs<()> {
fn to_tokens(&self, tokens: &mut TokenStream) {
let Self {
bracket,
cfgs_map: _,
cfgs_list,
} = self;
bracket.surround(tokens, |tokens| {
for cfg in cfgs_list {
cfg.to_tokens(tokens);
<Token![,]>::default().to_tokens(tokens);
}
});
}
}
fn hdl_main(
kw: impl CustomToken,
attr: TokenStream,
item: TokenStream,
) -> syn::Result<TokenStream> {
fn parse_evaluated_cfgs_attr<R>(
input: ParseStream,
parse_inner: impl FnOnce(ParseStream) -> syn::Result<R>,
) -> syn::Result<R> {
let _: Token![#] = input.parse()?;
let bracket_content;
bracketed!(bracket_content in input);
let _: kw::__evaluated_cfgs = bracket_content.parse()?;
let paren_content;
parenthesized!(paren_content in bracket_content);
parse_inner(&paren_content)
}
let (evaluated_cfgs, item): (_, TokenStream) = Parser::parse2(
|input: ParseStream| {
let peek = input.fork();
if parse_evaluated_cfgs_attr(&peek, |_| Ok(())).is_ok() {
let evaluated_cfgs = parse_evaluated_cfgs_attr(input, Cfgs::<bool>::parse)?;
Ok((Some(evaluated_cfgs), input.parse()?))
} else {
Ok((None, input.parse()?))
}
},
item,
)?;
let cfgs = if let Some(cfgs) = evaluated_cfgs {
cfgs
} else {
let cfgs = process_cfg::collect_cfgs(syn::parse2(item.clone())?)?;
if cfgs.cfgs_list.is_empty() {
Cfgs::default()
} else {
return Ok(quote! {
::fayalite::__cfg_expansion_helper! {
[]
#cfgs
{#[::fayalite::#kw(#attr)]} { #item }
}
});
}
};
let item = syn::parse2(quote! { #[#kw(#attr)] #item })?;
let Some(item) = process_cfg::process_cfgs(item, cfgs)? else {
return Ok(TokenStream::new());
};
match item {
Item::Enum(item) => hdl_enum::hdl_enum(item),
Item::Struct(item) => hdl_bundle::hdl_bundle(item),
@ -921,3 +1265,11 @@ pub fn hdl_attr(attr: TokenStream, item: TokenStream) -> syn::Result<TokenStream
)),
}
}
pub fn hdl_module(attr: TokenStream, item: TokenStream) -> syn::Result<TokenStream> {
hdl_main(kw::hdl_module::default(), attr, item)
}
pub fn hdl_attr(attr: TokenStream, item: TokenStream) -> syn::Result<TokenStream> {
hdl_main(kw::hdl::default(), attr, item)
}

File diff suppressed because it is too large Load diff

View file

@ -5,6 +5,9 @@ use std::{env, fs, path::Path};
fn main() {
println!("cargo::rustc-check-cfg=cfg(todo)");
println!("cargo::rustc-check-cfg=cfg(cfg_false_for_tests)");
println!("cargo::rustc-check-cfg=cfg(cfg_true_for_tests)");
println!("cargo::rustc-cfg=cfg_true_for_tests");
let path = "visit_types.json";
println!("cargo::rerun-if-changed={path}");
println!("cargo::rerun-if-changed=build.rs");

View file

@ -11,6 +11,59 @@ extern crate self as fayalite;
#[doc(hidden)]
pub use std as __std;
#[doc(hidden)]
#[macro_export]
macro_rules! __cfg_expansion_helper {
(
[
$($evaluated_cfgs:ident($($evaluated_exprs:tt)*) = $evaluated_results:ident,)*
]
[
$cfg:ident($($expr:tt)*),
$($unevaluated_cfgs:ident($($unevaluated_exprs:tt)*),)*
]
// pass as tt so we get right span for attribute
$after_evaluation_attr:tt $after_evaluation_body:tt
) => {
#[$cfg($($expr)*)]
$crate::__cfg_expansion_helper! {
[
$($evaluated_cfgs($($evaluated_exprs)*) = $evaluated_results,)*
$cfg($($expr)*) = true,
]
[
$($unevaluated_cfgs($($unevaluated_exprs)*),)*
]
$after_evaluation_attr $after_evaluation_body
}
#[$cfg(not($($expr)*))]
$crate::__cfg_expansion_helper! {
[
$($evaluated_cfgs($($evaluated_exprs)*) = $evaluated_results,)*
$cfg($($expr)*) = false,
]
[
$($unevaluated_cfgs($($unevaluated_exprs)*),)*
]
$after_evaluation_attr $after_evaluation_body
}
};
(
[
$($evaluated_cfgs:ident($($evaluated_exprs:tt)*) = $evaluated_results:ident,)*
]
[]
// don't use #[...] so we get right span for `#` and `[]` of attribute
{$($after_evaluation_attr:tt)*} {$($after_evaluation_body:tt)*}
) => {
$($after_evaluation_attr)*
#[__evaluated_cfgs([
$($evaluated_cfgs($($evaluated_exprs)*) = $evaluated_results,)*
])]
$($after_evaluation_body)*
};
}
#[doc(inline)]
/// The `#[hdl_module]` attribute is applied to a Rust function so that that function creates
/// a [`Module`][`::fayalite::module::Module`] when called.

View file

@ -1601,6 +1601,14 @@ impl MakeTraceDeclTarget {
}
}
struct DebugOpaque<T>(T);
impl<T> fmt::Debug for DebugOpaque<T> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
f.write_str("<...>")
}
}
#[derive(Debug)]
pub struct Compiler {
insns: Insns<InsnsBuilding>,
@ -1622,6 +1630,7 @@ pub struct Compiler {
registers: Vec<Register>,
traces: SimTraces<Vec<SimTrace<SimTraceKind, ()>>>,
memories: Vec<Memory>,
dump_assignments_dot: Option<DebugOpaque<Box<dyn Fn(&dyn fmt::Debug)>>>,
}
impl Compiler {
@ -1647,8 +1656,14 @@ impl Compiler {
registers: Vec::new(),
traces: SimTraces(Vec::new()),
memories: Vec::new(),
dump_assignments_dot: None,
}
}
#[doc(hidden)]
/// This is explicitly unstable and may be changed/removed at any time
pub fn dump_assignments_dot(&mut self, callback: Box<dyn Fn(&dyn fmt::Debug)>) {
self.dump_assignments_dot = Some(DebugOpaque(callback));
}
fn new_sim_trace(&mut self, kind: SimTraceKind) -> TraceScalarId {
let id = TraceScalarId(self.traces.0.len());
self.traces.0.push(SimTrace {
@ -4650,12 +4665,11 @@ impl Compiler {
fn process_assignments(&mut self) {
self.assignments
.finalize(self.insns.state_layout().ty.clone().into());
println!(
"{:#?}",
petgraph::dot::Dot::new(&petgraph::graph::DiGraph::<_, _, usize>::from_elements(
self.assignments.elements()
))
);
if let Some(DebugOpaque(dump_assignments_dot)) = &self.dump_assignments_dot {
let graph =
petgraph::graph::DiGraph::<_, _, usize>::from_elements(self.assignments.elements());
dump_assignments_dot(&petgraph::dot::Dot::new(&graph));
}
let assignments_order: Vec<_> = match petgraph::algo::toposort(&self.assignments, None) {
Ok(nodes) => nodes
.into_iter()
@ -6429,7 +6443,7 @@ impl_to_sim_value_for_int_value!(SIntValue, SInt, SIntType);
struct SimulationImpl {
state: interpreter::State,
io: Expr<Bundle>,
uninitialized_inputs: HashSet<Target>,
uninitialized_inputs: HashMap<Target, Vec<Target>>,
io_targets: HashMap<Target, CompiledValue<CanonicalType>>,
made_initial_step: bool,
needs_settle: bool,
@ -6483,37 +6497,52 @@ impl SimulationImpl {
.field("clocks_triggered", clocks_triggered)
.finish_non_exhaustive()
}
fn parse_io(&mut self, target: Target, value: CompiledValue<CanonicalType>) {
/// returns `true` if `target` or any sub-targets are uninitialized inputs
fn parse_io(&mut self, target: Target, value: CompiledValue<CanonicalType>) -> bool {
self.io_targets.insert(target, value);
match value.layout.body {
CompiledTypeLayoutBody::Scalar => match target.flow() {
Flow::Source => {}
Flow::Source => false,
Flow::Sink => {
self.uninitialized_inputs.insert(target);
self.uninitialized_inputs.insert(target, vec![]);
true
}
Flow::Duplex => unreachable!(),
},
CompiledTypeLayoutBody::Array { .. } => {
let value = value.map_ty(Array::from_canonical);
let mut sub_targets = Vec::new();
for index in 0..value.layout.ty.len() {
self.parse_io(
target.join(
TargetPathElement::from(TargetPathArrayElement { index })
.intern_sized(),
),
value.element(index),
let sub_target = target.join(
TargetPathElement::from(TargetPathArrayElement { index }).intern_sized(),
);
if self.parse_io(sub_target, value.element(index)) {
sub_targets.push(sub_target);
}
}
if sub_targets.is_empty() {
false
} else {
self.uninitialized_inputs.insert(target, sub_targets);
true
}
}
CompiledTypeLayoutBody::Bundle { .. } => {
let value = value.map_ty(Bundle::from_canonical);
let mut sub_targets = Vec::new();
for BundleField { name, .. } in value.layout.ty.fields() {
self.parse_io(
target.join(
TargetPathElement::from(TargetPathBundleField { name }).intern_sized(),
),
value.field_by_name(name),
let sub_target = target.join(
TargetPathElement::from(TargetPathBundleField { name }).intern_sized(),
);
if self.parse_io(sub_target, value.field_by_name(name)) {
sub_targets.push(sub_target);
}
}
if sub_targets.is_empty() {
false
} else {
self.uninitialized_inputs.insert(target, sub_targets);
true
}
}
}
@ -6522,7 +6551,7 @@ impl SimulationImpl {
let mut retval = Self {
state: State::new(compiled.insns),
io: compiled.io.to_expr(),
uninitialized_inputs: HashSet::new(),
uninitialized_inputs: HashMap::new(),
io_targets: HashMap::new(),
made_initial_step: false,
needs_settle: true,
@ -6791,6 +6820,35 @@ impl SimulationImpl {
};
panic!("simulator read/write expression must not have dynamic array indexes");
}
fn mark_target_as_initialized(&mut self, mut target: Target) {
fn remove_target_and_children(
uninitialized_inputs: &mut HashMap<Target, Vec<Target>>,
target: Target,
) {
let Some(children) = uninitialized_inputs.remove(&target) else {
return;
};
for child in children {
remove_target_and_children(uninitialized_inputs, child);
}
}
remove_target_and_children(&mut self.uninitialized_inputs, target);
while let Some(target_child) = target.child() {
let parent = target_child.parent();
for child in self
.uninitialized_inputs
.get(&*parent)
.map(|v| &**v)
.unwrap_or(&[])
{
if self.uninitialized_inputs.contains_key(child) {
return;
}
}
target = *parent;
self.uninitialized_inputs.remove(&target);
}
}
#[track_caller]
fn read_helper(&mut self, io: Expr<CanonicalType>) -> CompiledValue<CanonicalType> {
let Some(target) = io.target() else {
@ -6810,7 +6868,7 @@ impl SimulationImpl {
self.settle();
}
Flow::Sink => {
if self.uninitialized_inputs.contains(&*target) {
if self.uninitialized_inputs.contains_key(&*target) {
panic!("can't read from an uninitialized input");
}
}
@ -6833,7 +6891,7 @@ impl SimulationImpl {
Flow::Duplex => unreachable!(),
}
if !self.made_initial_step {
self.uninitialized_inputs.remove(&*target);
self.mark_target_as_initialized(*target);
}
self.needs_settle = true;
compiled_value
@ -7136,11 +7194,11 @@ pub struct Simulation<T: BundleType> {
io: Expr<T>,
}
struct SortedSetDebug<'a, T>(&'a HashSet<T>);
struct SortedSetDebug<'a, T, V>(&'a HashMap<T, V>);
impl<T: fmt::Debug> fmt::Debug for SortedSetDebug<'_, T> {
impl<T: fmt::Debug, V> fmt::Debug for SortedSetDebug<'_, T, V> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
let mut entries = Vec::from_iter(self.0.iter().map(|v| {
let mut entries = Vec::from_iter(self.0.iter().map(|(v, _)| {
if f.alternate() {
format!("{v:#?}")
} else {

View file

@ -5,6 +5,7 @@ use crate::{
enum_::{Enum, EnumType},
expr::Flow,
int::UInt,
intern::{Intern, Interned},
sim::{
time::{SimDuration, SimInstant},
TraceArray, TraceAsyncReset, TraceBool, TraceBundle, TraceClock, TraceDecl,
@ -15,12 +16,73 @@ use crate::{
},
};
use bitvec::{order::Lsb0, slice::BitSlice};
use hashbrown::{hash_map::Entry, HashMap};
use std::{
fmt,
io::{self, Write},
mem,
fmt::{self, Write as _},
io, mem,
};
#[derive(Default)]
struct Scope {
last_inserted: HashMap<Interned<str>, usize>,
}
#[derive(Copy, Clone)]
struct VerilogIdentifier {
unescaped_name: Interned<str>,
}
impl VerilogIdentifier {
fn needs_escape(self) -> bool {
// we only allow ascii, so we can just check bytes
let Some((&first, rest)) = self.unescaped_name.as_bytes().split_first() else {
unreachable!("Scope::new_identifier guarantees a non-empty name");
};
if !first.is_ascii_alphabetic() && first != b'_' {
true
} else {
rest.iter()
.any(|&ch| !ch.is_ascii_alphanumeric() && ch != b'_' && ch != b'$')
}
}
}
impl fmt::Display for VerilogIdentifier {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
if self.needs_escape() {
f.write_str("\\")?;
}
write!(f, "{}", Escaped(self.unescaped_name))
}
}
impl Scope {
fn new_identifier(&mut self, unescaped_name: Interned<str>) -> VerilogIdentifier {
let next_disambiguator = match self.last_inserted.entry(unescaped_name) {
Entry::Vacant(entry) => {
entry.insert(1);
return VerilogIdentifier { unescaped_name };
}
Entry::Occupied(entry) => entry.get() + 1,
};
let mut disambiguated_name = String::from(&*unescaped_name);
for disambiguator in next_disambiguator.. {
disambiguated_name.truncate(unescaped_name.len());
write!(disambiguated_name, "_{disambiguator}").expect("can't fail");
if let Entry::Vacant(entry) = self.last_inserted.entry((*disambiguated_name).intern()) {
let retval = VerilogIdentifier {
unescaped_name: *entry.key(),
};
entry.insert(1);
// speed up future searches
self.last_inserted.insert(unescaped_name, disambiguator);
return retval;
}
}
panic!("too many names");
}
}
pub struct VcdWriterDecls<W: io::Write + 'static> {
writer: W,
timescale: SimDuration,
@ -97,14 +159,20 @@ impl<W: io::Write> fmt::Debug for VcdWriterDecls<W> {
}
}
/// pass in scope to ensure it's not available in child scope
fn write_vcd_scope<W: io::Write, R>(
writer: &mut W,
scope_type: &str,
scope_name: &str,
f: impl FnOnce(&mut W) -> io::Result<R>,
scope_name: Interned<str>,
scope: &mut Scope,
f: impl FnOnce(&mut W, &mut Scope) -> io::Result<R>,
) -> io::Result<R> {
writeln!(writer, "$scope {scope_type} {scope_name} $end")?;
let retval = f(writer)?;
writeln!(
writer,
"$scope {scope_type} {} $end",
scope.new_identifier(scope_name),
)?;
let retval = f(writer, &mut Scope::default())?;
writeln!(writer, "$upscope $end")?;
Ok(retval)
}
@ -143,24 +211,28 @@ trait_arg! {
struct ArgModule<'a> {
properties: &'a mut VcdWriterProperties,
scope: &'a mut Scope,
}
impl<'a> ArgModule<'a> {
fn reborrow(&mut self) -> ArgModule<'_> {
ArgModule {
properties: self.properties,
scope: self.scope,
}
}
}
struct ArgModuleBody<'a> {
properties: &'a mut VcdWriterProperties,
scope: &'a mut Scope,
}
impl<'a> ArgModuleBody<'a> {
fn reborrow(&mut self) -> ArgModuleBody<'_> {
ArgModuleBody {
properties: self.properties,
scope: self.scope,
}
}
}
@ -170,6 +242,7 @@ struct ArgInType<'a> {
sink_var_type: &'static str,
duplex_var_type: &'static str,
properties: &'a mut VcdWriterProperties,
scope: &'a mut Scope,
}
impl<'a> ArgInType<'a> {
@ -179,6 +252,7 @@ impl<'a> ArgInType<'a> {
sink_var_type: self.sink_var_type,
duplex_var_type: self.duplex_var_type,
properties: self.properties,
scope: self.scope,
}
}
}
@ -226,55 +300,42 @@ fn write_vcd_id<W: io::Write>(writer: &mut W, mut id: usize) -> io::Result<()> {
Ok(())
}
fn write_escaped<W: io::Write>(writer: &mut W, value: impl fmt::Display) -> io::Result<()> {
// escaping rules from function GTKWave uses to decode VCD strings:
// https://github.com/gtkwave/gtkwave/blob/491f24d7e8619cfc1fcc65704ee5c967d1083c18/lib/libfst/fstapi.c#L7090
struct Wrapper<W>(W);
impl<W: io::Write> io::Write for Wrapper<W> {
fn write(&mut self, buf: &[u8]) -> io::Result<usize> {
if buf.is_empty() {
return self.0.write(buf);
}
let mut retval = 0;
for &byte in buf {
match byte {
b'\\' | b'\'' | b'"' | b'?' => self.0.write_all(&[b'\\', byte])?,
b'\n' => self.0.write_all(br"\n")?,
b'\r' => self.0.write_all(br"\r")?,
b'\t' => self.0.write_all(br"\t")?,
0x7 => self.0.write_all(br"\a")?,
0x8 => self.0.write_all(br"\b")?,
0xC => self.0.write_all(br"\f")?,
0xB => self.0.write_all(br"\v")?,
_ => {
if byte.is_ascii_graphic() {
self.0.write_all(&[byte])?;
} else {
write!(self.0, r"\x{byte:02x}")?;
struct Escaped<T: fmt::Display>(T);
impl<T: fmt::Display> fmt::Display for Escaped<T> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
// escaping rules from function GTKWave uses to decode VCD strings:
// https://github.com/gtkwave/gtkwave/blob/491f24d7e8619cfc1fcc65704ee5c967d1083c18/lib/libfst/fstapi.c#L7090
struct Wrapper<W>(W);
impl<W: fmt::Write> fmt::Write for Wrapper<W> {
fn write_str(&mut self, s: &str) -> fmt::Result {
for byte in s.bytes() {
match byte {
b'\\' | b'\'' | b'"' | b'?' => {
self.0.write_str("\\")?;
self.0.write_char(byte as char)?;
}
b'\n' => self.0.write_str(r"\n")?,
b'\r' => self.0.write_str(r"\r")?,
b'\t' => self.0.write_str(r"\t")?,
0x7 => self.0.write_str(r"\a")?,
0x8 => self.0.write_str(r"\b")?,
0xC => self.0.write_str(r"\f")?,
0xB => self.0.write_str(r"\v")?,
_ => {
if byte.is_ascii_graphic() {
self.0.write_char(byte as char)?;
} else {
write!(self.0, r"\x{byte:02x}")?;
}
}
}
}
retval += 1;
Ok(())
}
Ok(retval)
}
fn flush(&mut self) -> io::Result<()> {
self.0.flush()
}
write!(Wrapper(f), "{}", self.0)
}
write!(Wrapper(writer), "{value}")
}
fn is_unescaped_verilog_identifier(ident: &str) -> bool {
// we only allow ascii, so we can just check bytes
let Some((&first, rest)) = ident.as_bytes().split_first() else {
return false; // empty string is not an identifier
};
(first.is_ascii_alphabetic() || first == b'_')
&& rest
.iter()
.all(|&ch| ch.is_ascii_alphanumeric() || ch == b'_' || ch == b'$')
}
fn write_vcd_var<W: io::Write>(
@ -284,7 +345,7 @@ fn write_vcd_var<W: io::Write>(
var_type: &str,
size: usize,
location: TraceLocation,
name: &str,
name: VerilogIdentifier,
) -> io::Result<()> {
let id = match location {
TraceLocation::Scalar(id) => id.as_usize(),
@ -319,12 +380,7 @@ fn write_vcd_var<W: io::Write>(
};
write!(writer, "$var {var_type} {size} ")?;
write_vcd_id(writer, id)?;
writer.write_all(b" ")?;
if !is_unescaped_verilog_identifier(name) {
writer.write_all(b"\\")?;
}
write_escaped(writer, name)?;
writer.write_all(b" $end\n")
writeln!(writer, " {name} $end")
}
impl WriteTrace for TraceUInt {
@ -334,6 +390,7 @@ impl WriteTrace for TraceUInt {
sink_var_type,
duplex_var_type,
properties,
scope,
} = arg.in_type();
let Self {
location,
@ -356,7 +413,7 @@ impl WriteTrace for TraceUInt {
var_type,
ty.width(),
location,
&name,
scope.new_identifier(name),
)
}
}
@ -421,6 +478,7 @@ impl WriteTrace for TraceEnumDiscriminant {
sink_var_type: _,
duplex_var_type: _,
properties,
scope,
} = arg.in_type();
let Self {
location,
@ -435,7 +493,7 @@ impl WriteTrace for TraceEnumDiscriminant {
"string",
1,
location,
&name,
scope.new_identifier(name),
)
}
}
@ -507,11 +565,11 @@ impl WriteTrace for TraceScope {
impl WriteTrace for TraceModule {
fn write_trace<W: io::Write, A: Arg>(self, writer: &mut W, mut arg: A) -> io::Result<()> {
let ArgModule { properties } = arg.module();
let ArgModule { properties, scope } = arg.module();
let Self { name, children } = self;
write_vcd_scope(writer, "module", &name, |writer| {
write_vcd_scope(writer, "module", name, scope, |writer, scope| {
for child in children {
child.write_trace(writer, ArgModuleBody { properties })?;
child.write_trace(writer, ArgModuleBody { properties, scope })?;
}
Ok(())
})
@ -520,7 +578,7 @@ impl WriteTrace for TraceModule {
impl WriteTrace for TraceInstance {
fn write_trace<W: io::Write, A: Arg>(self, writer: &mut W, mut arg: A) -> io::Result<()> {
let ArgModuleBody { properties } = arg.module_body();
let ArgModuleBody { properties, scope } = arg.module_body();
let Self {
name: _,
instance_io,
@ -534,15 +592,16 @@ impl WriteTrace for TraceInstance {
sink_var_type: "wire",
duplex_var_type: "wire",
properties,
scope,
},
)?;
module.write_trace(writer, ArgModule { properties })
module.write_trace(writer, ArgModule { properties, scope })
}
}
impl WriteTrace for TraceMem {
fn write_trace<W: io::Write, A: Arg>(self, writer: &mut W, mut arg: A) -> io::Result<()> {
let ArgModuleBody { properties } = arg.module_body();
let ArgModuleBody { properties, scope } = arg.module_body();
let Self {
id,
name,
@ -551,27 +610,41 @@ impl WriteTrace for TraceMem {
ports,
array_type,
} = self;
write_vcd_scope(writer, "struct", &*name, |writer| {
write_vcd_scope(writer, "struct", "contents", |writer| {
for element_index in 0..array_type.len() {
write_vcd_scope(writer, "struct", &format!("[{element_index}]"), |writer| {
properties.memory_properties[id.as_usize()].element_index = element_index;
properties.memory_properties[id.as_usize()].element_part_index = 0;
element_type.write_trace(
write_vcd_scope(writer, "struct", name, scope, |writer, scope| {
write_vcd_scope(
writer,
"struct",
"contents".intern(),
scope,
|writer, scope| {
for element_index in 0..array_type.len() {
write_vcd_scope(
writer,
ArgInType {
source_var_type: "reg",
sink_var_type: "reg",
duplex_var_type: "reg",
properties,
"struct",
Intern::intern_owned(format!("[{element_index}]")),
scope,
|writer, scope| {
properties.memory_properties[id.as_usize()].element_index =
element_index;
properties.memory_properties[id.as_usize()].element_part_index = 0;
element_type.write_trace(
writer,
ArgInType {
source_var_type: "reg",
sink_var_type: "reg",
duplex_var_type: "reg",
properties,
scope,
},
)
},
)
})?;
}
Ok(())
})?;
)?;
}
Ok(())
},
)?;
for port in ports {
port.write_trace(writer, ArgModuleBody { properties })?;
port.write_trace(writer, ArgModuleBody { properties, scope })?;
}
Ok(())
})
@ -580,7 +653,7 @@ impl WriteTrace for TraceMem {
impl WriteTrace for TraceMemPort {
fn write_trace<W: io::Write, A: Arg>(self, writer: &mut W, mut arg: A) -> io::Result<()> {
let ArgModuleBody { properties } = arg.module_body();
let ArgModuleBody { properties, scope } = arg.module_body();
let Self {
name: _,
bundle,
@ -593,6 +666,7 @@ impl WriteTrace for TraceMemPort {
sink_var_type: "wire",
duplex_var_type: "wire",
properties,
scope,
},
)
}
@ -600,7 +674,7 @@ impl WriteTrace for TraceMemPort {
impl WriteTrace for TraceWire {
fn write_trace<W: io::Write, A: Arg>(self, writer: &mut W, mut arg: A) -> io::Result<()> {
let ArgModuleBody { properties } = arg.module_body();
let ArgModuleBody { properties, scope } = arg.module_body();
let Self {
name: _,
child,
@ -613,6 +687,7 @@ impl WriteTrace for TraceWire {
sink_var_type: "wire",
duplex_var_type: "wire",
properties,
scope,
},
)
}
@ -620,7 +695,7 @@ impl WriteTrace for TraceWire {
impl WriteTrace for TraceReg {
fn write_trace<W: io::Write, A: Arg>(self, writer: &mut W, mut arg: A) -> io::Result<()> {
let ArgModuleBody { properties } = arg.module_body();
let ArgModuleBody { properties, scope } = arg.module_body();
let Self {
name: _,
child,
@ -633,6 +708,7 @@ impl WriteTrace for TraceReg {
sink_var_type: "reg",
duplex_var_type: "reg",
properties,
scope,
},
)
}
@ -640,7 +716,7 @@ impl WriteTrace for TraceReg {
impl WriteTrace for TraceModuleIO {
fn write_trace<W: io::Write, A: Arg>(self, writer: &mut W, mut arg: A) -> io::Result<()> {
let ArgModuleBody { properties } = arg.module_body();
let ArgModuleBody { properties, scope } = arg.module_body();
let Self {
name: _,
child,
@ -654,6 +730,7 @@ impl WriteTrace for TraceModuleIO {
sink_var_type: "wire",
duplex_var_type: "wire",
properties,
scope,
},
)
}
@ -661,16 +738,31 @@ impl WriteTrace for TraceModuleIO {
impl WriteTrace for TraceBundle {
fn write_trace<W: io::Write, A: Arg>(self, writer: &mut W, mut arg: A) -> io::Result<()> {
let mut arg = arg.in_type();
let ArgInType {
source_var_type,
sink_var_type,
duplex_var_type,
properties,
scope,
} = arg.in_type();
let Self {
name,
fields,
ty: _,
flow: _,
} = self;
write_vcd_scope(writer, "struct", &name, |writer| {
write_vcd_scope(writer, "struct", name, scope, |writer, scope| {
for field in fields {
field.write_trace(writer, arg.reborrow())?;
field.write_trace(
writer,
ArgInType {
source_var_type,
sink_var_type,
duplex_var_type,
properties,
scope,
},
)?;
}
Ok(())
})
@ -679,16 +771,31 @@ impl WriteTrace for TraceBundle {
impl WriteTrace for TraceArray {
fn write_trace<W: io::Write, A: Arg>(self, writer: &mut W, mut arg: A) -> io::Result<()> {
let mut arg = arg.in_type();
let ArgInType {
source_var_type,
sink_var_type,
duplex_var_type,
properties,
scope,
} = arg.in_type();
let Self {
name,
elements,
ty: _,
flow: _,
} = self;
write_vcd_scope(writer, "struct", &name, |writer| {
write_vcd_scope(writer, "struct", name, scope, |writer, scope| {
for element in elements {
element.write_trace(writer, arg.reborrow())?;
element.write_trace(
writer,
ArgInType {
source_var_type,
sink_var_type,
duplex_var_type,
properties,
scope,
},
)?;
}
Ok(())
})
@ -697,7 +804,13 @@ impl WriteTrace for TraceArray {
impl WriteTrace for TraceEnumWithFields {
fn write_trace<W: io::Write, A: Arg>(self, writer: &mut W, mut arg: A) -> io::Result<()> {
let mut arg = arg.in_type();
let ArgInType {
source_var_type,
sink_var_type,
duplex_var_type,
properties,
scope,
} = arg.in_type();
let Self {
name,
discriminant,
@ -705,10 +818,28 @@ impl WriteTrace for TraceEnumWithFields {
ty: _,
flow: _,
} = self;
write_vcd_scope(writer, "struct", &name, |writer| {
discriminant.write_trace(writer, arg.reborrow())?;
write_vcd_scope(writer, "struct", name, scope, |writer, scope| {
discriminant.write_trace(
writer,
ArgInType {
source_var_type,
sink_var_type,
duplex_var_type,
properties,
scope,
},
)?;
for field in non_empty_fields {
field.write_trace(writer, arg.reborrow())?;
field.write_trace(
writer,
ArgInType {
source_var_type,
sink_var_type,
duplex_var_type,
properties,
scope,
},
)?;
}
Ok(())
})
@ -744,6 +875,7 @@ impl<W: io::Write> TraceWriterDecls for VcdWriterDecls<W> {
&mut writer,
ArgModule {
properties: &mut properties,
scope: &mut Scope::default(),
},
)?;
writeln!(writer, "$enddefinitions $end")?;
@ -798,9 +930,7 @@ fn write_string_value_change(
value: impl fmt::Display,
id: usize,
) -> io::Result<()> {
writer.write_all(b"s")?;
write_escaped(writer, value)?;
writer.write_all(b" ")?;
write!(writer, "s{} ", Escaped(value))?;
write_vcd_id(writer, id)?;
writer.write_all(b"\n")
}
@ -946,3 +1076,49 @@ impl<W: io::Write> fmt::Debug for VcdWriter<W> {
.finish_non_exhaustive()
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn test_scope() {
let mut scope = Scope::default();
assert_eq!(&*scope.new_identifier("foo".intern()).unescaped_name, "foo");
assert_eq!(
&*scope.new_identifier("foo_0".intern()).unescaped_name,
"foo_0"
);
assert_eq!(
&*scope.new_identifier("foo_1".intern()).unescaped_name,
"foo_1"
);
assert_eq!(
&*scope.new_identifier("foo_3".intern()).unescaped_name,
"foo_3"
);
assert_eq!(
&*scope.new_identifier("foo".intern()).unescaped_name,
"foo_2"
);
assert_eq!(
&*scope.new_identifier("foo".intern()).unescaped_name,
"foo_4"
);
assert_eq!(
&*scope.new_identifier("foo_0".intern()).unescaped_name,
"foo_0_2"
);
assert_eq!(
&*scope.new_identifier("foo_1".intern()).unescaped_name,
"foo_1_2"
);
for i in 5..1000u64 {
// verify it actually picks the next available identifier with no skips or duplicates
assert_eq!(
*scope.new_identifier("foo".intern()).unescaped_name,
format!("foo_{i}"),
);
}
}
}

View file

@ -49,6 +49,18 @@ impl<T: Type> ReadyValid<T> {
}
}
/// This debug port is only meant to assist the formal proof of the queue.
#[cfg(test)]
#[doc(hidden)]
#[hdl]
pub struct QueueDebugPort<Element, Index> {
#[hdl(flip)]
index_to_check: Index,
stored: Element,
inp_index: Index,
out_index: Index,
}
#[hdl_module]
pub fn queue<T: Type>(
ty: T,
@ -178,6 +190,22 @@ pub fn queue<T: Type>(
}
}
}
// These debug ports expose some internal state during the Induction phase
// of Formal Verification. They are not present in normal use.
#[cfg(test)]
{
#[hdl]
let dbg: QueueDebugPort<T, UInt> = m.output(QueueDebugPort[ty][index_ty]);
// read the memory word currently stored at some fixed index
let debug_port = mem.new_read_port();
connect(debug_port.addr, dbg.index_to_check);
connect(debug_port.en, true);
connect(debug_port.clk, cd.clk);
connect(dbg.stored, debug_port.data);
// also expose the current read and write indices
connect(dbg.inp_index, inp_index_reg);
connect(dbg.out_index, out_index_reg);
}
}
#[cfg(test)]
@ -196,13 +224,23 @@ mod tests {
format_args!("test_queue_{capacity}_{inp_ready_is_comb}_{out_valid_is_comb}"),
queue_test(capacity, inp_ready_is_comb, out_valid_is_comb),
FormalMode::Prove,
14,
2,
None,
ExportOptions {
simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
..ExportOptions::default()
},
);
/// Formal verification of the FIFO queue
///
/// The strategy derives from the observation that, if we filter its
/// input and output streams to consider just one in every N reads and
/// writes (where N is the FIFO capacity), then the FIFO effectively
/// behaves as a one-entry FIFO.
///
/// In particular, any counterexample of the full FIFO behaving badly
/// will also be caught by one of the filtered versions (one which
/// happens to be in phase with the offending input or output).
#[hdl_module]
fn queue_test(capacity: NonZeroUsize, inp_ready_is_comb: bool, out_valid_is_comb: bool) {
#[hdl]
@ -217,6 +255,8 @@ mod tests {
rst: formal_reset().to_reset(),
},
);
// random input data
#[hdl]
let inp_data: HdlOption<UInt<8>> = wire();
#[hdl]
@ -225,16 +265,26 @@ mod tests {
} else {
connect(inp_data, HdlNone());
}
// assert output ready at random
#[hdl]
let out_ready: Bool = wire();
connect(out_ready, any_seq(Bool));
let index_ty: UInt<32> = UInt::TYPE;
// The current number of elements in the FIFO ranges from zero to
// maximum capacity, inclusive.
let count_ty = UInt::range_inclusive(0..=capacity.get());
// type for counters that wrap around at the FIFO capacity
let index_ty = UInt::range(0..capacity.get());
// among all entries of the FIFO internal circular memory, choose
// one at random to check
#[hdl]
let index_to_check = wire();
let index_to_check = wire(index_ty);
connect(index_to_check, any_const(index_ty));
let index_max = !index_ty.zero();
// we saturate at index_max, so only check indexes where we properly maintain position
hdl_assume(clk, index_to_check.cmp_ne(index_max), "");
hdl_assume(clk, index_to_check.cmp_lt(capacity.get()), "");
// instantiate and connect the queue
#[hdl]
let dut = instance(queue(
UInt[ConstUsize::<8>],
@ -245,109 +295,172 @@ mod tests {
connect(dut.cd, cd);
connect(dut.inp.data, inp_data);
connect(dut.out.ready, out_ready);
hdl_assume(
clk,
index_to_check.cmp_ne(!Expr::ty(index_to_check).zero()),
"",
);
// Keep an independent count of words in the FIFO. Ensure that
// it's always correct, and never overflows.
#[hdl]
let expected_count_reg = reg_builder().clock_domain(cd).reset(0u32);
#[hdl]
let next_expected_count = wire();
connect(next_expected_count, expected_count_reg);
connect(expected_count_reg, next_expected_count);
let expected_count_reg = reg_builder().clock_domain(cd).reset(count_ty.zero());
#[hdl]
if ReadyValid::firing(dut.inp) & !ReadyValid::firing(dut.out) {
connect_any(next_expected_count, expected_count_reg + 1u8);
hdl_assert(clk, expected_count_reg.cmp_ne(capacity.get()), "");
connect_any(expected_count_reg, expected_count_reg + 1u8);
} else if !ReadyValid::firing(dut.inp) & ReadyValid::firing(dut.out) {
connect_any(next_expected_count, expected_count_reg - 1u8);
hdl_assert(clk, expected_count_reg.cmp_ne(count_ty.zero()), "");
connect_any(expected_count_reg, expected_count_reg - 1u8);
}
hdl_assert(cd.clk, expected_count_reg.cmp_eq(dut.count), "");
#[hdl]
let prev_out_ready_reg = reg_builder().clock_domain(cd).reset(!0_hdl_u3);
connect_any(
prev_out_ready_reg,
(prev_out_ready_reg << 1) | out_ready.cast_to(UInt[1]),
);
#[hdl]
let prev_inp_valid_reg = reg_builder().clock_domain(cd).reset(!0_hdl_u3);
connect_any(
prev_inp_valid_reg,
(prev_inp_valid_reg << 1) | HdlOption::is_some(inp_data).cast_to(UInt[1]),
);
hdl_assume(
clk,
(prev_out_ready_reg & prev_inp_valid_reg).cmp_ne(0u8),
"",
);
hdl_assert(clk, expected_count_reg.cmp_eq(dut.count), "");
// keep an independent write index into the FIFO's circular buffer
#[hdl]
let inp_index_reg = reg_builder().clock_domain(cd).reset(index_ty.zero());
#[hdl]
let stored_inp_data_reg = reg_builder().clock_domain(cd).reset(0u8);
#[hdl]
if let HdlSome(data) = ReadyValid::firing_data(dut.inp) {
if ReadyValid::firing(dut.inp) {
#[hdl]
if inp_index_reg.cmp_lt(index_max) {
if inp_index_reg.cmp_ne(capacity.get() - 1) {
connect_any(inp_index_reg, inp_index_reg + 1u8);
#[hdl]
if inp_index_reg.cmp_eq(index_to_check) {
connect(stored_inp_data_reg, data);
}
} else {
connect_any(inp_index_reg, 0_hdl_u0);
}
}
#[hdl]
if inp_index_reg.cmp_lt(index_to_check) {
hdl_assert(clk, stored_inp_data_reg.cmp_eq(0u8), "");
}
// keep an independent read index into the FIFO's circular buffer
#[hdl]
let out_index_reg = reg_builder().clock_domain(cd).reset(index_ty.zero());
#[hdl]
let stored_out_data_reg = reg_builder().clock_domain(cd).reset(0u8);
#[hdl]
if let HdlSome(data) = ReadyValid::firing_data(dut.out) {
if ReadyValid::firing(dut.out) {
#[hdl]
if out_index_reg.cmp_lt(index_max) {
if out_index_reg.cmp_ne(capacity.get() - 1) {
connect_any(out_index_reg, out_index_reg + 1u8);
} else {
connect_any(out_index_reg, 0_hdl_u0);
}
}
// filter the input data stream, predicated by the read index
// matching the chosen position in the FIFO's circular buffer
#[hdl]
let inp_index_matches = wire();
connect(inp_index_matches, inp_index_reg.cmp_eq(index_to_check));
#[hdl]
let inp_firing_data = wire();
connect(inp_firing_data, HdlNone());
#[hdl]
if inp_index_matches {
connect(inp_firing_data, ReadyValid::firing_data(dut.inp));
}
// filter the output data stream, predicated by the write index
// matching the chosen position in the FIFO's circular buffer
#[hdl]
let out_index_matches = wire();
connect(out_index_matches, out_index_reg.cmp_eq(index_to_check));
#[hdl]
let out_firing_data = wire();
connect(out_firing_data, HdlNone());
#[hdl]
if out_index_matches {
connect(out_firing_data, ReadyValid::firing_data(dut.out));
}
// Implement a one-entry FIFO and ensure its equivalence to the
// filtered FIFO.
//
// the holding register for our one-entry FIFO
#[hdl]
let stored_reg = reg_builder().clock_domain(cd).reset(HdlNone());
#[hdl]
match stored_reg {
// If the holding register is empty...
HdlNone => {
#[hdl]
if out_index_reg.cmp_eq(index_to_check) {
connect(stored_out_data_reg, data);
match inp_firing_data {
// ... and we are not receiving data, then we must not
// transmit any data.
HdlNone => hdl_assert(clk, HdlOption::is_none(out_firing_data), ""),
// If we are indeed receiving some data...
HdlSome(data_in) => {
#[hdl]
match out_firing_data {
// ... and transmitting at the same time, we
// must be transmitting the input data itself,
// since the holding register is empty.
HdlSome(data_out) => hdl_assert(clk, data_out.cmp_eq(data_in), ""),
// If we are receiving, but not transmitting,
// store the received data in the holding
// register.
HdlNone => connect(stored_reg, HdlSome(data_in)),
}
}
}
}
// If there is some value stored in the holding register...
HdlSome(stored) => {
#[hdl]
match out_firing_data {
// ... and we are not transmitting it, we cannot
// receive any more data.
HdlNone => hdl_assert(clk, HdlOption::is_none(inp_firing_data), ""),
// If we are transmitting a previously stored value...
HdlSome(data_out) => {
// ... it must be the same data we stored earlier.
hdl_assert(clk, data_out.cmp_eq(stored), "");
// Also, accept new data, if any. Otherwise,
// let the holding register become empty.
connect(stored_reg, inp_firing_data);
}
}
}
}
// from now on, some extra assertions in order to pass induction
// sync the holding register, when it's occupied, to the
// corresponding entry in the FIFO's circular buffer
connect(dut.dbg.index_to_check, index_to_check);
#[hdl]
if out_index_reg.cmp_lt(index_to_check) {
hdl_assert(clk, stored_out_data_reg.cmp_eq(0u8), "");
if let HdlSome(stored) = stored_reg {
hdl_assert(clk, stored.cmp_eq(dut.dbg.stored), "");
}
hdl_assert(clk, inp_index_reg.cmp_ge(out_index_reg), "");
// sync the read and write indices
hdl_assert(clk, inp_index_reg.cmp_eq(dut.dbg.inp_index), "");
hdl_assert(clk, out_index_reg.cmp_eq(dut.dbg.out_index), "");
// the indices should never go past the capacity, but induction
// doesn't know that...
hdl_assert(clk, inp_index_reg.cmp_lt(capacity.get()), "");
hdl_assert(clk, out_index_reg.cmp_lt(capacity.get()), "");
// strongly constrain the state of the holding register
//
// The holding register is full if and only if the corresponding
// FIFO entry was written to and not yet read. In other words, if
// the number of pending reads until the chosen entry is read out
// is greater than the current FIFO count, then the entry couldn't
// be in the FIFO in the first place.
#[hdl]
if inp_index_reg.cmp_lt(index_max) & out_index_reg.cmp_lt(index_max) {
hdl_assert(
clk,
expected_count_reg.cmp_eq(inp_index_reg - out_index_reg),
"",
);
let pending_reads: UInt = wire(index_ty);
// take care of wrap-around when subtracting indices, add the
// capacity amount to keep the result positive if necessary
#[hdl]
if index_to_check.cmp_ge(out_index_reg) {
connect(pending_reads, index_to_check - out_index_reg);
} else {
hdl_assert(
clk,
expected_count_reg.cmp_ge(inp_index_reg - out_index_reg),
"",
connect(
pending_reads,
index_to_check + capacity.get() - out_index_reg,
);
}
// check whether the chosen entry is in the FIFO
#[hdl]
if inp_index_reg.cmp_gt(index_to_check) & out_index_reg.cmp_gt(index_to_check) {
hdl_assert(clk, stored_inp_data_reg.cmp_eq(stored_out_data_reg), "");
}
let expected_stored: Bool = wire();
connect(expected_stored, pending_reads.cmp_lt(dut.count));
// sync with the state of the holding register
hdl_assert(
clk,
expected_stored.cmp_eq(HdlOption::is_some(stored_reg)),
"",
);
}
}
@ -430,4 +543,24 @@ mod tests {
fn test_4_true_true() {
test_queue(NonZero::new(4).unwrap(), true, true);
}
#[test]
fn test_many_false_false() {
test_queue(NonZero::new((2 << 16) - 5).unwrap(), false, false);
}
#[test]
fn test_many_false_true() {
test_queue(NonZero::new((2 << 16) - 5).unwrap(), false, true);
}
#[test]
fn test_many_true_false() {
test_queue(NonZero::new((2 << 16) - 5).unwrap(), true, false);
}
#[test]
fn test_many_true_true() {
test_queue(NonZero::new((2 << 16) - 5).unwrap(), true, true);
}
}

View file

@ -4287,3 +4287,61 @@ circuit check_deduce_resets:
",
};
}
// intentionally not outline_generated to ensure we get correct macro hygiene
#[hdl_module]
pub fn check_cfgs<#[cfg(cfg_false_for_tests)] A: Type, #[cfg(cfg_true_for_tests)] B: Type>(
#[cfg(cfg_false_for_tests)] a: A,
#[cfg(cfg_true_for_tests)] b: B,
) {
#[hdl]
struct S<#[cfg(cfg_false_for_tests)] A, #[cfg(cfg_true_for_tests)] B> {
#[cfg(cfg_false_for_tests)]
a: A,
#[cfg(cfg_true_for_tests)]
b: B,
}
#[hdl]
#[cfg(cfg_false_for_tests)]
let i_a: A = m.input(a);
#[hdl]
#[cfg(cfg_true_for_tests)]
let i_b: B = m.input(b);
#[hdl]
let w: S<UInt<8>> = wire();
#[cfg(cfg_false_for_tests)]
{
#[hdl]
let o_a: A = m.output(a);
connect(o_a, w.a.cast_bits_to(a));
connect_any(w.a, i_a.cast_to_bits());
}
#[cfg(cfg_true_for_tests)]
{
#[hdl]
let o_b: B = m.output(b);
connect(o_b, w.b.cast_bits_to(b));
connect_any(w.b, i_b.cast_to_bits());
}
}
#[test]
fn test_cfgs() {
let _n = SourceLocation::normalize_files_for_tests();
let m = check_cfgs(UInt[8]);
dbg!(m);
#[rustfmt::skip] // work around https://github.com/rust-lang/rustfmt/issues/6161
assert_export_firrtl! {
m =>
"/test/check_cfgs.fir": r"FIRRTL version 3.2.0
circuit check_cfgs:
type Ty0 = {b: UInt<8>}
module check_cfgs: @[the_test_file.rs 9962:1]
input i_b: UInt<8> @[the_test_file.rs 9979:20]
output o_b: UInt<8> @[the_test_file.rs 9992:24]
wire w: Ty0 @[the_test_file.rs 9981:25]
connect o_b, w.b @[the_test_file.rs 9993:9]
connect w.b, i_b @[the_test_file.rs 9994:9]
",
};
}

View file

@ -255,8 +255,14 @@ fn test_shift_register() {
let mut sim = Simulation::new(shift_register());
let mut writer = RcWriter::default();
sim.add_trace_writer(VcdWriterDecls::new(writer.clone()));
sim.write_clock(sim.io().cd.clk, false);
sim.write_reset(sim.io().cd.rst, true);
sim.write(
sim.io().cd,
#[hdl]
ClockDomain {
clk: false.to_clock(),
rst: true.to_sync_reset(),
},
);
sim.write_bool(sim.io().d, false);
sim.advance_time(SimDuration::from_micros(1));
sim.write_clock(sim.io().cd.clk, true);
@ -1240,3 +1246,33 @@ fn test_memories3() {
panic!();
}
}
#[hdl_module(outline_generated)]
pub fn duplicate_names() {
#[hdl]
let w = wire();
connect(w, 5u8);
#[hdl]
let w = wire();
connect(w, 6u8);
}
#[test]
fn test_duplicate_names() {
let _n = SourceLocation::normalize_files_for_tests();
let mut sim = Simulation::new(duplicate_names());
let mut writer = RcWriter::default();
sim.add_trace_writer(VcdWriterDecls::new(writer.clone()));
sim.advance_time(SimDuration::from_micros(1));
sim.flush_traces().unwrap();
let vcd = String::from_utf8(writer.take()).unwrap();
println!("####### VCD:\n{vcd}\n#######");
if vcd != include_str!("sim/expected/duplicate_names.vcd") {
panic!();
}
let sim_debug = format!("{sim:#?}");
println!("#######\n{sim_debug}\n#######");
if sim_debug != include_str!("sim/expected/duplicate_names.txt") {
panic!();
}
}

View file

@ -0,0 +1,153 @@
Simulation {
state: State {
insns: Insns {
state_layout: StateLayout {
ty: TypeLayout {
small_slots: StatePartLayout<SmallSlots> {
len: 0,
debug_data: [],
..
},
big_slots: StatePartLayout<BigSlots> {
len: 4,
debug_data: [
SlotDebugData {
name: "InstantiatedModule(duplicate_names: duplicate_names).duplicate_names::w",
ty: UInt<8>,
},
SlotDebugData {
name: "",
ty: UInt<8>,
},
SlotDebugData {
name: "InstantiatedModule(duplicate_names: duplicate_names).duplicate_names::w",
ty: UInt<8>,
},
SlotDebugData {
name: "",
ty: UInt<8>,
},
],
..
},
},
memories: StatePartLayout<Memories> {
len: 0,
debug_data: [],
layout_data: [],
..
},
},
insns: [
// at: module-XXXXXXXXXX.rs:1:1
0: Const {
dest: StatePartIndex<BigSlots>(3), // (0x6) SlotDebugData { name: "", ty: UInt<8> },
value: 0x6,
},
// at: module-XXXXXXXXXX.rs:5:1
1: Copy {
dest: StatePartIndex<BigSlots>(2), // (0x6) SlotDebugData { name: "InstantiatedModule(duplicate_names: duplicate_names).duplicate_names::w", ty: UInt<8> },
src: StatePartIndex<BigSlots>(3), // (0x6) SlotDebugData { name: "", ty: UInt<8> },
},
// at: module-XXXXXXXXXX.rs:1:1
2: Const {
dest: StatePartIndex<BigSlots>(1), // (0x5) SlotDebugData { name: "", ty: UInt<8> },
value: 0x5,
},
// at: module-XXXXXXXXXX.rs:3:1
3: Copy {
dest: StatePartIndex<BigSlots>(0), // (0x5) SlotDebugData { name: "InstantiatedModule(duplicate_names: duplicate_names).duplicate_names::w", ty: UInt<8> },
src: StatePartIndex<BigSlots>(1), // (0x5) SlotDebugData { name: "", ty: UInt<8> },
},
// at: module-XXXXXXXXXX.rs:1:1
4: Return,
],
..
},
pc: 4,
memory_write_log: [],
memories: StatePart {
value: [],
},
small_slots: StatePart {
value: [],
},
big_slots: StatePart {
value: [
5,
5,
6,
6,
],
},
},
io: Instance {
name: <simulator>::duplicate_names,
instantiated: Module {
name: duplicate_names,
..
},
},
uninitialized_inputs: {},
io_targets: {},
made_initial_step: true,
needs_settle: false,
trace_decls: TraceModule {
name: "duplicate_names",
children: [
TraceWire {
name: "w",
child: TraceUInt {
location: TraceScalarId(0),
name: "w",
ty: UInt<8>,
flow: Duplex,
},
ty: UInt<8>,
},
TraceWire {
name: "w",
child: TraceUInt {
location: TraceScalarId(1),
name: "w",
ty: UInt<8>,
flow: Duplex,
},
ty: UInt<8>,
},
],
},
traces: [
SimTrace {
id: TraceScalarId(0),
kind: BigUInt {
index: StatePartIndex<BigSlots>(0),
ty: UInt<8>,
},
state: 0x05,
last_state: 0x05,
},
SimTrace {
id: TraceScalarId(1),
kind: BigUInt {
index: StatePartIndex<BigSlots>(2),
ty: UInt<8>,
},
state: 0x06,
last_state: 0x06,
},
],
trace_memories: {},
trace_writers: [
Running(
VcdWriter {
finished_init: true,
timescale: 1 ps,
..
},
),
],
instant: 1 μs,
clocks_triggered: [],
..
}

View file

@ -0,0 +1,11 @@
$timescale 1 ps $end
$scope module duplicate_names $end
$var wire 8 ! w $end
$var wire 8 " w_2 $end
$upscope $end
$enddefinitions $end
$dumpvars
b101 !
b110 "
$end
#1000000

View file

@ -24,97 +24,97 @@ $upscope $end
$upscope $end
$scope struct mem $end
$scope struct contents $end
$scope struct [0] $end
$scope struct \[0] $end
$scope struct mem $end
$var reg 8 9 \0 $end
$var reg 8 I \1 $end
$upscope $end
$upscope $end
$scope struct [1] $end
$scope struct \[1] $end
$scope struct mem $end
$var reg 8 : \0 $end
$var reg 8 J \1 $end
$upscope $end
$upscope $end
$scope struct [2] $end
$scope struct \[2] $end
$scope struct mem $end
$var reg 8 ; \0 $end
$var reg 8 K \1 $end
$upscope $end
$upscope $end
$scope struct [3] $end
$scope struct \[3] $end
$scope struct mem $end
$var reg 8 < \0 $end
$var reg 8 L \1 $end
$upscope $end
$upscope $end
$scope struct [4] $end
$scope struct \[4] $end
$scope struct mem $end
$var reg 8 = \0 $end
$var reg 8 M \1 $end
$upscope $end
$upscope $end
$scope struct [5] $end
$scope struct \[5] $end
$scope struct mem $end
$var reg 8 > \0 $end
$var reg 8 N \1 $end
$upscope $end
$upscope $end
$scope struct [6] $end
$scope struct \[6] $end
$scope struct mem $end
$var reg 8 ? \0 $end
$var reg 8 O \1 $end
$upscope $end
$upscope $end
$scope struct [7] $end
$scope struct \[7] $end
$scope struct mem $end
$var reg 8 @ \0 $end
$var reg 8 P \1 $end
$upscope $end
$upscope $end
$scope struct [8] $end
$scope struct \[8] $end
$scope struct mem $end
$var reg 8 A \0 $end
$var reg 8 Q \1 $end
$upscope $end
$upscope $end
$scope struct [9] $end
$scope struct \[9] $end
$scope struct mem $end
$var reg 8 B \0 $end
$var reg 8 R \1 $end
$upscope $end
$upscope $end
$scope struct [10] $end
$scope struct \[10] $end
$scope struct mem $end
$var reg 8 C \0 $end
$var reg 8 S \1 $end
$upscope $end
$upscope $end
$scope struct [11] $end
$scope struct \[11] $end
$scope struct mem $end
$var reg 8 D \0 $end
$var reg 8 T \1 $end
$upscope $end
$upscope $end
$scope struct [12] $end
$scope struct \[12] $end
$scope struct mem $end
$var reg 8 E \0 $end
$var reg 8 U \1 $end
$upscope $end
$upscope $end
$scope struct [13] $end
$scope struct \[13] $end
$scope struct mem $end
$var reg 8 F \0 $end
$var reg 8 V \1 $end
$upscope $end
$upscope $end
$scope struct [14] $end
$scope struct \[14] $end
$scope struct mem $end
$var reg 8 G \0 $end
$var reg 8 W \1 $end
$upscope $end
$upscope $end
$scope struct [15] $end
$scope struct \[15] $end
$scope struct mem $end
$var reg 8 H \0 $end
$var reg 8 X \1 $end

View file

@ -11,31 +11,31 @@ $var wire 1 ' wmask $end
$upscope $end
$scope struct mem $end
$scope struct contents $end
$scope struct [0] $end
$scope struct \[0] $end
$scope struct mem $end
$var string 1 1 \$tag $end
$var reg 1 6 HdlSome $end
$upscope $end
$upscope $end
$scope struct [1] $end
$scope struct \[1] $end
$scope struct mem $end
$var string 1 2 \$tag $end
$var reg 1 7 HdlSome $end
$upscope $end
$upscope $end
$scope struct [2] $end
$scope struct \[2] $end
$scope struct mem $end
$var string 1 3 \$tag $end
$var reg 1 8 HdlSome $end
$upscope $end
$upscope $end
$scope struct [3] $end
$scope struct \[3] $end
$scope struct mem $end
$var string 1 4 \$tag $end
$var reg 1 9 HdlSome $end
$upscope $end
$upscope $end
$scope struct [4] $end
$scope struct \[4] $end
$scope struct mem $end
$var string 1 5 \$tag $end
$var reg 1 : HdlSome $end

View file

@ -42,7 +42,7 @@ $upscope $end
$upscope $end
$scope struct mem $end
$scope struct contents $end
$scope struct [0] $end
$scope struct \[0] $end
$scope struct mem $end
$var reg 8 ] \[0] $end
$var reg 8 e \[1] $end
@ -54,7 +54,7 @@ $var reg 8 /" \[6] $end
$var reg 8 7" \[7] $end
$upscope $end
$upscope $end
$scope struct [1] $end
$scope struct \[1] $end
$scope struct mem $end
$var reg 8 ^ \[0] $end
$var reg 8 f \[1] $end
@ -66,7 +66,7 @@ $var reg 8 0" \[6] $end
$var reg 8 8" \[7] $end
$upscope $end
$upscope $end
$scope struct [2] $end
$scope struct \[2] $end
$scope struct mem $end
$var reg 8 _ \[0] $end
$var reg 8 g \[1] $end
@ -78,7 +78,7 @@ $var reg 8 1" \[6] $end
$var reg 8 9" \[7] $end
$upscope $end
$upscope $end
$scope struct [3] $end
$scope struct \[3] $end
$scope struct mem $end
$var reg 8 ` \[0] $end
$var reg 8 h \[1] $end
@ -90,7 +90,7 @@ $var reg 8 2" \[6] $end
$var reg 8 :" \[7] $end
$upscope $end
$upscope $end
$scope struct [4] $end
$scope struct \[4] $end
$scope struct mem $end
$var reg 8 a \[0] $end
$var reg 8 i \[1] $end
@ -102,7 +102,7 @@ $var reg 8 3" \[6] $end
$var reg 8 ;" \[7] $end
$upscope $end
$upscope $end
$scope struct [5] $end
$scope struct \[5] $end
$scope struct mem $end
$var reg 8 b \[0] $end
$var reg 8 j \[1] $end
@ -114,7 +114,7 @@ $var reg 8 4" \[6] $end
$var reg 8 <" \[7] $end
$upscope $end
$upscope $end
$scope struct [6] $end
$scope struct \[6] $end
$scope struct mem $end
$var reg 8 c \[0] $end
$var reg 8 k \[1] $end
@ -126,7 +126,7 @@ $var reg 8 5" \[6] $end
$var reg 8 =" \[7] $end
$upscope $end
$upscope $end
$scope struct [7] $end
$scope struct \[7] $end
$scope struct mem $end
$var reg 8 d \[0] $end
$var reg 8 l \[1] $end