libre-chip/fayalite
3
0
Fork 2
Code Issues 1 Pull requests Projects Releases Packages Wiki Activity Actions

Compare commits

base: libre-chip:15a28aa7a778dbba5422f6f9e40e8c530fc0e31a
Branches Tags
libre-chip:master
libre-chip:square-brackets-generics-experiment
libre-chip:runtime-generics
libre-chip:type-deduction
libre-chip:v0.2.0
libre-chip:v0.1.0
...
compare: libre-chip:0d54b9a2a9abd7c8b34566ae6e55ca0d508c6a21
Branches Tags
libre-chip:master
libre-chip:square-brackets-generics-experiment
libre-chip:runtime-generics
libre-chip:type-deduction
libre-chip:v0.2.0
libre-chip:v0.1.0

2 commits
15a28aa7a7 ... 0d54b9a2a9

Author SHA1 Message Date
Jacob Lifshay
0d54b9a2a9
queue formal proof passes!
Some checks are pending
/ test (push) Has started running
Details
2024-10-03 23:07:14 -07:00
Jacob Lifshay
343805f80b
fix #[hdl] to work with unusual identifier hygiene from macros 2024-10-03 23:04:14 -07:00
11 changed files with 385 additions and 198 deletions
Download patch file Download diff file Expand all files Collapse all files

109
crates/fayalite-proc-macros-impl/src/hdl_bundle.rs
View file

@ -431,6 +431,7 @@ impl ToTokens for ParsedBundle {
builder_ident, builder_ident,
mask_type_builder_ident, mask_type_builder_ident,
} = self; } = self;
let span = ident.span();
let ItemOptions { let ItemOptions {
outline_generated: _, outline_generated: _,
target, target,
@ -440,7 +441,7 @@ impl ToTokens for ParsedBundle {
} = &options.body; } = &options.body;
let target = get_target(target, ident); let target = get_target(target, ident);
let mut item_attrs = attrs.clone(); let mut item_attrs = attrs.clone();
item_attrs.push(common_derives(ident.span())); item_attrs.push(common_derives(span));
ItemStruct { ItemStruct {
attrs: item_attrs, attrs: item_attrs,
vis: vis.clone(), vis: vis.clone(),
@ -462,19 +463,19 @@ impl ToTokens for ParsedBundle {
.map(|ParsedField { ident, ty, .. }| { .map(|ParsedField { ident, ty, .. }| {
let ident = ident.as_ref().unwrap(); let ident = ident.as_ref().unwrap();
let expr = ty.make_hdl_type_expr(context); let expr = ty.make_hdl_type_expr(context);
quote_spanned! {ident.span()=> quote_spanned! {span=>
#ident: #expr, #ident: #expr,
} }
}) })
.collect(); .collect();
parse_quote_spanned! {ident.span()=> parse_quote_spanned! {span=>
#target { #target {
#(#fields)* #(#fields)*
} }
} }
}) })
} }
let mut wrapped_in_const = WrappedInConst::new(tokens, ident.span()); let mut wrapped_in_const = WrappedInConst::new(tokens, span);
let tokens = wrapped_in_const.inner(); let tokens = wrapped_in_const.inner();
let builder = Builder { let builder = Builder {
vis: vis.clone(), vis: vis.clone(),
@ -488,9 +489,8 @@ impl ToTokens for ParsedBundle {
let unfilled_builder_ty = builder.builder_struct_ty(|_| BuilderFieldState::Unfilled); let unfilled_builder_ty = builder.builder_struct_ty(|_| BuilderFieldState::Unfilled);
let filled_builder_ty = builder.builder_struct_ty(|_| BuilderFieldState::Filled); let filled_builder_ty = builder.builder_struct_ty(|_| BuilderFieldState::Filled);
let mut mask_type_fields = FieldsNamed::from(fields.clone()); let mut mask_type_fields = FieldsNamed::from(fields.clone());
for Field { ident, ty, .. } in &mut mask_type_fields.named { for Field { ty, .. } in &mut mask_type_fields.named {
let ident = ident.as_ref().unwrap(); *ty = parse_quote_spanned! {span=>
*ty = parse_quote_spanned! {ident.span()=>
<#ty as ::fayalite::ty::Type>::MaskType <#ty as ::fayalite::ty::Type>::MaskType
}; };
} }
@ -509,8 +509,8 @@ impl ToTokens for ParsedBundle {
mask_type_builder.builder_struct_ty(|_| BuilderFieldState::Filled); mask_type_builder.builder_struct_ty(|_| BuilderFieldState::Filled);
ItemStruct { ItemStruct {
attrs: vec![ attrs: vec![
common_derives(ident.span()), common_derives(span),
parse_quote_spanned! {ident.span()=> parse_quote_spanned! {span=>
#[allow(non_camel_case_types, dead_code)] #[allow(non_camel_case_types, dead_code)]
}, },
], ],
@ -523,16 +523,15 @@ impl ToTokens for ParsedBundle {
} }
.to_tokens(tokens); .to_tokens(tokens);
let mut mask_type_match_variant_fields = mask_type_fields; let mut mask_type_match_variant_fields = mask_type_fields;
for Field { ident, ty, .. } in &mut mask_type_match_variant_fields.named { for Field { ty, .. } in &mut mask_type_match_variant_fields.named {
let ident = ident.as_ref().unwrap(); *ty = parse_quote_spanned! {span=>
*ty = parse_quote_spanned! {ident.span()=>
::fayalite::expr::Expr<#ty> ::fayalite::expr::Expr<#ty>
}; };
} }
ItemStruct { ItemStruct {
attrs: vec![ attrs: vec![
common_derives(ident.span()), common_derives(span),
parse_quote_spanned! {ident.span()=> parse_quote_spanned! {span=>
#[allow(non_camel_case_types, dead_code)] #[allow(non_camel_case_types, dead_code)]
}, },
], ],
@ -545,16 +544,15 @@ impl ToTokens for ParsedBundle {
} }
.to_tokens(tokens); .to_tokens(tokens);
let mut match_variant_fields = FieldsNamed::from(fields.clone()); let mut match_variant_fields = FieldsNamed::from(fields.clone());
for Field { ident, ty, .. } in &mut match_variant_fields.named { for Field { ty, .. } in &mut match_variant_fields.named {
let ident = ident.as_ref().unwrap(); *ty = parse_quote_spanned! {span=>
*ty = parse_quote_spanned! {ident.span()=>
::fayalite::expr::Expr<#ty> ::fayalite::expr::Expr<#ty>
}; };
} }
ItemStruct { ItemStruct {
attrs: vec![ attrs: vec![
common_derives(ident.span()), common_derives(span),
parse_quote_spanned! {ident.span()=> parse_quote_spanned! {span=>
#[allow(non_camel_case_types, dead_code)] #[allow(non_camel_case_types, dead_code)]
}, },
], ],
@ -566,17 +564,20 @@ impl ToTokens for ParsedBundle {
semi_token: None, semi_token: None,
} }
.to_tokens(tokens); .to_tokens(tokens);
let this_token = Ident::new("__this", span);
let fields_token = Ident::new("__fields", span);
let self_token = Token![self](span);
let match_variant_body_fields = Vec::from_iter(fields.named().into_iter().map(|field| { let match_variant_body_fields = Vec::from_iter(fields.named().into_iter().map(|field| {
let ident: &Ident = field.ident().as_ref().unwrap(); let ident: &Ident = field.ident().as_ref().unwrap();
let ident_str = ident.to_string(); let ident_str = ident.to_string();
quote_spanned! {ident.span()=> quote_spanned! {span=>
#ident: ::fayalite::expr::Expr::field(__this, #ident_str), #ident: ::fayalite::expr::Expr::field(#this_token, #ident_str),
} }
})); }));
let mask_type_body_fields = Vec::from_iter(fields.named().into_iter().map(|field| { let mask_type_body_fields = Vec::from_iter(fields.named().into_iter().map(|field| {
let ident: &Ident = field.ident().as_ref().unwrap(); let ident: &Ident = field.ident().as_ref().unwrap();
quote_spanned! {ident.span()=> quote_spanned! {span=>
#ident: ::fayalite::ty::Type::mask_type(&self.#ident), #ident: ::fayalite::ty::Type::mask_type(&#self_token.#ident),
} }
})); }));
let from_canonical_body_fields = let from_canonical_body_fields =
@ -585,13 +586,13 @@ impl ToTokens for ParsedBundle {
let ident: &Ident = field.ident().as_ref().unwrap(); let ident: &Ident = field.ident().as_ref().unwrap();
let ident_str = ident.to_string(); let ident_str = ident.to_string();
let flipped = flip.is_some(); let flipped = flip.is_some();
quote_spanned! {ident.span()=> quote_spanned! {span=>
#ident: { #ident: {
let ::fayalite::bundle::BundleField { let ::fayalite::bundle::BundleField {
name: __name, name: __name,
flipped: __flipped, flipped: __flipped,
ty: __ty, ty: __ty,
} = __fields[#index]; } = #fields_token[#index];
::fayalite::__std::assert_eq!(&*__name, #ident_str); ::fayalite::__std::assert_eq!(&*__name, #ident_str);
::fayalite::__std::assert_eq!(__flipped, #flipped); ::fayalite::__std::assert_eq!(__flipped, #flipped);
::fayalite::ty::Type::from_canonical(__ty) ::fayalite::ty::Type::from_canonical(__ty)
@ -604,17 +605,17 @@ impl ToTokens for ParsedBundle {
let ident: &Ident = field.ident().as_ref().unwrap(); let ident: &Ident = field.ident().as_ref().unwrap();
let ident_str = ident.to_string(); let ident_str = ident.to_string();
let flipped = flip.is_some(); let flipped = flip.is_some();
quote_spanned! {ident.span()=> quote_spanned! {span=>
::fayalite::bundle::BundleField { ::fayalite::bundle::BundleField {
name: ::fayalite::intern::Intern::intern(#ident_str), name: ::fayalite::intern::Intern::intern(#ident_str),
flipped: #flipped, flipped: #flipped,
ty: ::fayalite::ty::Type::canonical(&self.#ident), ty: ::fayalite::ty::Type::canonical(&#self_token.#ident),
}, },
} }
}, },
)); ));
let fields_len = fields.named().into_iter().len(); let fields_len = fields.named().into_iter().len();
quote_spanned! {ident.span()=> quote_spanned! {span=>
#[automatically_derived] #[automatically_derived]
impl #impl_generics ::fayalite::ty::Type for #mask_type_ident #type_generics impl #impl_generics ::fayalite::ty::Type for #mask_type_ident #type_generics
#where_clause #where_clause
@ -630,7 +631,7 @@ impl ToTokens for ParsedBundle {
<Self as ::fayalite::ty::Type>::MatchVariantAndInactiveScope, <Self as ::fayalite::ty::Type>::MatchVariantAndInactiveScope,
>; >;
fn match_variants( fn match_variants(
__this: ::fayalite::expr::Expr<Self>, #this_token: ::fayalite::expr::Expr<Self>,
__source_location: ::fayalite::source_location::SourceLocation, __source_location: ::fayalite::source_location::SourceLocation,
) -> <Self as ::fayalite::ty::Type>::MatchVariantsIter { ) -> <Self as ::fayalite::ty::Type>::MatchVariantsIter {
let __retval = #mask_type_match_variant_ident { let __retval = #mask_type_match_variant_ident {
@ -638,19 +639,19 @@ impl ToTokens for ParsedBundle {
}; };
::fayalite::__std::iter::once(::fayalite::ty::MatchVariantWithoutScope(__retval)) ::fayalite::__std::iter::once(::fayalite::ty::MatchVariantWithoutScope(__retval))
} }
fn mask_type(&self) -> <Self as ::fayalite::ty::Type>::MaskType { fn mask_type(&#self_token) -> <Self as ::fayalite::ty::Type>::MaskType {
*self *#self_token
} }
fn canonical(&self) -> ::fayalite::ty::CanonicalType { fn canonical(&#self_token) -> ::fayalite::ty::CanonicalType {
::fayalite::ty::Type::canonical(&::fayalite::bundle::Bundle::new(::fayalite::bundle::BundleType::fields(self))) ::fayalite::ty::Type::canonical(&::fayalite::bundle::Bundle::new(::fayalite::bundle::BundleType::fields(#self_token)))
} }
#[track_caller] #[track_caller]
fn from_canonical(__canonical_type: ::fayalite::ty::CanonicalType) -> Self { fn from_canonical(__canonical_type: ::fayalite::ty::CanonicalType) -> Self {
let ::fayalite::ty::CanonicalType::Bundle(__bundle) = __canonical_type else { let ::fayalite::ty::CanonicalType::Bundle(__bundle) = __canonical_type else {
::fayalite::__std::panic!("expected bundle"); ::fayalite::__std::panic!("expected bundle");
}; };
let __fields = ::fayalite::bundle::BundleType::fields(&__bundle); let #fields_token = ::fayalite::bundle::BundleType::fields(&__bundle);
::fayalite::__std::assert_eq!(__fields.len(), #fields_len, "bundle has wrong number of fields"); ::fayalite::__std::assert_eq!(#fields_token.len(), #fields_len, "bundle has wrong number of fields");
Self { Self {
#(#from_canonical_body_fields)* #(#from_canonical_body_fields)*
} }
@ -665,7 +666,7 @@ impl ToTokens for ParsedBundle {
{ {
type Builder = #unfilled_mask_type_builder_ty; type Builder = #unfilled_mask_type_builder_ty;
type FilledBuilder = #filled_mask_type_builder_ty; type FilledBuilder = #filled_mask_type_builder_ty;
fn fields(&self) -> ::fayalite::intern::Interned<[::fayalite::bundle::BundleField]> { fn fields(&#self_token) -> ::fayalite::intern::Interned<[::fayalite::bundle::BundleField]> {
::fayalite::intern::Intern::intern(&[#(#fields_body_fields)*][..]) ::fayalite::intern::Intern::intern(&[#(#fields_body_fields)*][..])
} }
} }
@ -680,8 +681,8 @@ impl ToTokens for ParsedBundle {
impl #impl_generics ::fayalite::ty::TypeWithDeref for #mask_type_ident #type_generics impl #impl_generics ::fayalite::ty::TypeWithDeref for #mask_type_ident #type_generics
#where_clause #where_clause
{ {
fn expr_deref(__this: &::fayalite::expr::Expr<Self>) -> &<Self as ::fayalite::ty::Type>::MatchVariant { fn expr_deref(#this_token: &::fayalite::expr::Expr<Self>) -> &<Self as ::fayalite::ty::Type>::MatchVariant {
let __this = *__this; let #this_token = *#this_token;
let __retval = #mask_type_match_variant_ident { let __retval = #mask_type_match_variant_ident {
#(#match_variant_body_fields)* #(#match_variant_body_fields)*
}; };
@ -703,7 +704,7 @@ impl ToTokens for ParsedBundle {
<Self as ::fayalite::ty::Type>::MatchVariantAndInactiveScope, <Self as ::fayalite::ty::Type>::MatchVariantAndInactiveScope,
>; >;
fn match_variants( fn match_variants(
__this: ::fayalite::expr::Expr<Self>, #this_token: ::fayalite::expr::Expr<Self>,
__source_location: ::fayalite::source_location::SourceLocation, __source_location: ::fayalite::source_location::SourceLocation,
) -> <Self as ::fayalite::ty::Type>::MatchVariantsIter { ) -> <Self as ::fayalite::ty::Type>::MatchVariantsIter {
let __retval = #match_variant_ident { let __retval = #match_variant_ident {
@ -711,21 +712,21 @@ impl ToTokens for ParsedBundle {
}; };
::fayalite::__std::iter::once(::fayalite::ty::MatchVariantWithoutScope(__retval)) ::fayalite::__std::iter::once(::fayalite::ty::MatchVariantWithoutScope(__retval))
} }
fn mask_type(&self) -> <Self as ::fayalite::ty::Type>::MaskType { fn mask_type(&#self_token) -> <Self as ::fayalite::ty::Type>::MaskType {
#mask_type_ident { #mask_type_ident {
#(#mask_type_body_fields)* #(#mask_type_body_fields)*
} }
} }
fn canonical(&self) -> ::fayalite::ty::CanonicalType { fn canonical(&#self_token) -> ::fayalite::ty::CanonicalType {
::fayalite::ty::Type::canonical(&::fayalite::bundle::Bundle::new(::fayalite::bundle::BundleType::fields(self))) ::fayalite::ty::Type::canonical(&::fayalite::bundle::Bundle::new(::fayalite::bundle::BundleType::fields(#self_token)))
} }
#[track_caller] #[track_caller]
fn from_canonical(__canonical_type: ::fayalite::ty::CanonicalType) -> Self { fn from_canonical(__canonical_type: ::fayalite::ty::CanonicalType) -> Self {
let ::fayalite::ty::CanonicalType::Bundle(__bundle) = __canonical_type else { let ::fayalite::ty::CanonicalType::Bundle(__bundle) = __canonical_type else {
::fayalite::__std::panic!("expected bundle"); ::fayalite::__std::panic!("expected bundle");
}; };
let __fields = ::fayalite::bundle::BundleType::fields(&__bundle); let #fields_token = ::fayalite::bundle::BundleType::fields(&__bundle);
::fayalite::__std::assert_eq!(__fields.len(), #fields_len, "bundle has wrong number of fields"); ::fayalite::__std::assert_eq!(#fields_token.len(), #fields_len, "bundle has wrong number of fields");
Self { Self {
#(#from_canonical_body_fields)* #(#from_canonical_body_fields)*
} }
@ -740,7 +741,7 @@ impl ToTokens for ParsedBundle {
{ {
type Builder = #unfilled_builder_ty; type Builder = #unfilled_builder_ty;
type FilledBuilder = #filled_builder_ty; type FilledBuilder = #filled_builder_ty;
fn fields(&self) -> ::fayalite::intern::Interned<[::fayalite::bundle::BundleField]> { fn fields(&#self_token) -> ::fayalite::intern::Interned<[::fayalite::bundle::BundleField]> {
::fayalite::intern::Intern::intern(&[#(#fields_body_fields)*][..]) ::fayalite::intern::Intern::intern(&[#(#fields_body_fields)*][..])
} }
} }
@ -755,8 +756,8 @@ impl ToTokens for ParsedBundle {
impl #impl_generics ::fayalite::ty::TypeWithDeref for #target #type_generics impl #impl_generics ::fayalite::ty::TypeWithDeref for #target #type_generics
#where_clause #where_clause
{ {
fn expr_deref(__this: &::fayalite::expr::Expr<Self>) -> &<Self as ::fayalite::ty::Type>::MatchVariant { fn expr_deref(#this_token: &::fayalite::expr::Expr<Self>) -> &<Self as ::fayalite::ty::Type>::MatchVariant {
let __this = *__this; let #this_token = *#this_token;
let __retval = #match_variant_ident { let __retval = #match_variant_ident {
#(#match_variant_body_fields)* #(#match_variant_body_fields)*
}; };
@ -772,7 +773,7 @@ impl ToTokens for ParsedBundle {
let static_type_body_fields = Vec::from_iter(fields.named().into_iter().map(|field| { let static_type_body_fields = Vec::from_iter(fields.named().into_iter().map(|field| {
let ident: &Ident = field.ident().as_ref().unwrap(); let ident: &Ident = field.ident().as_ref().unwrap();
let ty = field.ty(); let ty = field.ty();
quote_spanned! {ident.span()=> quote_spanned! {span=>
#ident: <#ty as ::fayalite::ty::StaticType>::TYPE, #ident: <#ty as ::fayalite::ty::StaticType>::TYPE,
} }
})); }));
@ -780,28 +781,26 @@ impl ToTokens for ParsedBundle {
Vec::from_iter(fields.named().into_iter().map(|field| { Vec::from_iter(fields.named().into_iter().map(|field| {
let ident: &Ident = field.ident().as_ref().unwrap(); let ident: &Ident = field.ident().as_ref().unwrap();
let ty = field.ty(); let ty = field.ty();
quote_spanned! {ident.span()=> quote_spanned! {span=>
#ident: <#ty as ::fayalite::ty::StaticType>::MASK_TYPE, #ident: <#ty as ::fayalite::ty::StaticType>::MASK_TYPE,
} }
})); }));
let type_properties = format_ident!("__type_properties", span = ident.span()); let type_properties = format_ident!("__type_properties", span = span);
let type_properties_fields = Vec::from_iter(fields.named().into_iter().zip(field_flips).map(|(field, field_flip)| { let type_properties_fields = Vec::from_iter(fields.named().into_iter().zip(field_flips).map(|(field, field_flip)| {
let ident: &Ident = field.ident().as_ref().unwrap();
let flipped = field_flip.is_some(); let flipped = field_flip.is_some();
let ty = field.ty(); let ty = field.ty();
quote_spanned! {ident.span()=> quote_spanned! {span=>
let #type_properties = #type_properties.field(#flipped, <#ty as ::fayalite::ty::StaticType>::TYPE_PROPERTIES); let #type_properties = #type_properties.field(#flipped, <#ty as ::fayalite::ty::StaticType>::TYPE_PROPERTIES);
} }
})); }));
let type_properties_mask_fields = Vec::from_iter(fields.named().into_iter().zip(field_flips).map(|(field, field_flip)| { let type_properties_mask_fields = Vec::from_iter(fields.named().into_iter().zip(field_flips).map(|(field, field_flip)| {
let ident: &Ident = field.ident().as_ref().unwrap();
let flipped = field_flip.is_some(); let flipped = field_flip.is_some();
let ty = field.ty(); let ty = field.ty();
quote_spanned! {ident.span()=> quote_spanned! {span=>
let #type_properties = #type_properties.field(#flipped, <#ty as ::fayalite::ty::StaticType>::MASK_TYPE_PROPERTIES); let #type_properties = #type_properties.field(#flipped, <#ty as ::fayalite::ty::StaticType>::MASK_TYPE_PROPERTIES);
} }
})); }));
quote_spanned! {ident.span()=> quote_spanned! {span=>
#[automatically_derived] #[automatically_derived]
impl #static_impl_generics ::fayalite::ty::StaticType for #mask_type_ident #static_type_generics impl #static_impl_generics ::fayalite::ty::StaticType for #mask_type_ident #static_type_generics
#static_where_clause #static_where_clause

96
crates/fayalite-proc-macros-impl/src/hdl_enum.rs
View file

@ -204,6 +204,7 @@ impl ToTokens for ParsedEnum {
variants, variants,
match_variant_ident, match_variant_ident,
} = self; } = self;
let span = ident.span();
let ItemOptions { let ItemOptions {
outline_generated: _, outline_generated: _,
target, target,
@ -213,8 +214,8 @@ impl ToTokens for ParsedEnum {
} = &options.body; } = &options.body;
let target = get_target(target, ident); let target = get_target(target, ident);
let mut struct_attrs = attrs.clone(); let mut struct_attrs = attrs.clone();
struct_attrs.push(common_derives(ident.span())); struct_attrs.push(common_derives(span));
struct_attrs.push(parse_quote_spanned! {ident.span()=> struct_attrs.push(parse_quote_spanned! {span=>
#[allow(non_snake_case)] #[allow(non_snake_case)]
}); });
let struct_fields = Punctuated::from_iter(variants.pairs().map_pair_value_ref( let struct_fields = Punctuated::from_iter(variants.pairs().map_pair_value_ref(
@ -238,8 +239,8 @@ impl ToTokens for ParsedEnum {
colon_token = Token![:](paren_token.span.open()); colon_token = Token![:](paren_token.span.open());
ty.clone().into() ty.clone().into()
} else { } else {
colon_token = Token![:](ident.span()); colon_token = Token![:](span);
parse_quote_spanned! {ident.span()=> parse_quote_spanned! {span=>
() ()
} }
}; };
@ -282,30 +283,30 @@ impl ToTokens for ParsedEnum {
}) = field }) = field
{ {
let expr = ty.make_hdl_type_expr(context); let expr = ty.make_hdl_type_expr(context);
quote_spanned! {ident.span()=> quote_spanned! {span=>
#ident: #expr, #ident: #expr,
} }
} else { } else {
quote_spanned! {ident.span()=> quote_spanned! {span=>
#ident: (), #ident: (),
} }
} }
}) })
.collect(); .collect();
parse_quote_spanned! {ident.span()=> parse_quote_spanned! {span=>
#target { #target {
#(#fields)* #(#fields)*
} }
} }
}) })
} }
let mut wrapped_in_const = WrappedInConst::new(tokens, ident.span()); let mut wrapped_in_const = WrappedInConst::new(tokens, span);
let tokens = wrapped_in_const.inner(); let tokens = wrapped_in_const.inner();
{ {
let mut wrapped_in_const = WrappedInConst::new(tokens, ident.span()); let mut wrapped_in_const = WrappedInConst::new(tokens, span);
let tokens = wrapped_in_const.inner(); let tokens = wrapped_in_const.inner();
let mut enum_attrs = attrs.clone(); let mut enum_attrs = attrs.clone();
enum_attrs.push(parse_quote_spanned! {ident.span()=> enum_attrs.push(parse_quote_spanned! {span=>
#[allow(dead_code)] #[allow(dead_code)]
}); });
ItemEnum { ItemEnum {
@ -354,7 +355,7 @@ impl ToTokens for ParsedEnum {
.to_tokens(tokens); .to_tokens(tokens);
} }
let mut enum_attrs = attrs.clone(); let mut enum_attrs = attrs.clone();
enum_attrs.push(parse_quote_spanned! {ident.span()=> enum_attrs.push(parse_quote_spanned! {span=>
#[allow(dead_code, non_camel_case_types)] #[allow(dead_code, non_camel_case_types)]
}); });
ItemEnum { ItemEnum {
@ -389,7 +390,7 @@ impl ToTokens for ParsedEnum {
mutability: FieldMutability::None, mutability: FieldMutability::None,
ident: None, ident: None,
colon_token: None, colon_token: None,
ty: parse_quote_spanned! {ident.span()=> ty: parse_quote_spanned! {span=>
::fayalite::expr::Expr<#ty> ::fayalite::expr::Expr<#ty>
}, },
}, },
@ -403,21 +404,22 @@ impl ToTokens for ParsedEnum {
)), )),
} }
.to_tokens(tokens); .to_tokens(tokens);
let self_token = Token![self](span);
for (index, ParsedVariant { ident, field, .. }) in variants.iter().enumerate() { for (index, ParsedVariant { ident, field, .. }) in variants.iter().enumerate() {
if let Some(ParsedVariantField { ty, .. }) = field { if let Some(ParsedVariantField { ty, .. }) = field {
quote_spanned! {ident.span()=> quote_spanned! {span=>
#[automatically_derived] #[automatically_derived]
impl #impl_generics #target #type_generics impl #impl_generics #target #type_generics
#where_clause #where_clause
{ {
#[allow(non_snake_case, dead_code)] #[allow(non_snake_case, dead_code)]
#vis fn #ident<__V: ::fayalite::expr::ToExpr<Type = #ty>>( #vis fn #ident<__V: ::fayalite::expr::ToExpr<Type = #ty>>(
self, #self_token,
v: __V, v: __V,
) -> ::fayalite::expr::Expr<Self> { ) -> ::fayalite::expr::Expr<Self> {
::fayalite::expr::ToExpr::to_expr( ::fayalite::expr::ToExpr::to_expr(
&::fayalite::expr::ops::EnumLiteral::new_by_index( &::fayalite::expr::ops::EnumLiteral::new_by_index(
self, #self_token,
#index, #index,
::fayalite::__std::option::Option::Some( ::fayalite::__std::option::Option::Some(
::fayalite::expr::Expr::canonical( ::fayalite::expr::Expr::canonical(
@ -430,16 +432,16 @@ impl ToTokens for ParsedEnum {
} }
} }
} else { } else {
quote_spanned! {ident.span()=> quote_spanned! {span=>
#[automatically_derived] #[automatically_derived]
impl #impl_generics #target #type_generics impl #impl_generics #target #type_generics
#where_clause #where_clause
{ {
#[allow(non_snake_case, dead_code)] #[allow(non_snake_case, dead_code)]
#vis fn #ident(self) -> ::fayalite::expr::Expr<Self> { #vis fn #ident(#self_token) -> ::fayalite::expr::Expr<Self> {
::fayalite::expr::ToExpr::to_expr( ::fayalite::expr::ToExpr::to_expr(
&::fayalite::expr::ops::EnumLiteral::new_by_index( &::fayalite::expr::ops::EnumLiteral::new_by_index(
self, #self_token,
#index, #index,
::fayalite::__std::option::Option::None, ::fayalite::__std::option::Option::None,
), ),
@ -450,46 +452,48 @@ impl ToTokens for ParsedEnum {
} }
.to_tokens(tokens); .to_tokens(tokens);
} }
let variants_token = Ident::new("variants", span);
let from_canonical_body_fields = Vec::from_iter(variants.iter().enumerate().map( let from_canonical_body_fields = Vec::from_iter(variants.iter().enumerate().map(
|(index, ParsedVariant { ident, field, .. })| { |(index, ParsedVariant { ident, field, .. })| {
let ident_str = ident.to_string(); let ident_str = ident.to_string();
let val = if field.is_some() { let val = if field.is_some() {
let missing_value_msg = format!("expected variant {ident} to have a field"); let missing_value_msg = format!("expected variant {ident} to have a field");
quote_spanned! {ident.span()=> quote_spanned! {span=>
::fayalite::ty::Type::from_canonical(ty.expect(#missing_value_msg)) ::fayalite::ty::Type::from_canonical(ty.expect(#missing_value_msg))
} }
} else { } else {
quote_spanned! {ident.span()=> quote_spanned! {span=>
::fayalite::__std::assert!(ty.is_none()); ::fayalite::__std::assert!(ty.is_none());
} }
}; };
quote_spanned! {ident.span()=> quote_spanned! {span=>
#ident: { #ident: {
let ::fayalite::enum_::EnumVariant { let ::fayalite::enum_::EnumVariant {
name, name,
ty, ty,
} = variants[#index]; } = #variants_token[#index];
::fayalite::__std::assert_eq!(&*name, #ident_str); ::fayalite::__std::assert_eq!(&*name, #ident_str);
#val #val
}, },
} }
}, },
)); ));
let variant_access_token = Ident::new("variant_access", span);
let match_active_scope_match_arms = Vec::from_iter(variants.iter().enumerate().map( let match_active_scope_match_arms = Vec::from_iter(variants.iter().enumerate().map(
|(index, ParsedVariant { ident, field, .. })| { |(index, ParsedVariant { ident, field, .. })| {
if field.is_some() { if field.is_some() {
quote_spanned! {ident.span()=> quote_spanned! {span=>
#index => #match_variant_ident::#ident( #index => #match_variant_ident::#ident(
::fayalite::expr::ToExpr::to_expr( ::fayalite::expr::ToExpr::to_expr(
&::fayalite::expr::ops::VariantAccess::new_by_index( &::fayalite::expr::ops::VariantAccess::new_by_index(
variant_access.base(), #variant_access_token.base(),
variant_access.variant_index(), #variant_access_token.variant_index(),
), ),
), ),
), ),
} }
} else { } else {
quote_spanned! {ident.span()=> quote_spanned! {span=>
#index => #match_variant_ident::#ident, #index => #match_variant_ident::#ident,
} }
} }
@ -507,16 +511,16 @@ impl ToTokens for ParsedEnum {
match field { match field {
Some(ParsedVariantField { options, .. }) => { Some(ParsedVariantField { options, .. }) => {
let FieldOptions {} = options.body; let FieldOptions {} = options.body;
quote_spanned! {ident.span()=> quote_spanned! {span=>
::fayalite::enum_::EnumVariant { ::fayalite::enum_::EnumVariant {
name: ::fayalite::intern::Intern::intern(#ident_str), name: ::fayalite::intern::Intern::intern(#ident_str),
ty: ::fayalite::__std::option::Option::Some( ty: ::fayalite::__std::option::Option::Some(
::fayalite::ty::Type::canonical(&self.#ident), ::fayalite::ty::Type::canonical(&#self_token.#ident),
), ),
}, },
} }
} }
None => quote_spanned! {ident.span()=> None => quote_spanned! {span=>
::fayalite::enum_::EnumVariant { ::fayalite::enum_::EnumVariant {
name: ::fayalite::intern::Intern::intern(#ident_str), name: ::fayalite::intern::Intern::intern(#ident_str),
ty: ::fayalite::__std::option::Option::None, ty: ::fayalite::__std::option::Option::None,
@ -526,7 +530,7 @@ impl ToTokens for ParsedEnum {
}, },
)); ));
let variants_len = variants.len(); let variants_len = variants.len();
quote_spanned! {ident.span()=> quote_spanned! {span=>
#[automatically_derived] #[automatically_derived]
impl #impl_generics ::fayalite::ty::Type for #target #type_generics impl #impl_generics ::fayalite::ty::Type for #target #type_generics
#where_clause #where_clause
@ -544,11 +548,11 @@ impl ToTokens for ParsedEnum {
) -> <Self as ::fayalite::ty::Type>::MatchVariantsIter { ) -> <Self as ::fayalite::ty::Type>::MatchVariantsIter {
::fayalite::module::enum_match_variants_helper(this, source_location) ::fayalite::module::enum_match_variants_helper(this, source_location)
} }
fn mask_type(&self) -> <Self as ::fayalite::ty::Type>::MaskType { fn mask_type(&#self_token) -> <Self as ::fayalite::ty::Type>::MaskType {
::fayalite::int::Bool ::fayalite::int::Bool
} }
fn canonical(&self) -> ::fayalite::ty::CanonicalType { fn canonical(&#self_token) -> ::fayalite::ty::CanonicalType {
::fayalite::ty::CanonicalType::Enum(::fayalite::enum_::Enum::new(::fayalite::enum_::EnumType::variants(self))) ::fayalite::ty::CanonicalType::Enum(::fayalite::enum_::Enum::new(::fayalite::enum_::EnumType::variants(#self_token)))
} }
#[track_caller] #[track_caller]
#[allow(non_snake_case)] #[allow(non_snake_case)]
@ -556,8 +560,8 @@ impl ToTokens for ParsedEnum {
let ::fayalite::ty::CanonicalType::Enum(enum_) = canonical_type else { let ::fayalite::ty::CanonicalType::Enum(enum_) = canonical_type else {
::fayalite::__std::panic!("expected enum"); ::fayalite::__std::panic!("expected enum");
}; };
let variants = ::fayalite::enum_::EnumType::variants(&enum_); let #variants_token = ::fayalite::enum_::EnumType::variants(&enum_);
::fayalite::__std::assert_eq!(variants.len(), #variants_len, "enum has wrong number of variants"); ::fayalite::__std::assert_eq!(#variants_token.len(), #variants_len, "enum has wrong number of variants");
Self { Self {
#(#from_canonical_body_fields)* #(#from_canonical_body_fields)*
} }
@ -573,16 +577,16 @@ impl ToTokens for ParsedEnum {
fn match_activate_scope( fn match_activate_scope(
v: <Self as ::fayalite::ty::Type>::MatchVariantAndInactiveScope, v: <Self as ::fayalite::ty::Type>::MatchVariantAndInactiveScope,
) -> (<Self as ::fayalite::ty::Type>::MatchVariant, <Self as ::fayalite::ty::Type>::MatchActiveScope) { ) -> (<Self as ::fayalite::ty::Type>::MatchVariant, <Self as ::fayalite::ty::Type>::MatchActiveScope) {
let (variant_access, scope) = v.activate(); let (#variant_access_token, scope) = v.activate();
( (
match variant_access.variant_index() { match #variant_access_token.variant_index() {
#(#match_active_scope_match_arms)* #(#match_active_scope_match_arms)*
#variants_len.. => ::fayalite::__std::panic!("invalid variant index"), #variants_len.. => ::fayalite::__std::panic!("invalid variant index"),
}, },
scope, scope,
) )
} }
fn variants(&self) -> ::fayalite::intern::Interned<[::fayalite::enum_::EnumVariant]> { fn variants(&#self_token) -> ::fayalite::intern::Interned<[::fayalite::enum_::EnumVariant]> {
::fayalite::intern::Intern::intern(&[ ::fayalite::intern::Intern::intern(&[
#(#variants_body_variants)* #(#variants_body_variants)*
][..]) ][..])
@ -597,34 +601,34 @@ impl ToTokens for ParsedEnum {
let static_type_body_variants = let static_type_body_variants =
Vec::from_iter(variants.iter().map(|ParsedVariant { ident, field, .. }| { Vec::from_iter(variants.iter().map(|ParsedVariant { ident, field, .. }| {
if let Some(_) = field { if let Some(_) = field {
quote_spanned! {ident.span()=> quote_spanned! {span=>
#ident: ::fayalite::ty::StaticType::TYPE, #ident: ::fayalite::ty::StaticType::TYPE,
} }
} else { } else {
quote_spanned! {ident.span()=> quote_spanned! {span=>
#ident: (), #ident: (),
} }
} }
})); }));
let type_properties = format_ident!("__type_properties", span = ident.span()); let type_properties = format_ident!("__type_properties", span = span);
let type_properties_variants = let type_properties_variants =
Vec::from_iter(variants.iter().map(|ParsedVariant { ident, field, .. }| { Vec::from_iter(variants.iter().map(|ParsedVariant { field, .. }| {
let variant = if let Some(ParsedVariantField { ty, .. }) = field { let variant = if let Some(ParsedVariantField { ty, .. }) = field {
quote_spanned! {ident.span()=> quote_spanned! {span=>
::fayalite::__std::option::Option::Some( ::fayalite::__std::option::Option::Some(
<#ty as ::fayalite::ty::StaticType>::TYPE_PROPERTIES, <#ty as ::fayalite::ty::StaticType>::TYPE_PROPERTIES,
) )
} }
} else { } else {
quote_spanned! {ident.span()=> quote_spanned! {span=>
::fayalite::__std::option::Option::None ::fayalite::__std::option::Option::None
} }
}; };
quote_spanned! {ident.span()=> quote_spanned! {span=>
let #type_properties = #type_properties.variant(#variant); let #type_properties = #type_properties.variant(#variant);
} }
})); }));
quote_spanned! {ident.span()=> quote_spanned! {span=>
#[automatically_derived] #[automatically_derived]
impl #static_impl_generics ::fayalite::ty::StaticType impl #static_impl_generics ::fayalite::ty::StaticType
for #target #static_type_generics for #target #static_type_generics

39
crates/fayalite-proc-macros-impl/src/hdl_type_common.rs
View file

@ -1896,6 +1896,7 @@ pub(crate) mod known_items {
impl_known_item!(::fayalite::array::ArrayType); impl_known_item!(::fayalite::array::ArrayType);
impl_known_item!(::fayalite::bundle::BundleType); impl_known_item!(::fayalite::bundle::BundleType);
impl_known_item!(::fayalite::enum_::EnumType); impl_known_item!(::fayalite::enum_::EnumType);
impl_known_item!(::fayalite::int::BoolOrIntType);
impl_known_item!(::fayalite::int::DynSize); impl_known_item!(::fayalite::int::DynSize);
impl_known_item!(::fayalite::int::IntType); impl_known_item!(::fayalite::int::IntType);
impl_known_item!(::fayalite::int::KnownSize); impl_known_item!(::fayalite::int::KnownSize);
@ -2085,6 +2086,7 @@ macro_rules! impl_bounds {
impl_bounds! { impl_bounds! {
#[struct = ParsedBounds] #[struct = ParsedBounds]
pub(crate) enum ParsedBound { pub(crate) enum ParsedBound {
BoolOrIntType,
BundleType, BundleType,
EnumType, EnumType,
IntType, IntType,
@ -2098,6 +2100,7 @@ impl_bounds! {
impl_bounds! { impl_bounds! {
#[struct = ParsedTypeBounds] #[struct = ParsedTypeBounds]
pub(crate) enum ParsedTypeBound { pub(crate) enum ParsedTypeBound {
BoolOrIntType,
BundleType, BundleType,
EnumType, EnumType,
IntType, IntType,
@ -2109,6 +2112,7 @@ impl_bounds! {
impl From<ParsedTypeBound> for ParsedBound { impl From<ParsedTypeBound> for ParsedBound {
fn from(value: ParsedTypeBound) -> Self { fn from(value: ParsedTypeBound) -> Self {
match value { match value {
ParsedTypeBound::BoolOrIntType(v) => ParsedBound::BoolOrIntType(v),
ParsedTypeBound::BundleType(v) => ParsedBound::BundleType(v), ParsedTypeBound::BundleType(v) => ParsedBound::BundleType(v),
ParsedTypeBound::EnumType(v) => ParsedBound::EnumType(v), ParsedTypeBound::EnumType(v) => ParsedBound::EnumType(v),
ParsedTypeBound::IntType(v) => ParsedBound::IntType(v), ParsedTypeBound::IntType(v) => ParsedBound::IntType(v),
@ -2121,6 +2125,7 @@ impl From<ParsedTypeBound> for ParsedBound {
impl From<ParsedTypeBounds> for ParsedBounds { impl From<ParsedTypeBounds> for ParsedBounds {
fn from(value: ParsedTypeBounds) -> Self { fn from(value: ParsedTypeBounds) -> Self {
let ParsedTypeBounds { let ParsedTypeBounds {
BoolOrIntType,
BundleType, BundleType,
EnumType, EnumType,
IntType, IntType,
@ -2128,6 +2133,7 @@ impl From<ParsedTypeBounds> for ParsedBounds {
Type, Type,
} = value; } = value;
Self { Self {
BoolOrIntType,
BundleType, BundleType,
EnumType, EnumType,
IntType, IntType,
@ -2143,6 +2149,10 @@ impl ParsedTypeBound {
fn implied_bounds(self) -> ParsedTypeBounds { fn implied_bounds(self) -> ParsedTypeBounds {
let span = self.span(); let span = self.span();
match self { match self {
Self::BoolOrIntType(v) => ParsedTypeBounds::from_iter([
ParsedTypeBound::from(v),
ParsedTypeBound::Type(known_items::Type(span)),
]),
Self::BundleType(v) => ParsedTypeBounds::from_iter([ Self::BundleType(v) => ParsedTypeBounds::from_iter([
ParsedTypeBound::from(v), ParsedTypeBound::from(v),
ParsedTypeBound::Type(known_items::Type(span)), ParsedTypeBound::Type(known_items::Type(span)),
@ -2153,6 +2163,7 @@ impl ParsedTypeBound {
]), ]),
Self::IntType(v) => ParsedTypeBounds::from_iter([ Self::IntType(v) => ParsedTypeBounds::from_iter([
ParsedTypeBound::from(v), ParsedTypeBound::from(v),
ParsedTypeBound::BoolOrIntType(known_items::BoolOrIntType(span)),
ParsedTypeBound::Type(known_items::Type(span)), ParsedTypeBound::Type(known_items::Type(span)),
]), ]),
Self::StaticType(v) => ParsedTypeBounds::from_iter([ Self::StaticType(v) => ParsedTypeBounds::from_iter([
@ -2185,6 +2196,7 @@ impl From<ParsedSizeTypeBounds> for ParsedBounds {
fn from(value: ParsedSizeTypeBounds) -> Self { fn from(value: ParsedSizeTypeBounds) -> Self {
let ParsedSizeTypeBounds { KnownSize, Size } = value; let ParsedSizeTypeBounds { KnownSize, Size } = value;
Self { Self {
BoolOrIntType: None,
BundleType: None, BundleType: None,
EnumType: None, EnumType: None,
IntType: None, IntType: None,
@ -2260,6 +2272,7 @@ pub(crate) enum ParsedBoundCategory {
impl ParsedBound { impl ParsedBound {
fn categorize(self) -> ParsedBoundCategory { fn categorize(self) -> ParsedBoundCategory {
match self { match self {
Self::BoolOrIntType(v) => ParsedBoundCategory::Type(ParsedTypeBound::BoolOrIntType(v)),
Self::BundleType(v) => ParsedBoundCategory::Type(ParsedTypeBound::BundleType(v)), Self::BundleType(v) => ParsedBoundCategory::Type(ParsedTypeBound::BundleType(v)),
Self::EnumType(v) => ParsedBoundCategory::Type(ParsedTypeBound::EnumType(v)), Self::EnumType(v) => ParsedBoundCategory::Type(ParsedTypeBound::EnumType(v)),
Self::IntType(v) => ParsedBoundCategory::Type(ParsedTypeBound::IntType(v)), Self::IntType(v) => ParsedBoundCategory::Type(ParsedTypeBound::IntType(v)),
@ -2575,6 +2588,7 @@ impl ParsedGenerics {
} }
}) })
.collect(); .collect();
let param_token = Ident::new("__param", ident.span());
for (param_count, (generics_accumulation_type, next_param)) in generics_accumulation_types for (param_count, (generics_accumulation_type, next_param)) in generics_accumulation_types
.iter() .iter()
.zip(&self.params) .zip(&self.params)
@ -2623,7 +2637,7 @@ impl ParsedGenerics {
next_generics.split_for_impl(); next_generics.split_for_impl();
let next_turbofish = next_type_generics.as_turbofish(); let next_turbofish = next_type_generics.as_turbofish();
let mut param: Expr = parse_quote_spanned! {ident.span()=> let mut param: Expr = parse_quote_spanned! {ident.span()=>
__param #param_token
}; };
let mut generics = next_generics.clone(); let mut generics = next_generics.clone();
let mut index_type = param_ident.clone(); let mut index_type = param_ident.clone();
@ -2638,7 +2652,7 @@ impl ParsedGenerics {
is_const: false, is_const: false,
}); });
param = parse_quote_spanned! {ident.span()=> param = parse_quote_spanned! {ident.span()=>
::fayalite::ty::TypeOrDefault::get(__param, || #default_expr) ::fayalite::ty::TypeOrDefault::get(#param_token, || #default_expr)
}; };
let context = MakeHdlTypeExprContext { let context = MakeHdlTypeExprContext {
named_param_values: self_members[..param_count] named_param_values: self_members[..param_count]
@ -2703,7 +2717,7 @@ impl ParsedGenerics {
{ {
type Output = #next_target #next_type_generics; type Output = #next_target #next_type_generics;
fn index(&self, __param: #index_type) -> &Self::Output { fn index(&self, #param_token: #index_type) -> &Self::Output {
::fayalite::intern::Interned::<_>::into_inner( ::fayalite::intern::Interned::<_>::into_inner(
::fayalite::intern::Intern::intern_sized(#output_expr), ::fayalite::intern::Intern::intern_sized(#output_expr),
) )
@ -2724,7 +2738,7 @@ impl ParsedGenerics {
.iter() .iter()
.cloned() .cloned()
.chain([parse_quote_spanned! {ident.span()=> .chain([parse_quote_spanned! {ident.span()=>
__param #param_token
}]) }])
.collect(), .collect(),
is_const: false, is_const: false,
@ -2763,7 +2777,7 @@ impl ParsedGenerics {
{ {
type Output = #next_target #next_target_args; type Output = #next_target #next_target_args;
fn index(&self, __param: #param_ident) -> &Self::Output { fn index(&self, #param_token: #param_ident) -> &Self::Output {
::fayalite::intern::Interned::<_>::into_inner( ::fayalite::intern::Interned::<_>::into_inner(
::fayalite::intern::Intern::intern_sized(#output_expr), ::fayalite::intern::Intern::intern_sized(#output_expr),
) )
@ -2791,7 +2805,7 @@ impl ParsedGenerics {
.iter() .iter()
.cloned() .cloned()
.chain([parse_quote_spanned! {ident.span()=> .chain([parse_quote_spanned! {ident.span()=>
__param #param_token
}]) }])
.collect(), .collect(),
is_const: false, is_const: false,
@ -2833,7 +2847,7 @@ impl ParsedGenerics {
{ {
type Output = #next_target #next_target_args; type Output = #next_target #next_target_args;
fn index(&self, __param: __Param) -> &Self::Output { fn index(&self, #param_token: __Param) -> &Self::Output {
::fayalite::intern::Interned::<_>::into_inner( ::fayalite::intern::Interned::<_>::into_inner(
::fayalite::intern::Intern::intern_sized(#output_expr), ::fayalite::intern::Intern::intern_sized(#output_expr),
) )
@ -3145,16 +3159,21 @@ impl ParsedGenerics {
.Type .Type
.get_or_insert_with(|| known_items::Type(bound.span())); .get_or_insert_with(|| known_items::Type(bound.span()));
match bound { match bound {
ParsedTypeBound::BundleType(_) ParsedTypeBound::BoolOrIntType(_)
| ParsedTypeBound::BundleType(_)
| ParsedTypeBound::EnumType(_) | ParsedTypeBound::EnumType(_)
| ParsedTypeBound::IntType(_) => { | ParsedTypeBound::IntType(_) => {
errors.error(bound, "bound on mask type not implemented"); errors.error(bound, "bound on mask type not implemented");
} }
ParsedTypeBound::StaticType(bound) => { ParsedTypeBound::StaticType(bound) => {
if bounds.StaticType.is_none() { if bounds.StaticType.is_none() {
errors.error(bound, "StaticType bound on mask type without corresponding StaticType bound on original type is not implemented"); errors.error(
bound,
"StaticType bound on mask type without corresponding \
StaticType bound on original type is not implemented",
);
} }
}, }
ParsedTypeBound::Type(_) => {} ParsedTypeBound::Type(_) => {}
} }
} }

2
crates/fayalite/src/cli.rs
View file

@ -516,7 +516,7 @@ impl FormalArgs {
std::fs::write(&sby_file, self.sby_contents(&output)?)?; std::fs::write(&sby_file, self.sby_contents(&output)?)?;
let mut cmd = process::Command::new(&self.sby); let mut cmd = process::Command::new(&self.sby);
cmd.arg("-f"); cmd.arg("-f");
cmd.arg(sby_file); cmd.arg(sby_file.file_name().unwrap());
cmd.args(&self.sby_extra_args); cmd.args(&self.sby_extra_args);
cmd.current_dir(&output.verilog.firrtl.output_dir); cmd.current_dir(&output.verilog.firrtl.output_dir);
let status = self.verilog.firrtl.base.run_external_command(cmd)?; let status = self.verilog.firrtl.base.run_external_command(cmd)?;

70
crates/fayalite/src/formal.rs
View file

@ -1,7 +1,8 @@
// SPDX-License-Identifier: LGPL-3.0-or-later // SPDX-License-Identifier: LGPL-3.0-or-later
// See Notices.txt for copyright information // See Notices.txt for copyright information
use crate::{ use crate::{
intern::{Intern, Interned}, int::BoolOrIntType,
intern::{Intern, Interned, Memoize},
prelude::*, prelude::*,
}; };
use std::sync::OnceLock; use std::sync::OnceLock;
@ -172,12 +173,7 @@ pub fn formal_reset() -> Expr<SyncReset> {
m.annotate_module(BlackBoxInlineAnnotation { m.annotate_module(BlackBoxInlineAnnotation {
path: "fayalite_formal_reset.v".intern(), path: "fayalite_formal_reset.v".intern(),
text: r"module __fayalite_formal_reset(output rst); text: r"module __fayalite_formal_reset(output rst);
reg rst; assign rst = $initstate;
(* gclk *)
reg gclk;
initial rst = 1;
always @(posedge gclk)
rst <= 0;
endmodule endmodule
" "
.intern(), .intern(),
@ -189,3 +185,63 @@ endmodule
let formal_reset = instance(*MOD.get_or_init(formal_reset)); let formal_reset = instance(*MOD.get_or_init(formal_reset));
formal_reset.rst formal_reset.rst
} }
macro_rules! make_any_const_fn {
($ident:ident, $verilog_attribute:literal) => {
#[hdl]
pub fn $ident<T: BoolOrIntType>(ty: T) -> Expr<T> {
#[hdl_module(extern)]
pub(super) fn $ident<T: BoolOrIntType>(ty: T) {
#[hdl]
let out: T = m.output(ty);
let width = ty.width();
let verilog_bitslice = if width == 1 {
String::new()
} else {
format!(" [{}:0]", width - 1)
};
m.annotate_module(BlackBoxInlineAnnotation {
path: Intern::intern_owned(format!(
"fayalite_{}_{width}.v",
stringify!($ident),
)),
text: Intern::intern_owned(format!(
r"module __fayalite_{}_{width}(output{verilog_bitslice} out);
(* {} *)
reg{verilog_bitslice} out;
endmodule
",
stringify!($ident),
$verilog_attribute,
)),
});
m.verilog_name(format!("__fayalite_{}_{width}", stringify!($ident)));
}
#[derive(Copy, Clone, PartialEq, Eq, Hash)]
struct TheMemoize<T>(T);
impl<T: BoolOrIntType> Memoize for TheMemoize<T> {
type Input = ();
type InputOwned = ();
type Output = Option<Interned<Module<$ident<T>>>>;
fn inner(self, _input: &Self::Input) -> Self::Output {
if self.0.width() == 0 {
None
} else {
Some($ident(self.0))
}
}
}
let Some(module) = TheMemoize(ty).get_owned(()) else {
return 0_hdl_u0.cast_bits_to(ty);
};
#[hdl]
let $ident = instance(module);
$ident.out
}
};
}
make_any_const_fn!(any_const, "anyconst");
make_any_const_fn!(any_seq, "anyseq");
make_any_const_fn!(all_const, "allconst");
make_any_const_fn!(all_seq, "allseq");

5
crates/fayalite/src/prelude.rs
View file

@ -14,8 +14,9 @@ pub use crate::{
ReduceBits, ToExpr, ReduceBits, ToExpr,
}, },
formal::{ formal::{
formal_global_clock, formal_reset, hdl_assert, hdl_assert_with_enable, hdl_assume, all_const, all_seq, any_const, any_seq, formal_global_clock, formal_reset, hdl_assert,
hdl_assume_with_enable, hdl_cover, hdl_cover_with_enable, MakeFormalExpr, hdl_assert_with_enable, hdl_assume, hdl_assume_with_enable, hdl_cover,
hdl_cover_with_enable, MakeFormalExpr,
}, },
hdl, hdl_module, hdl, hdl_module,
int::{Bool, DynSize, KnownSize, SInt, SIntType, Size, UInt, UIntType}, int::{Bool, DynSize, KnownSize, SInt, SIntType, Size, UInt, UIntType},

4
crates/fayalite/src/testing.rs
View file

@ -68,7 +68,6 @@ fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf {
}, },
); );
let mut dir = String::with_capacity(64); let mut dir = String::with_capacity(64);
write!(dir, "{simple_hash:08x}-").unwrap();
for ch in Path::new(file) for ch in Path::new(file)
.file_stem() .file_stem()
.unwrap_or_default() .unwrap_or_default()
@ -84,6 +83,7 @@ fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf {
_ => '_', _ => '_',
}); });
} }
write!(dir, "-{simple_hash:08x}").unwrap();
let index = *DIRS let index = *DIRS
.lock() .lock()
.unwrap() .unwrap()
@ -91,7 +91,7 @@ fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf {
.entry_ref(&dir) .entry_ref(&dir)
.and_modify(|v| *v += 1) .and_modify(|v| *v += 1)
.or_insert(0); .or_insert(0);
write!(dir, ".{index}").unwrap(); write!(dir, "-{index}").unwrap();
get_cargo_target_dir() get_cargo_target_dir()
.join("fayalite_assert_formal") .join("fayalite_assert_formal")
.join(dir) .join(dir)

4
crates/fayalite/src/ty.rs
View file

@ -210,7 +210,9 @@ impl sealed::BaseTypeSealed for CanonicalType {}
impl BaseType for CanonicalType {} impl BaseType for CanonicalType {}
pub trait TypeOrDefault<D: Type>: sealed::TypeOrDefaultSealed { pub trait TypeOrDefault<D: Type>:
sealed::TypeOrDefaultSealed + Copy + Eq + Hash + fmt::Debug
{
type Type: Type; type Type: Type;
fn get<F: FnOnce() -> D>(self, default: F) -> Self::Type; fn get<F: FnOnce() -> D>(self, default: F) -> Self::Type;
} }

170
crates/fayalite/src/util/ready_valid.rs
View file

@ -49,7 +49,6 @@ impl<T: Type> ReadyValid<T> {
} }
} }
// TODO: needs testing
#[hdl_module] #[hdl_module]
pub fn queue<T: Type>( pub fn queue<T: Type>(
ty: T, ty: T,
@ -134,7 +133,7 @@ pub fn queue<T: Type>(
#[hdl] #[hdl]
if inp_fire { if inp_fire {
#[hdl] #[hdl]
if inp_index.cmp_eq(capacity) { if inp_index.cmp_eq(capacity.get() - 1) {
connect_any(inp_index, 0_hdl_u0); connect_any(inp_index, 0_hdl_u0);
} else { } else {
connect_any(inp_index, inp_index + 1_hdl_u1); connect_any(inp_index, inp_index + 1_hdl_u1);
@ -144,7 +143,7 @@ pub fn queue<T: Type>(
#[hdl] #[hdl]
if out_fire { if out_fire {
#[hdl] #[hdl]
if out_index.cmp_eq(capacity) { if out_index.cmp_eq(capacity.get() - 1) {
connect_any(out_index, 0_hdl_u0); connect_any(out_index, 0_hdl_u0);
} else { } else {
connect_any(out_index, out_index + 1_hdl_u1); connect_any(out_index, out_index + 1_hdl_u1);
@ -153,10 +152,12 @@ pub fn queue<T: Type>(
#[hdl] #[hdl]
if indexes_equal { if indexes_equal {
connect( #[hdl]
count, if maybe_full {
maybe_full.cast_to_static::<UInt<1>>() << (count_ty.width() - 1), connect_any(count, capacity);
); } else {
connect_any(count, 0_hdl_u0);
}
} else { } else {
if capacity.is_power_of_two() { if capacity.is_power_of_two() {
debug_assert_eq!(count_ty.width(), index_ty.width() + 1); debug_assert_eq!(count_ty.width(), index_ty.width() + 1);
@ -182,6 +183,7 @@ mod tests {
use crate::{ use crate::{
cli::FormalMode, firrtl::ExportOptions, cli::FormalMode, firrtl::ExportOptions,
module::transform::simplify_enums::SimplifyEnumsKind, testing::assert_formal, module::transform::simplify_enums::SimplifyEnumsKind, testing::assert_formal,
ty::StaticType,
}; };
use std::num::NonZero; use std::num::NonZero;
@ -190,8 +192,8 @@ mod tests {
assert_formal( assert_formal(
format_args!("test_queue_{capacity}_{inp_ready_is_comb}_{out_valid_is_comb}"), format_args!("test_queue_{capacity}_{inp_ready_is_comb}_{out_valid_is_comb}"),
queue_test(capacity, inp_ready_is_comb, out_valid_is_comb), queue_test(capacity, inp_ready_is_comb, out_valid_is_comb),
FormalMode::BMC, FormalMode::Prove,
20, 14,
None, None,
ExportOptions { ExportOptions {
simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts), simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
@ -200,12 +202,6 @@ mod tests {
); );
#[hdl_module] #[hdl_module]
fn queue_test(capacity: NonZeroUsize, inp_ready_is_comb: bool, out_valid_is_comb: bool) { fn queue_test(capacity: NonZeroUsize, inp_ready_is_comb: bool, out_valid_is_comb: bool) {
#[hdl]
let inp_data: HdlOption<UInt<8>> = m.input();
#[hdl]
let out_ready: Bool = m.input();
#[hdl]
let start_check: Bool = m.input();
#[hdl] #[hdl]
let clk: Clock = m.input(); let clk: Clock = m.input();
#[hdl] #[hdl]
@ -219,6 +215,24 @@ mod tests {
}, },
); );
#[hdl] #[hdl]
let inp_data: HdlOption<UInt<8>> = wire();
#[hdl]
if any_seq(Bool) {
connect(inp_data, HdlSome(any_seq(UInt::<8>::TYPE)));
} else {
connect(inp_data, HdlNone());
}
#[hdl]
let out_ready: Bool = wire();
connect(out_ready, any_seq(Bool));
let index_ty: UInt<32> = UInt::TYPE;
#[hdl]
let index_to_check = wire();
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]
let dut = instance(queue( let dut = instance(queue(
UInt[ConstUsize::<8>], UInt[ConstUsize::<8>],
capacity, capacity,
@ -228,63 +242,97 @@ mod tests {
connect(dut.cd, cd); connect(dut.cd, cd);
connect(dut.inp.data, inp_data); connect(dut.inp.data, inp_data);
connect(dut.out.ready, out_ready); connect(dut.out.ready, out_ready);
hdl_assume(
clk,
index_to_check.cmp_ne(!Expr::ty(index_to_check).zero()),
"",
);
#[hdl] #[hdl]
let count = reg_builder().clock_domain(cd).reset(0u32); let expected_count = reg_builder().clock_domain(cd).reset(0u32);
#[hdl] #[hdl]
let next_count = wire(); let next_expected_count = wire();
connect(next_count, count); connect(next_expected_count, expected_count);
connect(count, next_count); connect(expected_count, next_expected_count);
#[hdl] #[hdl]
if ReadyValid::fire(dut.inp) & !ReadyValid::fire(dut.out) { if ReadyValid::fire(dut.inp) & !ReadyValid::fire(dut.out) {
connect_any(next_count, count + 1u8); connect_any(next_expected_count, expected_count + 1u8);
} else if !ReadyValid::fire(dut.inp) & ReadyValid::fire(dut.out) { } else if !ReadyValid::fire(dut.inp) & ReadyValid::fire(dut.out) {
connect_any(next_count, count - 1u8); connect_any(next_expected_count, expected_count - 1u8);
} }
hdl_assert(cd.clk, count.cmp_eq(dut.count), ""); hdl_assert(cd.clk, expected_count.cmp_eq(dut.count), "");
#[hdl] #[hdl]
let started_check = reg_builder().clock_domain(cd).reset(false); let prev_out_ready = reg_builder().clock_domain(cd).reset(!0_hdl_u3);
connect_any(
prev_out_ready,
(prev_out_ready << 1) | out_ready.cast_to(UInt[1]),
);
#[hdl] #[hdl]
let steps_till_output = reg_builder().clock_domain(cd).reset(0u32); let prev_inp_valid = reg_builder().clock_domain(cd).reset(!0_hdl_u3);
connect_any(
prev_inp_valid,
(prev_inp_valid << 1) | HdlOption::is_some(inp_data).cast_to(UInt[1]),
);
hdl_assume(clk, (prev_out_ready & prev_inp_valid).cmp_ne(0u8), "");
#[hdl] #[hdl]
let expected_output = reg_builder().clock_domain(cd).reset(HdlNone()); let inp_index = reg_builder().clock_domain(cd).reset(index_ty.zero());
#[hdl] #[hdl]
if start_check & !started_check { let stored_inp_data = reg_builder().clock_domain(cd).reset(0u8);
#[hdl]
if let HdlSome(data) = ReadyValid::fire_data(dut.inp) {
#[hdl] #[hdl]
if let HdlSome(inp) = ReadyValid::fire_data(dut.inp) { if inp_index.cmp_lt(index_max) {
connect(started_check, true); connect_any(inp_index, inp_index + 1u8);
connect_any(
steps_till_output,
count + (!ReadyValid::fire(dut.out)).cast_to(UInt[1]),
);
connect(expected_output, HdlSome(inp));
}
} else if started_check & steps_till_output.cmp_ne(0u32) & ReadyValid::fire(dut.out) {
connect_any(steps_till_output, steps_till_output - 1u32);
}
#[hdl]
let stored_output = reg_builder().clock_domain(cd).reset(HdlNone());
#[hdl]
if let HdlSome(out) = ReadyValid::fire_data(dut.out) {
#[hdl]
if (start_check & !started_check) | (started_check & steps_till_output.cmp_ne(0u32))
{
connect(stored_output, HdlSome(out));
}
}
#[hdl]
if started_check & steps_till_output.cmp_eq(0u32) {
#[hdl]
if let HdlSome(expected_output) = expected_output {
#[hdl] #[hdl]
if let HdlSome(stored_output) = stored_output { if inp_index.cmp_eq(index_to_check) {
hdl_assert(cd.clk, stored_output.cmp_eq(expected_output), ""); connect(stored_inp_data, data);
} else {
hdl_assert(cd.clk, false.to_expr(), "");
} }
} else {
hdl_assert(cd.clk, false.to_expr(), "");
} }
} }
#[hdl]
if inp_index.cmp_lt(index_to_check) {
hdl_assert(clk, stored_inp_data.cmp_eq(0u8), "");
}
#[hdl]
let out_index = reg_builder().clock_domain(cd).reset(index_ty.zero());
#[hdl]
let stored_out_data = reg_builder().clock_domain(cd).reset(0u8);
#[hdl]
if let HdlSome(data) = ReadyValid::fire_data(dut.out) {
#[hdl]
if out_index.cmp_lt(index_max) {
connect_any(out_index, out_index + 1u8);
#[hdl]
if out_index.cmp_eq(index_to_check) {
connect(stored_out_data, data);
}
}
}
#[hdl]
if out_index.cmp_lt(index_to_check) {
hdl_assert(clk, stored_out_data.cmp_eq(0u8), "");
}
hdl_assert(clk, inp_index.cmp_ge(out_index), "");
#[hdl]
if inp_index.cmp_lt(index_max) & out_index.cmp_lt(index_max) {
hdl_assert(clk, expected_count.cmp_eq(inp_index - out_index), "");
} else {
hdl_assert(clk, expected_count.cmp_ge(inp_index - out_index), "");
}
#[hdl]
if inp_index.cmp_gt(index_to_check) & out_index.cmp_gt(index_to_check) {
hdl_assert(clk, stored_inp_data.cmp_eq(stored_out_data), "");
}
} }
} }
@ -328,49 +376,41 @@ mod tests {
test_queue(NonZero::new(2).unwrap(), true, true); test_queue(NonZero::new(2).unwrap(), true, true);
} }
#[cfg(todo)]
#[test] #[test]
fn test_3_false_false() { fn test_3_false_false() {
test_queue(NonZero::new(3).unwrap(), false, false); test_queue(NonZero::new(3).unwrap(), false, false);
} }
#[cfg(todo)]
#[test] #[test]
fn test_3_false_true() { fn test_3_false_true() {
test_queue(NonZero::new(3).unwrap(), false, true); test_queue(NonZero::new(3).unwrap(), false, true);
} }
#[cfg(todo)]
#[test] #[test]
fn test_3_true_false() { fn test_3_true_false() {
test_queue(NonZero::new(3).unwrap(), true, false); test_queue(NonZero::new(3).unwrap(), true, false);
} }
#[cfg(todo)]
#[test] #[test]
fn test_3_true_true() { fn test_3_true_true() {
test_queue(NonZero::new(3).unwrap(), true, true); test_queue(NonZero::new(3).unwrap(), true, true);
} }
#[cfg(todo)]
#[test] #[test]
fn test_4_false_false() { fn test_4_false_false() {
test_queue(NonZero::new(4).unwrap(), false, false); test_queue(NonZero::new(4).unwrap(), false, false);
} }
#[cfg(todo)]
#[test] #[test]
fn test_4_false_true() { fn test_4_false_true() {
test_queue(NonZero::new(4).unwrap(), false, true); test_queue(NonZero::new(4).unwrap(), false, true);
} }
#[cfg(todo)]
#[test] #[test]
fn test_4_true_false() { fn test_4_true_false() {
test_queue(NonZero::new(4).unwrap(), true, false); test_queue(NonZero::new(4).unwrap(), true, false);
} }
#[cfg(todo)]
#[test] #[test]
fn test_4_true_true() { fn test_4_true_true() {
test_queue(NonZero::new(4).unwrap(), true, true); test_queue(NonZero::new(4).unwrap(), true, true);

66
crates/fayalite/tests/hdl_types.rs
View file

@ -29,3 +29,69 @@ pub enum E<T> {
pub struct S2<T = ()> { pub struct S2<T = ()> {
pub v: E<T>, pub v: E<T>,
} }
// check that #[hdl] properly handles hygiene
macro_rules! types_in_macros {
($a:ident, $b:ident, $c:ident, $d:ident, $e:ident, $f:ident, $A:ident, $B:ident, $C:ident, $D:ident, $E:ident, $F:ident) => {
#[hdl]
struct $F {}
#[hdl]
struct $A<$B, $C: Size, const $D: usize, $E = $F> {
$a: $B,
$b: UIntType<$C>,
$c: SInt<$D>,
$d: HdlOption<$E>,
$e: $E,
$f: $F,
}
#[allow(non_camel_case_types)]
#[hdl]
enum $B<$C: Size, const $D: usize, $E = $F> {
$a($A<(), $C, $D, $E>),
$b(UIntType<$C>),
$c(SInt<$D>),
$d,
$e($E),
$f($F),
}
};
// ensure every identifier has different hygiene
() => {
types_in_macros!(a);
};
($a:ident) => {
types_in_macros!($a, b);
};
($a:ident, $b:ident) => {
types_in_macros!($a, $b, c);
};
($a:ident, $b:ident, $c:ident) => {
types_in_macros!($a, $b, $c, d);
};
($a:ident, $b:ident, $c:ident, $d:ident) => {
types_in_macros!($a, $b, $c, $d, e);
};
($a:ident, $b:ident, $c:ident, $d:ident, $e:ident) => {
types_in_macros!($a, $b, $c, $d, $e, f);
};
($a:ident, $b:ident, $c:ident, $d:ident, $e:ident, $f:ident) => {
types_in_macros!($a, $b, $c, $d, $e, $f, A);
};
($a:ident, $b:ident, $c:ident, $d:ident, $e:ident, $f:ident, $A:ident) => {
types_in_macros!($a, $b, $c, $d, $e, $f, $A, B);
};
($a:ident, $b:ident, $c:ident, $d:ident, $e:ident, $f:ident, $A:ident, $B:ident) => {
types_in_macros!($a, $b, $c, $d, $e, $f, $A, $B, C);
};
($a:ident, $b:ident, $c:ident, $d:ident, $e:ident, $f:ident, $A:ident, $B:ident, $C:ident) => {
types_in_macros!($a, $b, $c, $d, $e, $f, $A, $B, $C, D);
};
($a:ident, $b:ident, $c:ident, $d:ident, $e:ident, $f:ident, $A:ident, $B:ident, $C:ident, $D:ident) => {
types_in_macros!($a, $b, $c, $d, $e, $f, $A, $B, $C, $D, E);
};
($a:ident, $b:ident, $c:ident, $d:ident, $e:ident, $f:ident, $A:ident, $B:ident, $C:ident, $D:ident, $E:ident) => {
types_in_macros!($a, $b, $c, $d, $e, $f, $A, $B, $C, $D, $E, F);
};
}
types_in_macros!();

18
crates/fayalite/tests/module.rs
View file

@ -3394,7 +3394,7 @@ circuit check_formal: %[[
{ {
"class": "firrtl.transforms.BlackBoxInlineAnno", "class": "firrtl.transforms.BlackBoxInlineAnno",
"name": "fayalite_formal_reset.v", "name": "fayalite_formal_reset.v",
"text": "module __fayalite_formal_reset(output rst);\n reg rst;\n (* gclk *)\n reg gclk;\n initial rst = 1;\n always @(posedge gclk)\n rst <= 0;\nendmodule\n", "text": "module __fayalite_formal_reset(output rst);\n assign rst = $initstate;\nendmodule\n",
"target": "~check_formal|formal_reset" "target": "~check_formal|formal_reset"
} }
]] ]]
@ -3407,20 +3407,20 @@ circuit check_formal: %[[
input pred1: UInt<1> @[module-XXXXXXXXXX.rs 6:1] input pred1: UInt<1> @[module-XXXXXXXXXX.rs 6:1]
input pred2: UInt<1> @[module-XXXXXXXXXX.rs 7:1] input pred2: UInt<1> @[module-XXXXXXXXXX.rs 7:1]
input pred3: UInt<1> @[module-XXXXXXXXXX.rs 8:1] input pred3: UInt<1> @[module-XXXXXXXXXX.rs 8:1]
inst formal_reset of formal_reset @[formal.rs 189:24] inst formal_reset of formal_reset @[formal.rs 185:24]
assert(clk, pred1, and(en1, not(formal_reset.rst)), "en check 1") @[module-XXXXXXXXXX.rs 9:1] assert(clk, pred1, and(en1, not(formal_reset.rst)), "en check 1") @[module-XXXXXXXXXX.rs 9:1]
inst formal_reset_1 of formal_reset @[formal.rs 189:24] inst formal_reset_1 of formal_reset @[formal.rs 185:24]
assume(clk, pred2, and(en2, not(formal_reset_1.rst)), "en check 2") @[module-XXXXXXXXXX.rs 10:1] assume(clk, pred2, and(en2, not(formal_reset_1.rst)), "en check 2") @[module-XXXXXXXXXX.rs 10:1]
inst formal_reset_2 of formal_reset @[formal.rs 189:24] inst formal_reset_2 of formal_reset @[formal.rs 185:24]
cover(clk, pred3, and(en3, not(formal_reset_2.rst)), "en check 3") @[module-XXXXXXXXXX.rs 11:1] cover(clk, pred3, and(en3, not(formal_reset_2.rst)), "en check 3") @[module-XXXXXXXXXX.rs 11:1]
inst formal_reset_3 of formal_reset @[formal.rs 189:24] inst formal_reset_3 of formal_reset @[formal.rs 185:24]
assert(clk, pred1, and(UInt<1>(0h1), not(formal_reset_3.rst)), "check 1") @[module-XXXXXXXXXX.rs 12:1] assert(clk, pred1, and(UInt<1>(0h1), not(formal_reset_3.rst)), "check 1") @[module-XXXXXXXXXX.rs 12:1]
inst formal_reset_4 of formal_reset @[formal.rs 189:24] inst formal_reset_4 of formal_reset @[formal.rs 185:24]
assume(clk, pred2, and(UInt<1>(0h1), not(formal_reset_4.rst)), "check 2") @[module-XXXXXXXXXX.rs 13:1] assume(clk, pred2, and(UInt<1>(0h1), not(formal_reset_4.rst)), "check 2") @[module-XXXXXXXXXX.rs 13:1]
inst formal_reset_5 of formal_reset @[formal.rs 189:24] inst formal_reset_5 of formal_reset @[formal.rs 185:24]
cover(clk, pred3, and(UInt<1>(0h1), not(formal_reset_5.rst)), "check 3") @[module-XXXXXXXXXX.rs 14:1] cover(clk, pred3, and(UInt<1>(0h1), not(formal_reset_5.rst)), "check 3") @[module-XXXXXXXXXX.rs 14:1]
extmodule formal_reset: @[formal.rs 168:5] extmodule formal_reset: @[formal.rs 169:5]
output rst: UInt<1> @[formal.rs 171:32] output rst: UInt<1> @[formal.rs 172:32]
defname = __fayalite_formal_reset defname = __fayalite_formal_reset
"#, "#,
}; };