From 343805f80b14982495fd4c208b906e7bc694a4f0 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Thu, 3 Oct 2024 23:04:14 -0700 Subject: [PATCH 1/2] fix #[hdl] to work with unusual identifier hygiene from macros --- .../src/hdl_bundle.rs | 109 +++++++++--------- .../fayalite-proc-macros-impl/src/hdl_enum.rs | 96 +++++++-------- .../src/hdl_type_common.rs | 39 +++++-- crates/fayalite/src/ty.rs | 4 +- crates/fayalite/tests/hdl_types.rs | 66 +++++++++++ 5 files changed, 202 insertions(+), 112 deletions(-) diff --git a/crates/fayalite-proc-macros-impl/src/hdl_bundle.rs b/crates/fayalite-proc-macros-impl/src/hdl_bundle.rs index 30cf90f..f3a589a 100644 --- a/crates/fayalite-proc-macros-impl/src/hdl_bundle.rs +++ b/crates/fayalite-proc-macros-impl/src/hdl_bundle.rs @@ -431,6 +431,7 @@ impl ToTokens for ParsedBundle { builder_ident, mask_type_builder_ident, } = self; + let span = ident.span(); let ItemOptions { outline_generated: _, target, @@ -440,7 +441,7 @@ impl ToTokens for ParsedBundle { } = &options.body; let target = get_target(target, ident); let mut item_attrs = attrs.clone(); - item_attrs.push(common_derives(ident.span())); + item_attrs.push(common_derives(span)); ItemStruct { attrs: item_attrs, vis: vis.clone(), @@ -462,19 +463,19 @@ impl ToTokens for ParsedBundle { .map(|ParsedField { ident, ty, .. }| { let ident = ident.as_ref().unwrap(); let expr = ty.make_hdl_type_expr(context); - quote_spanned! {ident.span()=> + quote_spanned! {span=> #ident: #expr, } }) .collect(); - parse_quote_spanned! {ident.span()=> + parse_quote_spanned! {span=> #target { #(#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 builder = Builder { vis: vis.clone(), @@ -488,9 +489,8 @@ impl ToTokens for ParsedBundle { let unfilled_builder_ty = builder.builder_struct_ty(|_| BuilderFieldState::Unfilled); let filled_builder_ty = builder.builder_struct_ty(|_| BuilderFieldState::Filled); let mut mask_type_fields = FieldsNamed::from(fields.clone()); - for Field { ident, ty, .. } in &mut mask_type_fields.named { - let ident = ident.as_ref().unwrap(); - *ty = parse_quote_spanned! {ident.span()=> + for Field { ty, .. } in &mut mask_type_fields.named { + *ty = parse_quote_spanned! {span=> <#ty as ::fayalite::ty::Type>::MaskType }; } @@ -509,8 +509,8 @@ impl ToTokens for ParsedBundle { mask_type_builder.builder_struct_ty(|_| BuilderFieldState::Filled); ItemStruct { attrs: vec![ - common_derives(ident.span()), - parse_quote_spanned! {ident.span()=> + common_derives(span), + parse_quote_spanned! {span=> #[allow(non_camel_case_types, dead_code)] }, ], @@ -523,16 +523,15 @@ impl ToTokens for ParsedBundle { } .to_tokens(tokens); let mut mask_type_match_variant_fields = mask_type_fields; - for Field { ident, ty, .. } in &mut mask_type_match_variant_fields.named { - let ident = ident.as_ref().unwrap(); - *ty = parse_quote_spanned! {ident.span()=> + for Field { ty, .. } in &mut mask_type_match_variant_fields.named { + *ty = parse_quote_spanned! {span=> ::fayalite::expr::Expr<#ty> }; } ItemStruct { attrs: vec![ - common_derives(ident.span()), - parse_quote_spanned! {ident.span()=> + common_derives(span), + parse_quote_spanned! {span=> #[allow(non_camel_case_types, dead_code)] }, ], @@ -545,16 +544,15 @@ impl ToTokens for ParsedBundle { } .to_tokens(tokens); let mut match_variant_fields = FieldsNamed::from(fields.clone()); - for Field { ident, ty, .. } in &mut match_variant_fields.named { - let ident = ident.as_ref().unwrap(); - *ty = parse_quote_spanned! {ident.span()=> + for Field { ty, .. } in &mut match_variant_fields.named { + *ty = parse_quote_spanned! {span=> ::fayalite::expr::Expr<#ty> }; } ItemStruct { attrs: vec![ - common_derives(ident.span()), - parse_quote_spanned! {ident.span()=> + common_derives(span), + parse_quote_spanned! {span=> #[allow(non_camel_case_types, dead_code)] }, ], @@ -566,17 +564,20 @@ impl ToTokens for ParsedBundle { semi_token: None, } .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 ident: &Ident = field.ident().as_ref().unwrap(); let ident_str = ident.to_string(); - quote_spanned! {ident.span()=> - #ident: ::fayalite::expr::Expr::field(__this, #ident_str), + quote_spanned! {span=> + #ident: ::fayalite::expr::Expr::field(#this_token, #ident_str), } })); let mask_type_body_fields = Vec::from_iter(fields.named().into_iter().map(|field| { let ident: &Ident = field.ident().as_ref().unwrap(); - quote_spanned! {ident.span()=> - #ident: ::fayalite::ty::Type::mask_type(&self.#ident), + quote_spanned! {span=> + #ident: ::fayalite::ty::Type::mask_type(&#self_token.#ident), } })); let from_canonical_body_fields = @@ -585,13 +586,13 @@ impl ToTokens for ParsedBundle { let ident: &Ident = field.ident().as_ref().unwrap(); let ident_str = ident.to_string(); let flipped = flip.is_some(); - quote_spanned! {ident.span()=> + quote_spanned! {span=> #ident: { let ::fayalite::bundle::BundleField { name: __name, flipped: __flipped, ty: __ty, - } = __fields[#index]; + } = #fields_token[#index]; ::fayalite::__std::assert_eq!(&*__name, #ident_str); ::fayalite::__std::assert_eq!(__flipped, #flipped); ::fayalite::ty::Type::from_canonical(__ty) @@ -604,17 +605,17 @@ impl ToTokens for ParsedBundle { let ident: &Ident = field.ident().as_ref().unwrap(); let ident_str = ident.to_string(); let flipped = flip.is_some(); - quote_spanned! {ident.span()=> + quote_spanned! {span=> ::fayalite::bundle::BundleField { name: ::fayalite::intern::Intern::intern(#ident_str), 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(); - quote_spanned! {ident.span()=> + quote_spanned! {span=> #[automatically_derived] impl #impl_generics ::fayalite::ty::Type for #mask_type_ident #type_generics #where_clause @@ -630,7 +631,7 @@ impl ToTokens for ParsedBundle { ::MatchVariantAndInactiveScope, >; fn match_variants( - __this: ::fayalite::expr::Expr, + #this_token: ::fayalite::expr::Expr, __source_location: ::fayalite::source_location::SourceLocation, ) -> ::MatchVariantsIter { let __retval = #mask_type_match_variant_ident { @@ -638,19 +639,19 @@ impl ToTokens for ParsedBundle { }; ::fayalite::__std::iter::once(::fayalite::ty::MatchVariantWithoutScope(__retval)) } - fn mask_type(&self) -> ::MaskType { - *self + fn mask_type(&#self_token) -> ::MaskType { + *#self_token } - fn canonical(&self) -> ::fayalite::ty::CanonicalType { - ::fayalite::ty::Type::canonical(&::fayalite::bundle::Bundle::new(::fayalite::bundle::BundleType::fields(self))) + fn canonical(&#self_token) -> ::fayalite::ty::CanonicalType { + ::fayalite::ty::Type::canonical(&::fayalite::bundle::Bundle::new(::fayalite::bundle::BundleType::fields(#self_token))) } #[track_caller] fn from_canonical(__canonical_type: ::fayalite::ty::CanonicalType) -> Self { let ::fayalite::ty::CanonicalType::Bundle(__bundle) = __canonical_type else { ::fayalite::__std::panic!("expected bundle"); }; - let __fields = ::fayalite::bundle::BundleType::fields(&__bundle); - ::fayalite::__std::assert_eq!(__fields.len(), #fields_len, "bundle has wrong number of fields"); + let #fields_token = ::fayalite::bundle::BundleType::fields(&__bundle); + ::fayalite::__std::assert_eq!(#fields_token.len(), #fields_len, "bundle has wrong number of fields"); Self { #(#from_canonical_body_fields)* } @@ -665,7 +666,7 @@ impl ToTokens for ParsedBundle { { type Builder = #unfilled_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)*][..]) } } @@ -680,8 +681,8 @@ impl ToTokens for ParsedBundle { impl #impl_generics ::fayalite::ty::TypeWithDeref for #mask_type_ident #type_generics #where_clause { - fn expr_deref(__this: &::fayalite::expr::Expr) -> &::MatchVariant { - let __this = *__this; + fn expr_deref(#this_token: &::fayalite::expr::Expr) -> &::MatchVariant { + let #this_token = *#this_token; let __retval = #mask_type_match_variant_ident { #(#match_variant_body_fields)* }; @@ -703,7 +704,7 @@ impl ToTokens for ParsedBundle { ::MatchVariantAndInactiveScope, >; fn match_variants( - __this: ::fayalite::expr::Expr, + #this_token: ::fayalite::expr::Expr, __source_location: ::fayalite::source_location::SourceLocation, ) -> ::MatchVariantsIter { let __retval = #match_variant_ident { @@ -711,21 +712,21 @@ impl ToTokens for ParsedBundle { }; ::fayalite::__std::iter::once(::fayalite::ty::MatchVariantWithoutScope(__retval)) } - fn mask_type(&self) -> ::MaskType { + fn mask_type(&#self_token) -> ::MaskType { #mask_type_ident { #(#mask_type_body_fields)* } } - fn canonical(&self) -> ::fayalite::ty::CanonicalType { - ::fayalite::ty::Type::canonical(&::fayalite::bundle::Bundle::new(::fayalite::bundle::BundleType::fields(self))) + fn canonical(&#self_token) -> ::fayalite::ty::CanonicalType { + ::fayalite::ty::Type::canonical(&::fayalite::bundle::Bundle::new(::fayalite::bundle::BundleType::fields(#self_token))) } #[track_caller] fn from_canonical(__canonical_type: ::fayalite::ty::CanonicalType) -> Self { let ::fayalite::ty::CanonicalType::Bundle(__bundle) = __canonical_type else { ::fayalite::__std::panic!("expected bundle"); }; - let __fields = ::fayalite::bundle::BundleType::fields(&__bundle); - ::fayalite::__std::assert_eq!(__fields.len(), #fields_len, "bundle has wrong number of fields"); + let #fields_token = ::fayalite::bundle::BundleType::fields(&__bundle); + ::fayalite::__std::assert_eq!(#fields_token.len(), #fields_len, "bundle has wrong number of fields"); Self { #(#from_canonical_body_fields)* } @@ -740,7 +741,7 @@ impl ToTokens for ParsedBundle { { type Builder = #unfilled_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)*][..]) } } @@ -755,8 +756,8 @@ impl ToTokens for ParsedBundle { impl #impl_generics ::fayalite::ty::TypeWithDeref for #target #type_generics #where_clause { - fn expr_deref(__this: &::fayalite::expr::Expr) -> &::MatchVariant { - let __this = *__this; + fn expr_deref(#this_token: &::fayalite::expr::Expr) -> &::MatchVariant { + let #this_token = *#this_token; let __retval = #match_variant_ident { #(#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 ident: &Ident = field.ident().as_ref().unwrap(); let ty = field.ty(); - quote_spanned! {ident.span()=> + quote_spanned! {span=> #ident: <#ty as ::fayalite::ty::StaticType>::TYPE, } })); @@ -780,28 +781,26 @@ impl ToTokens for ParsedBundle { Vec::from_iter(fields.named().into_iter().map(|field| { let ident: &Ident = field.ident().as_ref().unwrap(); let ty = field.ty(); - quote_spanned! {ident.span()=> + quote_spanned! {span=> #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 ident: &Ident = field.ident().as_ref().unwrap(); let flipped = field_flip.is_some(); 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_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 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); } })); - quote_spanned! {ident.span()=> + quote_spanned! {span=> #[automatically_derived] impl #static_impl_generics ::fayalite::ty::StaticType for #mask_type_ident #static_type_generics #static_where_clause diff --git a/crates/fayalite-proc-macros-impl/src/hdl_enum.rs b/crates/fayalite-proc-macros-impl/src/hdl_enum.rs index 50fb138..adddd74 100644 --- a/crates/fayalite-proc-macros-impl/src/hdl_enum.rs +++ b/crates/fayalite-proc-macros-impl/src/hdl_enum.rs @@ -204,6 +204,7 @@ impl ToTokens for ParsedEnum { variants, match_variant_ident, } = self; + let span = ident.span(); let ItemOptions { outline_generated: _, target, @@ -213,8 +214,8 @@ impl ToTokens for ParsedEnum { } = &options.body; let target = get_target(target, ident); let mut struct_attrs = attrs.clone(); - struct_attrs.push(common_derives(ident.span())); - struct_attrs.push(parse_quote_spanned! {ident.span()=> + struct_attrs.push(common_derives(span)); + struct_attrs.push(parse_quote_spanned! {span=> #[allow(non_snake_case)] }); 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()); ty.clone().into() } else { - colon_token = Token![:](ident.span()); - parse_quote_spanned! {ident.span()=> + colon_token = Token![:](span); + parse_quote_spanned! {span=> () } }; @@ -282,30 +283,30 @@ impl ToTokens for ParsedEnum { }) = field { let expr = ty.make_hdl_type_expr(context); - quote_spanned! {ident.span()=> + quote_spanned! {span=> #ident: #expr, } } else { - quote_spanned! {ident.span()=> + quote_spanned! {span=> #ident: (), } } }) .collect(); - parse_quote_spanned! {ident.span()=> + parse_quote_spanned! {span=> #target { #(#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 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 mut enum_attrs = attrs.clone(); - enum_attrs.push(parse_quote_spanned! {ident.span()=> + enum_attrs.push(parse_quote_spanned! {span=> #[allow(dead_code)] }); ItemEnum { @@ -354,7 +355,7 @@ impl ToTokens for ParsedEnum { .to_tokens(tokens); } 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)] }); ItemEnum { @@ -389,7 +390,7 @@ impl ToTokens for ParsedEnum { mutability: FieldMutability::None, ident: None, colon_token: None, - ty: parse_quote_spanned! {ident.span()=> + ty: parse_quote_spanned! {span=> ::fayalite::expr::Expr<#ty> }, }, @@ -403,21 +404,22 @@ impl ToTokens for ParsedEnum { )), } .to_tokens(tokens); + let self_token = Token![self](span); for (index, ParsedVariant { ident, field, .. }) in variants.iter().enumerate() { if let Some(ParsedVariantField { ty, .. }) = field { - quote_spanned! {ident.span()=> + quote_spanned! {span=> #[automatically_derived] impl #impl_generics #target #type_generics #where_clause { #[allow(non_snake_case, dead_code)] #vis fn #ident<__V: ::fayalite::expr::ToExpr>( - self, + #self_token, v: __V, ) -> ::fayalite::expr::Expr { ::fayalite::expr::ToExpr::to_expr( &::fayalite::expr::ops::EnumLiteral::new_by_index( - self, + #self_token, #index, ::fayalite::__std::option::Option::Some( ::fayalite::expr::Expr::canonical( @@ -430,16 +432,16 @@ impl ToTokens for ParsedEnum { } } } else { - quote_spanned! {ident.span()=> + quote_spanned! {span=> #[automatically_derived] impl #impl_generics #target #type_generics #where_clause { #[allow(non_snake_case, dead_code)] - #vis fn #ident(self) -> ::fayalite::expr::Expr { + #vis fn #ident(#self_token) -> ::fayalite::expr::Expr { ::fayalite::expr::ToExpr::to_expr( &::fayalite::expr::ops::EnumLiteral::new_by_index( - self, + #self_token, #index, ::fayalite::__std::option::Option::None, ), @@ -450,46 +452,48 @@ impl ToTokens for ParsedEnum { } .to_tokens(tokens); } + let variants_token = Ident::new("variants", span); let from_canonical_body_fields = Vec::from_iter(variants.iter().enumerate().map( |(index, ParsedVariant { ident, field, .. })| { let ident_str = ident.to_string(); let val = if field.is_some() { 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)) } } else { - quote_spanned! {ident.span()=> + quote_spanned! {span=> ::fayalite::__std::assert!(ty.is_none()); } }; - quote_spanned! {ident.span()=> + quote_spanned! {span=> #ident: { let ::fayalite::enum_::EnumVariant { name, ty, - } = variants[#index]; + } = #variants_token[#index]; ::fayalite::__std::assert_eq!(&*name, #ident_str); #val }, } }, )); + let variant_access_token = Ident::new("variant_access", span); let match_active_scope_match_arms = Vec::from_iter(variants.iter().enumerate().map( |(index, ParsedVariant { ident, field, .. })| { if field.is_some() { - quote_spanned! {ident.span()=> + quote_spanned! {span=> #index => #match_variant_ident::#ident( ::fayalite::expr::ToExpr::to_expr( &::fayalite::expr::ops::VariantAccess::new_by_index( - variant_access.base(), - variant_access.variant_index(), + #variant_access_token.base(), + #variant_access_token.variant_index(), ), ), ), } } else { - quote_spanned! {ident.span()=> + quote_spanned! {span=> #index => #match_variant_ident::#ident, } } @@ -507,16 +511,16 @@ impl ToTokens for ParsedEnum { match field { Some(ParsedVariantField { options, .. }) => { let FieldOptions {} = options.body; - quote_spanned! {ident.span()=> + quote_spanned! {span=> ::fayalite::enum_::EnumVariant { name: ::fayalite::intern::Intern::intern(#ident_str), 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 { name: ::fayalite::intern::Intern::intern(#ident_str), ty: ::fayalite::__std::option::Option::None, @@ -526,7 +530,7 @@ impl ToTokens for ParsedEnum { }, )); let variants_len = variants.len(); - quote_spanned! {ident.span()=> + quote_spanned! {span=> #[automatically_derived] impl #impl_generics ::fayalite::ty::Type for #target #type_generics #where_clause @@ -544,11 +548,11 @@ impl ToTokens for ParsedEnum { ) -> ::MatchVariantsIter { ::fayalite::module::enum_match_variants_helper(this, source_location) } - fn mask_type(&self) -> ::MaskType { + fn mask_type(&#self_token) -> ::MaskType { ::fayalite::int::Bool } - fn canonical(&self) -> ::fayalite::ty::CanonicalType { - ::fayalite::ty::CanonicalType::Enum(::fayalite::enum_::Enum::new(::fayalite::enum_::EnumType::variants(self))) + fn canonical(&#self_token) -> ::fayalite::ty::CanonicalType { + ::fayalite::ty::CanonicalType::Enum(::fayalite::enum_::Enum::new(::fayalite::enum_::EnumType::variants(#self_token))) } #[track_caller] #[allow(non_snake_case)] @@ -556,8 +560,8 @@ impl ToTokens for ParsedEnum { let ::fayalite::ty::CanonicalType::Enum(enum_) = canonical_type else { ::fayalite::__std::panic!("expected enum"); }; - let variants = ::fayalite::enum_::EnumType::variants(&enum_); - ::fayalite::__std::assert_eq!(variants.len(), #variants_len, "enum has wrong number of variants"); + let #variants_token = ::fayalite::enum_::EnumType::variants(&enum_); + ::fayalite::__std::assert_eq!(#variants_token.len(), #variants_len, "enum has wrong number of variants"); Self { #(#from_canonical_body_fields)* } @@ -573,16 +577,16 @@ impl ToTokens for ParsedEnum { fn match_activate_scope( v: ::MatchVariantAndInactiveScope, ) -> (::MatchVariant, ::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)* #variants_len.. => ::fayalite::__std::panic!("invalid variant index"), }, scope, ) } - fn variants(&self) -> ::fayalite::intern::Interned<[::fayalite::enum_::EnumVariant]> { + fn variants(&#self_token) -> ::fayalite::intern::Interned<[::fayalite::enum_::EnumVariant]> { ::fayalite::intern::Intern::intern(&[ #(#variants_body_variants)* ][..]) @@ -597,34 +601,34 @@ impl ToTokens for ParsedEnum { let static_type_body_variants = Vec::from_iter(variants.iter().map(|ParsedVariant { ident, field, .. }| { if let Some(_) = field { - quote_spanned! {ident.span()=> + quote_spanned! {span=> #ident: ::fayalite::ty::StaticType::TYPE, } } else { - quote_spanned! {ident.span()=> + quote_spanned! {span=> #ident: (), } } })); - let type_properties = format_ident!("__type_properties", span = ident.span()); + let type_properties = format_ident!("__type_properties", span = span); 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 { - quote_spanned! {ident.span()=> + quote_spanned! {span=> ::fayalite::__std::option::Option::Some( <#ty as ::fayalite::ty::StaticType>::TYPE_PROPERTIES, ) } } else { - quote_spanned! {ident.span()=> + quote_spanned! {span=> ::fayalite::__std::option::Option::None } }; - quote_spanned! {ident.span()=> + quote_spanned! {span=> let #type_properties = #type_properties.variant(#variant); } })); - quote_spanned! {ident.span()=> + quote_spanned! {span=> #[automatically_derived] impl #static_impl_generics ::fayalite::ty::StaticType for #target #static_type_generics diff --git a/crates/fayalite-proc-macros-impl/src/hdl_type_common.rs b/crates/fayalite-proc-macros-impl/src/hdl_type_common.rs index efbe7f3..e7561fe 100644 --- a/crates/fayalite-proc-macros-impl/src/hdl_type_common.rs +++ b/crates/fayalite-proc-macros-impl/src/hdl_type_common.rs @@ -1896,6 +1896,7 @@ pub(crate) mod known_items { impl_known_item!(::fayalite::array::ArrayType); impl_known_item!(::fayalite::bundle::BundleType); impl_known_item!(::fayalite::enum_::EnumType); + impl_known_item!(::fayalite::int::BoolOrIntType); impl_known_item!(::fayalite::int::DynSize); impl_known_item!(::fayalite::int::IntType); impl_known_item!(::fayalite::int::KnownSize); @@ -2085,6 +2086,7 @@ macro_rules! impl_bounds { impl_bounds! { #[struct = ParsedBounds] pub(crate) enum ParsedBound { + BoolOrIntType, BundleType, EnumType, IntType, @@ -2098,6 +2100,7 @@ impl_bounds! { impl_bounds! { #[struct = ParsedTypeBounds] pub(crate) enum ParsedTypeBound { + BoolOrIntType, BundleType, EnumType, IntType, @@ -2109,6 +2112,7 @@ impl_bounds! { impl From for ParsedBound { fn from(value: ParsedTypeBound) -> Self { match value { + ParsedTypeBound::BoolOrIntType(v) => ParsedBound::BoolOrIntType(v), ParsedTypeBound::BundleType(v) => ParsedBound::BundleType(v), ParsedTypeBound::EnumType(v) => ParsedBound::EnumType(v), ParsedTypeBound::IntType(v) => ParsedBound::IntType(v), @@ -2121,6 +2125,7 @@ impl From for ParsedBound { impl From for ParsedBounds { fn from(value: ParsedTypeBounds) -> Self { let ParsedTypeBounds { + BoolOrIntType, BundleType, EnumType, IntType, @@ -2128,6 +2133,7 @@ impl From for ParsedBounds { Type, } = value; Self { + BoolOrIntType, BundleType, EnumType, IntType, @@ -2143,6 +2149,10 @@ impl ParsedTypeBound { fn implied_bounds(self) -> ParsedTypeBounds { let span = self.span(); match self { + Self::BoolOrIntType(v) => ParsedTypeBounds::from_iter([ + ParsedTypeBound::from(v), + ParsedTypeBound::Type(known_items::Type(span)), + ]), Self::BundleType(v) => ParsedTypeBounds::from_iter([ ParsedTypeBound::from(v), ParsedTypeBound::Type(known_items::Type(span)), @@ -2153,6 +2163,7 @@ impl ParsedTypeBound { ]), Self::IntType(v) => ParsedTypeBounds::from_iter([ ParsedTypeBound::from(v), + ParsedTypeBound::BoolOrIntType(known_items::BoolOrIntType(span)), ParsedTypeBound::Type(known_items::Type(span)), ]), Self::StaticType(v) => ParsedTypeBounds::from_iter([ @@ -2185,6 +2196,7 @@ impl From for ParsedBounds { fn from(value: ParsedSizeTypeBounds) -> Self { let ParsedSizeTypeBounds { KnownSize, Size } = value; Self { + BoolOrIntType: None, BundleType: None, EnumType: None, IntType: None, @@ -2260,6 +2272,7 @@ pub(crate) enum ParsedBoundCategory { impl ParsedBound { fn categorize(self) -> ParsedBoundCategory { match self { + Self::BoolOrIntType(v) => ParsedBoundCategory::Type(ParsedTypeBound::BoolOrIntType(v)), Self::BundleType(v) => ParsedBoundCategory::Type(ParsedTypeBound::BundleType(v)), Self::EnumType(v) => ParsedBoundCategory::Type(ParsedTypeBound::EnumType(v)), Self::IntType(v) => ParsedBoundCategory::Type(ParsedTypeBound::IntType(v)), @@ -2575,6 +2588,7 @@ impl ParsedGenerics { } }) .collect(); + let param_token = Ident::new("__param", ident.span()); for (param_count, (generics_accumulation_type, next_param)) in generics_accumulation_types .iter() .zip(&self.params) @@ -2623,7 +2637,7 @@ impl ParsedGenerics { next_generics.split_for_impl(); let next_turbofish = next_type_generics.as_turbofish(); let mut param: Expr = parse_quote_spanned! {ident.span()=> - __param + #param_token }; let mut generics = next_generics.clone(); let mut index_type = param_ident.clone(); @@ -2638,7 +2652,7 @@ impl ParsedGenerics { is_const: false, }); param = parse_quote_spanned! {ident.span()=> - ::fayalite::ty::TypeOrDefault::get(__param, || #default_expr) + ::fayalite::ty::TypeOrDefault::get(#param_token, || #default_expr) }; let context = MakeHdlTypeExprContext { named_param_values: self_members[..param_count] @@ -2703,7 +2717,7 @@ impl ParsedGenerics { { 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::Intern::intern_sized(#output_expr), ) @@ -2724,7 +2738,7 @@ impl ParsedGenerics { .iter() .cloned() .chain([parse_quote_spanned! {ident.span()=> - __param + #param_token }]) .collect(), is_const: false, @@ -2763,7 +2777,7 @@ impl ParsedGenerics { { 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::Intern::intern_sized(#output_expr), ) @@ -2791,7 +2805,7 @@ impl ParsedGenerics { .iter() .cloned() .chain([parse_quote_spanned! {ident.span()=> - __param + #param_token }]) .collect(), is_const: false, @@ -2833,7 +2847,7 @@ impl ParsedGenerics { { 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::Intern::intern_sized(#output_expr), ) @@ -3145,16 +3159,21 @@ impl ParsedGenerics { .Type .get_or_insert_with(|| known_items::Type(bound.span())); match bound { - ParsedTypeBound::BundleType(_) + ParsedTypeBound::BoolOrIntType(_) + | ParsedTypeBound::BundleType(_) | ParsedTypeBound::EnumType(_) | ParsedTypeBound::IntType(_) => { errors.error(bound, "bound on mask type not implemented"); } ParsedTypeBound::StaticType(bound) => { 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(_) => {} } } diff --git a/crates/fayalite/src/ty.rs b/crates/fayalite/src/ty.rs index c7081eb..380d2e6 100644 --- a/crates/fayalite/src/ty.rs +++ b/crates/fayalite/src/ty.rs @@ -210,7 +210,9 @@ impl sealed::BaseTypeSealed for CanonicalType {} impl BaseType for CanonicalType {} -pub trait TypeOrDefault: sealed::TypeOrDefaultSealed { +pub trait TypeOrDefault: + sealed::TypeOrDefaultSealed + Copy + Eq + Hash + fmt::Debug +{ type Type: Type; fn get D>(self, default: F) -> Self::Type; } diff --git a/crates/fayalite/tests/hdl_types.rs b/crates/fayalite/tests/hdl_types.rs index d043013..3f11de3 100644 --- a/crates/fayalite/tests/hdl_types.rs +++ b/crates/fayalite/tests/hdl_types.rs @@ -29,3 +29,69 @@ pub enum E { pub struct S2 { pub v: E, } + +// 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!(); From 0d54b9a2a9abd7c8b34566ae6e55ca0d508c6a21 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Thu, 3 Oct 2024 23:07:14 -0700 Subject: [PATCH 2/2] queue formal proof passes! --- crates/fayalite/src/cli.rs | 2 +- crates/fayalite/src/formal.rs | 70 +++++++++- crates/fayalite/src/prelude.rs | 5 +- crates/fayalite/src/testing.rs | 4 +- crates/fayalite/src/util/ready_valid.rs | 170 +++++++++++++++--------- crates/fayalite/tests/module.rs | 18 +-- 6 files changed, 183 insertions(+), 86 deletions(-) diff --git a/crates/fayalite/src/cli.rs b/crates/fayalite/src/cli.rs index b0b818c..f1d69d2 100644 --- a/crates/fayalite/src/cli.rs +++ b/crates/fayalite/src/cli.rs @@ -516,7 +516,7 @@ impl FormalArgs { std::fs::write(&sby_file, self.sby_contents(&output)?)?; let mut cmd = process::Command::new(&self.sby); cmd.arg("-f"); - cmd.arg(sby_file); + cmd.arg(sby_file.file_name().unwrap()); cmd.args(&self.sby_extra_args); cmd.current_dir(&output.verilog.firrtl.output_dir); let status = self.verilog.firrtl.base.run_external_command(cmd)?; diff --git a/crates/fayalite/src/formal.rs b/crates/fayalite/src/formal.rs index eab1969..17d3122 100644 --- a/crates/fayalite/src/formal.rs +++ b/crates/fayalite/src/formal.rs @@ -1,7 +1,8 @@ // SPDX-License-Identifier: LGPL-3.0-or-later // See Notices.txt for copyright information use crate::{ - intern::{Intern, Interned}, + int::BoolOrIntType, + intern::{Intern, Interned, Memoize}, prelude::*, }; use std::sync::OnceLock; @@ -172,12 +173,7 @@ pub fn formal_reset() -> Expr { m.annotate_module(BlackBoxInlineAnnotation { path: "fayalite_formal_reset.v".intern(), text: r"module __fayalite_formal_reset(output rst); - reg rst; - (* gclk *) - reg gclk; - initial rst = 1; - always @(posedge gclk) - rst <= 0; + assign rst = $initstate; endmodule " .intern(), @@ -189,3 +185,63 @@ endmodule let formal_reset = instance(*MOD.get_or_init(formal_reset)); formal_reset.rst } + +macro_rules! make_any_const_fn { + ($ident:ident, $verilog_attribute:literal) => { + #[hdl] + pub fn $ident(ty: T) -> Expr { + #[hdl_module(extern)] + pub(super) fn $ident(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); + impl Memoize for TheMemoize { + type Input = (); + type InputOwned = (); + type Output = Option>>>; + 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"); diff --git a/crates/fayalite/src/prelude.rs b/crates/fayalite/src/prelude.rs index f1a9736..46d9e6e 100644 --- a/crates/fayalite/src/prelude.rs +++ b/crates/fayalite/src/prelude.rs @@ -14,8 +14,9 @@ pub use crate::{ ReduceBits, ToExpr, }, formal::{ - formal_global_clock, formal_reset, hdl_assert, hdl_assert_with_enable, hdl_assume, - hdl_assume_with_enable, hdl_cover, hdl_cover_with_enable, MakeFormalExpr, + all_const, all_seq, any_const, any_seq, formal_global_clock, formal_reset, hdl_assert, + hdl_assert_with_enable, hdl_assume, hdl_assume_with_enable, hdl_cover, + hdl_cover_with_enable, MakeFormalExpr, }, hdl, hdl_module, int::{Bool, DynSize, KnownSize, SInt, SIntType, Size, UInt, UIntType}, diff --git a/crates/fayalite/src/testing.rs b/crates/fayalite/src/testing.rs index 07252f1..4517e34 100644 --- a/crates/fayalite/src/testing.rs +++ b/crates/fayalite/src/testing.rs @@ -68,7 +68,6 @@ fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf { }, ); let mut dir = String::with_capacity(64); - write!(dir, "{simple_hash:08x}-").unwrap(); for ch in Path::new(file) .file_stem() .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 .lock() .unwrap() @@ -91,7 +91,7 @@ fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf { .entry_ref(&dir) .and_modify(|v| *v += 1) .or_insert(0); - write!(dir, ".{index}").unwrap(); + write!(dir, "-{index}").unwrap(); get_cargo_target_dir() .join("fayalite_assert_formal") .join(dir) diff --git a/crates/fayalite/src/util/ready_valid.rs b/crates/fayalite/src/util/ready_valid.rs index 41299a6..f3d5653 100644 --- a/crates/fayalite/src/util/ready_valid.rs +++ b/crates/fayalite/src/util/ready_valid.rs @@ -49,7 +49,6 @@ impl ReadyValid { } } -// TODO: needs testing #[hdl_module] pub fn queue( ty: T, @@ -134,7 +133,7 @@ pub fn queue( #[hdl] if inp_fire { #[hdl] - if inp_index.cmp_eq(capacity) { + if inp_index.cmp_eq(capacity.get() - 1) { connect_any(inp_index, 0_hdl_u0); } else { connect_any(inp_index, inp_index + 1_hdl_u1); @@ -144,7 +143,7 @@ pub fn queue( #[hdl] if out_fire { #[hdl] - if out_index.cmp_eq(capacity) { + if out_index.cmp_eq(capacity.get() - 1) { connect_any(out_index, 0_hdl_u0); } else { connect_any(out_index, out_index + 1_hdl_u1); @@ -153,10 +152,12 @@ pub fn queue( #[hdl] if indexes_equal { - connect( - count, - maybe_full.cast_to_static::>() << (count_ty.width() - 1), - ); + #[hdl] + if maybe_full { + connect_any(count, capacity); + } else { + connect_any(count, 0_hdl_u0); + } } else { if capacity.is_power_of_two() { debug_assert_eq!(count_ty.width(), index_ty.width() + 1); @@ -182,6 +183,7 @@ mod tests { use crate::{ cli::FormalMode, firrtl::ExportOptions, module::transform::simplify_enums::SimplifyEnumsKind, testing::assert_formal, + ty::StaticType, }; use std::num::NonZero; @@ -190,8 +192,8 @@ mod tests { assert_formal( 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::BMC, - 20, + FormalMode::Prove, + 14, None, ExportOptions { simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts), @@ -200,12 +202,6 @@ mod tests { ); #[hdl_module] fn queue_test(capacity: NonZeroUsize, inp_ready_is_comb: bool, out_valid_is_comb: bool) { - #[hdl] - let inp_data: HdlOption> = m.input(); - #[hdl] - let out_ready: Bool = m.input(); - #[hdl] - let start_check: Bool = m.input(); #[hdl] let clk: Clock = m.input(); #[hdl] @@ -219,6 +215,24 @@ mod tests { }, ); #[hdl] + let inp_data: HdlOption> = 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( UInt[ConstUsize::<8>], capacity, @@ -228,63 +242,97 @@ 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()), + "", + ); + #[hdl] - let count = reg_builder().clock_domain(cd).reset(0u32); + let expected_count = reg_builder().clock_domain(cd).reset(0u32); #[hdl] - let next_count = wire(); - connect(next_count, count); - connect(count, next_count); + let next_expected_count = wire(); + connect(next_expected_count, expected_count); + connect(expected_count, next_expected_count); #[hdl] 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) { - 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] - 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] - 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] - let expected_output = reg_builder().clock_domain(cd).reset(HdlNone()); + let inp_index = reg_builder().clock_domain(cd).reset(index_ty.zero()); #[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] - if let HdlSome(inp) = ReadyValid::fire_data(dut.inp) { - connect(started_check, true); - 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 { + if inp_index.cmp_lt(index_max) { + connect_any(inp_index, inp_index + 1u8); #[hdl] - if let HdlSome(stored_output) = stored_output { - hdl_assert(cd.clk, stored_output.cmp_eq(expected_output), ""); - } else { - hdl_assert(cd.clk, false.to_expr(), ""); + if inp_index.cmp_eq(index_to_check) { + connect(stored_inp_data, data); } - } 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); } - #[cfg(todo)] #[test] fn test_3_false_false() { test_queue(NonZero::new(3).unwrap(), false, false); } - #[cfg(todo)] #[test] fn test_3_false_true() { test_queue(NonZero::new(3).unwrap(), false, true); } - #[cfg(todo)] #[test] fn test_3_true_false() { test_queue(NonZero::new(3).unwrap(), true, false); } - #[cfg(todo)] #[test] fn test_3_true_true() { test_queue(NonZero::new(3).unwrap(), true, true); } - #[cfg(todo)] #[test] fn test_4_false_false() { test_queue(NonZero::new(4).unwrap(), false, false); } - #[cfg(todo)] #[test] fn test_4_false_true() { test_queue(NonZero::new(4).unwrap(), false, true); } - #[cfg(todo)] #[test] fn test_4_true_false() { test_queue(NonZero::new(4).unwrap(), true, false); } - #[cfg(todo)] #[test] fn test_4_true_true() { test_queue(NonZero::new(4).unwrap(), true, true); diff --git a/crates/fayalite/tests/module.rs b/crates/fayalite/tests/module.rs index 7d12739..0d690f2 100644 --- a/crates/fayalite/tests/module.rs +++ b/crates/fayalite/tests/module.rs @@ -3394,7 +3394,7 @@ circuit check_formal: %[[ { "class": "firrtl.transforms.BlackBoxInlineAnno", "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" } ]] @@ -3407,20 +3407,20 @@ circuit check_formal: %[[ input pred1: UInt<1> @[module-XXXXXXXXXX.rs 6:1] input pred2: UInt<1> @[module-XXXXXXXXXX.rs 7: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] - 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] - 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] - 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] - 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] - 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] - extmodule formal_reset: @[formal.rs 168:5] - output rst: UInt<1> @[formal.rs 171:32] + extmodule formal_reset: @[formal.rs 169:5] + output rst: UInt<1> @[formal.rs 172:32] defname = __fayalite_formal_reset "#, };