From e8c393f3bbbd7677864847f054adeefaaf55ea4f Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Tue, 1 Oct 2024 18:40:52 -0700 Subject: [PATCH 1/5] sort pub mod items --- crates/fayalite/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crates/fayalite/src/lib.rs b/crates/fayalite/src/lib.rs index 70ce724..9192645 100644 --- a/crates/fayalite/src/lib.rs +++ b/crates/fayalite/src/lib.rs @@ -43,12 +43,12 @@ pub mod int; pub mod intern; pub mod memory; pub mod module; +pub mod prelude; pub mod reg; pub mod reset; pub mod source_location; +pub mod testing; pub mod ty; pub mod util; //pub mod valueless; -pub mod prelude; -pub mod testing; pub mod wire; From f35d88d2bbe5f95ec46773727e5d375b4f90ffff Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Tue, 1 Oct 2024 18:41:41 -0700 Subject: [PATCH 2/5] remove unused valueless.rs --- crates/fayalite/src/lib.rs | 2 - crates/fayalite/src/valueless.rs | 88 -------------------------------- 2 files changed, 90 deletions(-) delete mode 100644 crates/fayalite/src/valueless.rs diff --git a/crates/fayalite/src/lib.rs b/crates/fayalite/src/lib.rs index 9192645..6e1ccd3 100644 --- a/crates/fayalite/src/lib.rs +++ b/crates/fayalite/src/lib.rs @@ -30,7 +30,6 @@ pub struct __; #[cfg(feature = "unstable-doc")] pub mod _docs; -// FIXME: finish pub mod annotations; pub mod array; pub mod bundle; @@ -50,5 +49,4 @@ pub mod source_location; pub mod testing; pub mod ty; pub mod util; -//pub mod valueless; pub mod wire; diff --git a/crates/fayalite/src/valueless.rs b/crates/fayalite/src/valueless.rs deleted file mode 100644 index d34905e..0000000 --- a/crates/fayalite/src/valueless.rs +++ /dev/null @@ -1,88 +0,0 @@ -// SPDX-License-Identifier: LGPL-3.0-or-later -// See Notices.txt for copyright information -use crate::{ - int::{DynIntType, DynSIntType, DynUIntType, IntTypeTrait, SIntType}, - ty::{Type, Value}, -}; -use std::ops::RangeBounds; - -#[derive(Copy, Clone, Debug, Hash, Eq, PartialEq, Default)] -pub struct Valueless { - pub ty: T, -} - -impl Valueless { - pub fn to_canonical(&self) -> Valueless { - Valueless { - ty: self.ty.canonical(), - } - } - pub fn from_canonical(v: Valueless) -> Self { - Valueless { - ty: T::from_canonical_type(v.ty), - } - } -} - -mod sealed { - pub trait Sealed {} -} - -pub trait ValuelessTr: sealed::Sealed { - type Type: Type; - type Value: Value; -} - -impl sealed::Sealed for Valueless {} - -impl ValuelessTr for Valueless { - type Type = T; - type Value = T::Value; -} - -impl Valueless { - pub fn signum(&self) -> Valueless> { - Valueless::default() - } - pub fn as_same_width_uint(self) -> Valueless { - Valueless { - ty: self.ty.as_same_width_uint(), - } - } - pub fn as_same_width_sint(self) -> Valueless { - Valueless { - ty: self.ty.as_same_width_sint(), - } - } - pub fn as_same_value_uint(self) -> Valueless { - Valueless { - ty: self.ty.as_same_value_uint(), - } - } - pub fn as_same_value_sint(self) -> Valueless { - Valueless { - ty: self.ty.as_same_value_sint(), - } - } - pub fn concat( - &self, - high_part: Valueless, - ) -> Valueless> { - let ty = DynIntType::new( - self.ty - .width() - .checked_add(high_part.ty.width()) - .expect("result has too many bits"), - ); - Valueless { ty } - } - pub fn repeat(&self, count: usize) -> Valueless> { - let width = self.ty.width(); - let ty = DynIntType::new(width.checked_mul(count).expect("result has too many bits")); - Valueless { ty } - } - pub fn slice>(&self, index: I) -> Valueless { - let ty = self.ty.slice(index); - Valueless { ty } - } -} From f3d6528f5b1e23cb3e9a1ef338c477738c7d7b08 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Tue, 1 Oct 2024 19:54:17 -0700 Subject: [PATCH 3/5] make annotations easier to use --- crates/fayalite/src/annotations.rs | 138 ++++++++++++++++-- crates/fayalite/src/firrtl.rs | 4 +- crates/fayalite/src/module/transform/visit.rs | 2 +- crates/fayalite/src/prelude.rs | 5 +- crates/fayalite/tests/module.rs | 58 ++++---- crates/fayalite/visit_types.json | 7 +- 6 files changed, 163 insertions(+), 51 deletions(-) diff --git a/crates/fayalite/src/annotations.rs b/crates/fayalite/src/annotations.rs index 6b96d01..8eff4a0 100644 --- a/crates/fayalite/src/annotations.rs +++ b/crates/fayalite/src/annotations.rs @@ -8,6 +8,7 @@ use serde::{Deserialize, Serialize}; use std::{ fmt, hash::{Hash, Hasher}, + iter::FusedIterator, ops::Deref, }; @@ -118,6 +119,9 @@ pub struct CustomFirrtlAnnotation { pub additional_fields: CustomFirrtlAnnotationFields, } +#[derive(Copy, Clone, PartialEq, Eq, Debug, Hash, Serialize, Deserialize)] +pub struct DontTouchAnnotation; + #[derive(Copy, Clone, PartialEq, Eq, Debug, Hash, Serialize, Deserialize)] pub struct SVAttributeAnnotation { pub text: Interned, @@ -139,15 +143,63 @@ pub struct DocStringAnnotation { pub text: Interned, } -#[derive(Clone, PartialEq, Eq, Hash, Debug)] -#[non_exhaustive] -pub enum Annotation { - DontTouch, - SVAttribute(SVAttributeAnnotation), - BlackBoxInline(BlackBoxInlineAnnotation), - BlackBoxPath(BlackBoxPathAnnotation), - DocString(DocStringAnnotation), - CustomFirrtl(CustomFirrtlAnnotation), +macro_rules! make_annotation_enum { + ( + $(#[$meta:meta])* + $vis:vis enum $Annotation:ident { + $($Variant:ident($T:ident),)* + } + ) => { + $(#[$meta])* + $vis enum $Annotation { + $($Variant($T),)* + } + + $(impl IntoAnnotations for $T { + type IntoAnnotations = [$Annotation; 1]; + + fn into_annotations(self) -> Self::IntoAnnotations { + [$Annotation::$Variant(self)] + } + } + + impl IntoAnnotations for &'_ $T { + type IntoAnnotations = [$Annotation; 1]; + + fn into_annotations(self) -> Self::IntoAnnotations { + [$Annotation::$Variant(*self)] + } + } + + impl IntoAnnotations for &'_ mut $T { + type IntoAnnotations = [$Annotation; 1]; + + fn into_annotations(self) -> Self::IntoAnnotations { + [$Annotation::$Variant(*self)] + } + } + + impl IntoAnnotations for Box<$T> { + type IntoAnnotations = [$Annotation; 1]; + + fn into_annotations(self) -> Self::IntoAnnotations { + [$Annotation::$Variant(*self)] + } + })* + }; +} + +make_annotation_enum! { + #[derive(Clone, PartialEq, Eq, Hash, Debug)] + #[non_exhaustive] + pub enum Annotation { + DontTouch(DontTouchAnnotation), + SVAttribute(SVAttributeAnnotation), + BlackBoxInline(BlackBoxInlineAnnotation), + BlackBoxPath(BlackBoxPathAnnotation), + DocString(DocStringAnnotation), + CustomFirrtl(CustomFirrtlAnnotation), + } } #[derive(Clone, PartialEq, Eq, Hash, Debug)] @@ -212,10 +264,70 @@ impl IntoAnnotations for &'_ mut Annotation { } } -impl> IntoAnnotations for T { - type IntoAnnotations = Self; +pub struct IterIntoAnnotations> { + outer: T, + inner: Option<<::IntoAnnotations as IntoIterator>::IntoIter>, +} - fn into_annotations(self) -> Self::IntoAnnotations { - self +impl> Iterator for IterIntoAnnotations { + type Item = Annotation; + + fn next(&mut self) -> Option { + loop { + if let Some(inner) = &mut self.inner { + let Some(retval) = inner.next() else { + self.inner = None; + continue; + }; + return Some(retval); + } else { + self.inner = Some(self.outer.next()?.into_annotations().into_iter()); + } + } + } + + fn size_hint(&self) -> (usize, Option) { + if let (0, Some(0)) = self.outer.size_hint() { + self.inner + .as_ref() + .map(|v| v.size_hint()) + .unwrap_or((0, Some(0))) + } else { + ( + self.inner.as_ref().map(|v| v.size_hint().0).unwrap_or(0), + None, + ) + } + } + + fn fold(self, init: B, f: F) -> B + where + Self: Sized, + F: FnMut(B, Self::Item) -> B, + { + self.inner + .into_iter() + .chain(self.outer.map(|v| v.into_annotations().into_iter())) + .flatten() + .fold(init, f) + } +} + +impl< + T: FusedIterator< + Item: IntoAnnotations>, + >, + > FusedIterator for IterIntoAnnotations +{ +} + +impl> IntoAnnotations for T { + type IntoAnnotations = IterIntoAnnotations; + + fn into_annotations(self) -> Self::IntoAnnotations { + IterIntoAnnotations { + outer: self.into_iter(), + inner: None, + } } } diff --git a/crates/fayalite/src/firrtl.rs b/crates/fayalite/src/firrtl.rs index 0be61b5..5a2cc00 100644 --- a/crates/fayalite/src/firrtl.rs +++ b/crates/fayalite/src/firrtl.rs @@ -4,7 +4,7 @@ use crate::{ annotations::{ Annotation, BlackBoxInlineAnnotation, BlackBoxPathAnnotation, CustomFirrtlAnnotation, - DocStringAnnotation, SVAttributeAnnotation, + DocStringAnnotation, DontTouchAnnotation, SVAttributeAnnotation, }, array::Array, bundle::{Bundle, BundleField, BundleType}, @@ -1805,7 +1805,7 @@ impl<'a> Exporter<'a> { } fn annotation(&mut self, path: AnnotationTargetPath, annotation: &Annotation) { let data = match annotation { - Annotation::DontTouch => AnnotationData::DontTouch, + Annotation::DontTouch(DontTouchAnnotation {}) => AnnotationData::DontTouch, Annotation::SVAttribute(SVAttributeAnnotation { text }) => { AnnotationData::AttributeAnnotation { description: *text } } diff --git a/crates/fayalite/src/module/transform/visit.rs b/crates/fayalite/src/module/transform/visit.rs index 77079dd..1165a46 100644 --- a/crates/fayalite/src/module/transform/visit.rs +++ b/crates/fayalite/src/module/transform/visit.rs @@ -4,7 +4,7 @@ use crate::{ annotations::{ Annotation, BlackBoxInlineAnnotation, BlackBoxPathAnnotation, CustomFirrtlAnnotation, - DocStringAnnotation, SVAttributeAnnotation, TargetedAnnotation, + DocStringAnnotation, DontTouchAnnotation, SVAttributeAnnotation, TargetedAnnotation, }, array::ArrayType, bundle::{Bundle, BundleField, BundleType}, diff --git a/crates/fayalite/src/prelude.rs b/crates/fayalite/src/prelude.rs index 16dccb9..c793775 100644 --- a/crates/fayalite/src/prelude.rs +++ b/crates/fayalite/src/prelude.rs @@ -1,7 +1,10 @@ // SPDX-License-Identifier: LGPL-3.0-or-later // See Notices.txt for copyright information pub use crate::{ - annotations::Annotation, + annotations::{ + BlackBoxInlineAnnotation, BlackBoxPathAnnotation, CustomFirrtlAnnotation, + DocStringAnnotation, DontTouchAnnotation, SVAttributeAnnotation, + }, array::{Array, ArrayType}, cli::Cli, clock::{Clock, ClockDomain, ToClock}, diff --git a/crates/fayalite/tests/module.rs b/crates/fayalite/tests/module.rs index 70b3f56..856cbf0 100644 --- a/crates/fayalite/tests/module.rs +++ b/crates/fayalite/tests/module.rs @@ -1,16 +1,8 @@ // SPDX-License-Identifier: LGPL-3.0-or-later // See Notices.txt for copyright information use fayalite::{ - annotations::{ - BlackBoxInlineAnnotation, BlackBoxPathAnnotation, CustomFirrtlAnnotation, - DocStringAnnotation, SVAttributeAnnotation, - }, - assert_export_firrtl, - firrtl::ExportOptions, - intern::Intern, - module::transform::simplify_enums::SimplifyEnumsKind, - prelude::*, - ty::StaticType, + assert_export_firrtl, firrtl::ExportOptions, intern::Intern, + module::transform::simplify_enums::SimplifyEnumsKind, prelude::*, ty::StaticType, }; use serde_json::json; @@ -3057,30 +3049,30 @@ circuit check_memory_of_array_of_enum: #[hdl_module(outline_generated)] pub fn check_annotations() { - m.annotate_module(Annotation::CustomFirrtl(CustomFirrtlAnnotation { + m.annotate_module(CustomFirrtlAnnotation { class: "the.annotation.Example".intern(), additional_fields: json!({ "bar": "a nice module!", }) .try_into() .unwrap(), - })); - m.annotate_module(Annotation::DocString(DocStringAnnotation { + }); + m.annotate_module(DocStringAnnotation { text: r"This module is used as a test that fayalite's firrtl backend properly emits annotations. Testing... " .intern(), - })); + }); #[hdl] let raddr: UInt<8> = m.input(); - annotate(raddr, Annotation::DontTouch); + annotate(raddr, DontTouchAnnotation); #[hdl] let rdata: Array, 2> = m.output(); annotate( rdata, - Annotation::CustomFirrtl(CustomFirrtlAnnotation { + CustomFirrtlAnnotation { class: "the.annotation.ExampleClass".intern(), additional_fields: json!({ "foo": "bar", @@ -3088,7 +3080,7 @@ Testing... }) .try_into() .unwrap(), - }), + }, ); #[hdl] let waddr: UInt<8> = m.input(); @@ -3098,21 +3090,21 @@ Testing... let wmask: Array = m.input(); annotate( wmask[1], - Annotation::CustomFirrtl(CustomFirrtlAnnotation { + CustomFirrtlAnnotation { class: "some.annotation.Class".intern(), additional_fields: json!({ "baz": "second mask bit", }) .try_into() .unwrap(), - }), + }, ); #[hdl] let clk: Clock = m.input(); #[hdl] let mut mem = memory(); mem.depth(0x100); - mem.annotate(Annotation::CustomFirrtl(CustomFirrtlAnnotation { + mem.annotate(CustomFirrtlAnnotation { class: "the.annotation.ExampleClass2".intern(), additional_fields: json!({ "bar": "foo", @@ -3120,18 +3112,18 @@ Testing... }) .try_into() .unwrap(), - })); + }); let read_port = mem.new_read_port(); annotate( read_port, - Annotation::CustomFirrtl(CustomFirrtlAnnotation { + CustomFirrtlAnnotation { class: "the.annotation.ExampleClass3".intern(), additional_fields: json!({ "foo": "my read port", }) .try_into() .unwrap(), - }), + }, ); connect_any(read_port.addr, raddr); connect(read_port.en, true); @@ -3140,14 +3132,14 @@ Testing... let write_port = mem.new_write_port(); annotate( write_port.data[0], - Annotation::CustomFirrtl(CustomFirrtlAnnotation { + CustomFirrtlAnnotation { class: "some.annotation.Class".intern(), additional_fields: json!({ "baz": "first mask bit", }) .try_into() .unwrap(), - }), + }, ); connect_any(write_port.addr, waddr); connect(write_port.en, true); @@ -3157,35 +3149,35 @@ Testing... #[hdl_module(extern)] fn black_box1() { m.verilog_name("BlackBox1"); - m.annotate_module(Annotation::BlackBoxInline(BlackBoxInlineAnnotation { + m.annotate_module(BlackBoxInlineAnnotation { path: "black_box1.v".intern(), text: r"(* blackbox *) module BlackBox1(); endmodule " .intern(), - })); + }); } #[hdl] let black_box1_instance = instance(black_box1()); - annotate(black_box1_instance, Annotation::DontTouch); + annotate(black_box1_instance, DontTouchAnnotation); #[hdl_module(extern)] fn black_box2() { m.verilog_name("BlackBox2"); - m.annotate_module(Annotation::BlackBoxPath(BlackBoxPathAnnotation { + m.annotate_module(BlackBoxPathAnnotation { path: "black_box2.v".intern(), - })); + }); } #[hdl] let black_box2_instance = instance(black_box2()); - annotate(black_box2_instance, Annotation::DontTouch); + annotate(black_box2_instance, DontTouchAnnotation); #[hdl] let a_wire: (SInt<1>, Bool) = wire(); annotate( a_wire.1, - Annotation::SVAttribute(SVAttributeAnnotation { + SVAttributeAnnotation { text: "custom_sv_attr = \"abc\"".intern(), - }), + }, ); connect(a_wire, (0_hdl_i1, false)); } diff --git a/crates/fayalite/visit_types.json b/crates/fayalite/visit_types.json index 7064df2..09ae23f 100644 --- a/crates/fayalite/visit_types.json +++ b/crates/fayalite/visit_types.json @@ -1163,7 +1163,7 @@ "Annotation": { "data": { "$kind": "Enum", - "DontTouch": null, + "DontTouch": "Visible", "SVAttribute": "Visible", "BlackBoxInline": "Visible", "BlackBoxPath": "Visible", @@ -1171,6 +1171,11 @@ "CustomFirrtl": "Visible" } }, + "DontTouchAnnotation": { + "data": { + "$kind": "Struct" + } + }, "SVAttributeAnnotation": { "data": { "$kind": "Struct", From 0cf01600b3b3883929ffb1edae914fa216c9c434 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Tue, 1 Oct 2024 19:56:17 -0700 Subject: [PATCH 4/5] add mod formal and move assert/assume/cover stuff to it --- crates/fayalite/src/firrtl.rs | 11 +- crates/fayalite/src/formal.rs | 186 ++++++++++++++++++ crates/fayalite/src/lib.rs | 1 + crates/fayalite/src/module.rs | 146 ++------------ crates/fayalite/src/module/transform/visit.rs | 5 +- crates/fayalite/src/prelude.rs | 9 +- crates/fayalite/visit_types.json | 2 +- 7 files changed, 218 insertions(+), 142 deletions(-) create mode 100644 crates/fayalite/src/formal.rs diff --git a/crates/fayalite/src/firrtl.rs b/crates/fayalite/src/firrtl.rs index 5a2cc00..ef955ea 100644 --- a/crates/fayalite/src/firrtl.rs +++ b/crates/fayalite/src/firrtl.rs @@ -17,6 +17,7 @@ use crate::{ }, Expr, ExprEnum, }, + formal::FormalKind, int::{Bool, DynSize, IntType, SIntValue, UInt, UIntValue}, intern::{Intern, Interned}, memory::{Mem, PortKind, PortName, ReadUnderWrite}, @@ -27,8 +28,8 @@ use crate::{ }, AnnotatedModuleIO, Block, ExternModuleBody, ExternModuleParameter, ExternModuleParameterValue, Module, ModuleBody, NameId, NormalModuleBody, Stmt, - StmtConnect, StmtDeclaration, StmtFormal, StmtFormalKind, StmtIf, StmtInstance, StmtMatch, - StmtReg, StmtWire, + StmtConnect, StmtDeclaration, StmtFormal, StmtIf, StmtInstance, StmtMatch, StmtReg, + StmtWire, }, reset::{AsyncReset, Reset, SyncReset}, source_location::SourceLocation, @@ -2011,9 +2012,9 @@ impl<'a> Exporter<'a> { let pred = self.expr(Expr::canonical(pred), &definitions, false); let en = self.expr(Expr::canonical(en), &definitions, false); let kind = match kind { - StmtFormalKind::Assert => "assert", - StmtFormalKind::Assume => "assume", - StmtFormalKind::Cover => "cover", + FormalKind::Assert => "assert", + FormalKind::Assume => "assume", + FormalKind::Cover => "cover", }; let text = EscapedString { value: &text, diff --git a/crates/fayalite/src/formal.rs b/crates/fayalite/src/formal.rs new file mode 100644 index 0000000..5e90b59 --- /dev/null +++ b/crates/fayalite/src/formal.rs @@ -0,0 +1,186 @@ +// SPDX-License-Identifier: LGPL-3.0-or-later +// See Notices.txt for copyright information +use crate::{intern::Intern, prelude::*}; + +#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)] +pub enum FormalKind { + Assert, + Assume, + Cover, +} + +impl FormalKind { + pub fn as_str(self) -> &'static str { + match self { + Self::Assert => "assert", + Self::Assume => "assume", + Self::Cover => "cover", + } + } +} + +#[track_caller] +pub fn formal_stmt_with_enable_and_loc( + kind: FormalKind, + clk: Expr, + pred: Expr, + en: Expr, + text: &str, + source_location: SourceLocation, +) { + crate::module::add_stmt_formal(crate::module::StmtFormal { + kind, + clk, + pred, + en, + text: text.intern(), + source_location, + }); +} + +#[track_caller] +pub fn formal_stmt_with_enable( + kind: FormalKind, + clk: Expr, + pred: Expr, + en: Expr, + text: &str, +) { + formal_stmt_with_enable_and_loc(kind, clk, pred, en, text, SourceLocation::caller()); +} + +#[track_caller] +pub fn formal_stmt_with_loc( + kind: FormalKind, + clk: Expr, + pred: Expr, + text: &str, + source_location: SourceLocation, +) { + formal_stmt_with_enable_and_loc(kind, clk, pred, true.to_expr(), text, source_location); +} + +#[track_caller] +pub fn formal_stmt(kind: FormalKind, clk: Expr, pred: Expr, text: &str) { + formal_stmt_with_loc(kind, clk, pred, text, SourceLocation::caller()); +} + +macro_rules! make_formal { + ($kind:ident, $formal_stmt_with_enable_and_loc:ident, $formal_stmt_with_enable:ident, $formal_stmt_with_loc:ident, $formal_stmt:ident) => { + #[track_caller] + pub fn $formal_stmt_with_enable_and_loc( + clk: Expr, + pred: Expr, + en: Expr, + text: &str, + source_location: SourceLocation, + ) { + formal_stmt_with_enable_and_loc( + FormalKind::$kind, + clk, + pred, + en, + text, + source_location, + ); + } + #[track_caller] + pub fn $formal_stmt_with_enable( + clk: Expr, + pred: Expr, + en: Expr, + text: &str, + ) { + formal_stmt_with_enable(FormalKind::$kind, clk, pred, en, text); + } + #[track_caller] + pub fn $formal_stmt_with_loc( + clk: Expr, + pred: Expr, + text: &str, + source_location: SourceLocation, + ) { + formal_stmt_with_loc(FormalKind::$kind, clk, pred, text, source_location); + } + #[track_caller] + pub fn $formal_stmt(clk: Expr, pred: Expr, text: &str) { + formal_stmt(FormalKind::$kind, clk, pred, text); + } + }; +} + +make_formal!( + Assert, + hdl_assert_with_enable_and_loc, + hdl_assert_with_enable, + hdl_assert_with_loc, + hdl_assert +); + +make_formal!( + Assume, + hdl_assume_with_enable_and_loc, + hdl_assume_with_enable, + hdl_assume_with_loc, + hdl_assume +); + +make_formal!( + Cover, + hdl_cover_with_enable_and_loc, + hdl_cover_with_enable, + hdl_cover_with_loc, + hdl_cover +); + +pub trait MakeFormalExpr: Type {} + +impl MakeFormalExpr for T {} + +#[hdl] +pub fn formal_global_clock() -> Expr { + #[hdl_module(extern)] + fn formal_global_clock() { + #[hdl] + let clk: Clock = m.output(); + m.annotate_module(BlackBoxInlineAnnotation { + path: "fayalite_formal_global_clock.v".intern(), + text: r"module __fayalite_formal_global_clock(output clk); + (* gclk *) + reg clk; +endmodule +" + .intern(), + }); + m.verilog_name("__fayalite_formal_global_clock"); + } + #[hdl] + let formal_global_clock = instance(formal_global_clock()); + formal_global_clock.clk +} + +#[hdl] +pub fn formal_reset() -> Expr { + #[hdl_module(extern)] + fn formal_reset() { + #[hdl] + let rst: AsyncReset = m.output(); + 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; +endmodule +" + .intern(), + }); + m.verilog_name("__fayalite_formal_reset"); + } + #[hdl] + let formal_reset = instance(formal_reset()); + formal_reset.rst +} diff --git a/crates/fayalite/src/lib.rs b/crates/fayalite/src/lib.rs index 6e1ccd3..eedb1bb 100644 --- a/crates/fayalite/src/lib.rs +++ b/crates/fayalite/src/lib.rs @@ -38,6 +38,7 @@ pub mod clock; pub mod enum_; pub mod expr; pub mod firrtl; +pub mod formal; pub mod int; pub mod intern; pub mod memory; diff --git a/crates/fayalite/src/module.rs b/crates/fayalite/src/module.rs index f93758a..872c75f 100644 --- a/crates/fayalite/src/module.rs +++ b/crates/fayalite/src/module.rs @@ -15,6 +15,7 @@ use crate::{ }, Expr, Flow, ToExpr, }, + formal::FormalKind, int::{Bool, DynSize, Size}, intern::{Intern, Interned}, memory::{Mem, MemBuilder, MemBuilderTarget, PortName}, @@ -233,26 +234,9 @@ impl fmt::Debug for StmtConnect { } } -#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)] -pub enum StmtFormalKind { - Assert, - Assume, - Cover, -} - -impl StmtFormalKind { - pub fn as_str(self) -> &'static str { - match self { - Self::Assert => "assert", - Self::Assume => "assume", - Self::Cover => "cover", - } - } -} - #[derive(Clone, PartialEq, Eq, Hash)] pub struct StmtFormal { - pub kind: StmtFormalKind, + pub kind: FormalKind, pub clk: Expr, pub pred: Expr, pub en: Expr, @@ -279,6 +263,19 @@ impl fmt::Debug for StmtFormal { } } +#[track_caller] +pub(crate) fn add_stmt_formal(formal: StmtFormal) { + ModuleBuilder::with(|m| { + m.impl_ + .borrow_mut() + .body + .builder_normal_body() + .block(m.block_stack.top()) + .stmts + .push(formal.into()); + }); +} + #[derive(Clone, PartialEq, Eq, Hash)] pub struct StmtIf { pub cond: Expr, @@ -2439,119 +2436,6 @@ pub fn match_with_loc( T::match_variants(expr.to_expr(), source_location) } -#[track_caller] -pub fn formal_with_enable_and_loc( - kind: StmtFormalKind, - clk: Expr, - pred: Expr, - en: Expr, - text: &str, - source_location: SourceLocation, -) { - ModuleBuilder::with(|m| { - m.impl_ - .borrow_mut() - .body - .builder_normal_body() - .block(m.block_stack.top()) - .stmts - .push( - StmtFormal { - kind, - clk, - pred, - en, - text: text.intern(), - source_location, - } - .into(), - ); - }); -} - -#[track_caller] -pub fn formal_with_enable( - kind: StmtFormalKind, - clk: Expr, - pred: Expr, - en: Expr, - text: &str, -) { - formal_with_enable_and_loc(kind, clk, pred, en, text, SourceLocation::caller()); -} - -#[track_caller] -pub fn formal_with_loc( - kind: StmtFormalKind, - clk: Expr, - pred: Expr, - text: &str, - source_location: SourceLocation, -) { - formal_with_enable_and_loc(kind, clk, pred, true.to_expr(), text, source_location); -} - -#[track_caller] -pub fn formal(kind: StmtFormalKind, clk: Expr, pred: Expr, text: &str) { - formal_with_loc(kind, clk, pred, text, SourceLocation::caller()); -} - -macro_rules! make_formal { - ($kind:ident, $formal_with_enable_and_loc:ident, $formal_with_enable:ident, $formal_with_loc:ident, $formal:ident) => { - #[track_caller] - pub fn $formal_with_enable_and_loc( - clk: Expr, - pred: Expr, - en: Expr, - text: &str, - source_location: SourceLocation, - ) { - formal_with_enable_and_loc(StmtFormalKind::$kind, clk, pred, en, text, source_location); - } - #[track_caller] - pub fn $formal_with_enable(clk: Expr, pred: Expr, en: Expr, text: &str) { - formal_with_enable(StmtFormalKind::$kind, clk, pred, en, text); - } - #[track_caller] - pub fn $formal_with_loc( - clk: Expr, - pred: Expr, - text: &str, - source_location: SourceLocation, - ) { - formal_with_loc(StmtFormalKind::$kind, clk, pred, text, source_location); - } - #[track_caller] - pub fn $formal(clk: Expr, pred: Expr, text: &str) { - formal(StmtFormalKind::$kind, clk, pred, text); - } - }; -} - -make_formal!( - Assert, - hdl_assert_with_enable_and_loc, - hdl_assert_with_enable, - hdl_assert_with_loc, - hdl_assert -); - -make_formal!( - Assume, - hdl_assume_with_enable_and_loc, - hdl_assume_with_enable, - hdl_assume_with_loc, - hdl_assume -); - -make_formal!( - Cover, - hdl_cover_with_enable_and_loc, - hdl_cover_with_enable, - hdl_cover_with_loc, - hdl_cover -); - #[track_caller] pub fn connect_any_with_loc( lhs: Lhs, diff --git a/crates/fayalite/src/module/transform/visit.rs b/crates/fayalite/src/module/transform/visit.rs index 1165a46..2e1e48f 100644 --- a/crates/fayalite/src/module/transform/visit.rs +++ b/crates/fayalite/src/module/transform/visit.rs @@ -18,14 +18,15 @@ use crate::{ }, Expr, ExprEnum, }, + formal::FormalKind, int::{Bool, SIntType, SIntValue, Size, UIntType, UIntValue}, intern::{Intern, Interned}, memory::{Mem, MemPort, PortKind, PortName, PortType, ReadUnderWrite}, module::{ AnnotatedModuleIO, Block, BlockId, ExternModuleBody, ExternModuleParameter, ExternModuleParameterValue, Instance, Module, ModuleBody, ModuleIO, NameId, - NormalModuleBody, ScopedNameId, Stmt, StmtConnect, StmtDeclaration, StmtFormal, - StmtFormalKind, StmtIf, StmtInstance, StmtMatch, StmtReg, StmtWire, + NormalModuleBody, ScopedNameId, Stmt, StmtConnect, StmtDeclaration, StmtFormal, StmtIf, + StmtInstance, StmtMatch, StmtReg, StmtWire, }, reg::Reg, reset::{AsyncReset, Reset, SyncReset}, diff --git a/crates/fayalite/src/prelude.rs b/crates/fayalite/src/prelude.rs index c793775..f1a9736 100644 --- a/crates/fayalite/src/prelude.rs +++ b/crates/fayalite/src/prelude.rs @@ -13,13 +13,16 @@ pub use crate::{ repeat, CastBitsTo, CastTo, CastToBits, Expr, HdlPartialEq, HdlPartialOrd, MakeUninitExpr, 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, + }, hdl, hdl_module, int::{Bool, DynSize, KnownSize, SInt, SIntType, Size, UInt, UIntType}, memory::{Mem, MemBuilder, ReadUnderWrite}, module::{ - annotate, connect, connect_any, hdl_assert, hdl_assert_with_enable, hdl_assume, - hdl_assume_with_enable, hdl_cover, hdl_cover_with_enable, incomplete_wire, instance, - memory, memory_array, memory_with_init, reg_builder, wire, Instance, Module, ModuleBuilder, + annotate, connect, connect_any, incomplete_wire, instance, memory, memory_array, + memory_with_init, reg_builder, wire, Instance, Module, ModuleBuilder, }, reg::Reg, reset::{AsyncReset, Reset, SyncReset, ToAsyncReset, ToReset, ToSyncReset}, diff --git a/crates/fayalite/visit_types.json b/crates/fayalite/visit_types.json index 09ae23f..366ee2f 100644 --- a/crates/fayalite/visit_types.json +++ b/crates/fayalite/visit_types.json @@ -1089,7 +1089,7 @@ "source_location": "Visible" } }, - "StmtFormalKind": { + "FormalKind": { "data": { "$kind": "Enum", "Assert": null, From 1c63a441a9ca35edfaec23fee0de21b6d48f4c10 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Thu, 3 Oct 2024 00:27:28 -0700 Subject: [PATCH 5/5] add needed tools to CI --- .forgejo/workflows/test.yml | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/.forgejo/workflows/test.yml b/.forgejo/workflows/test.yml index 6e82abf..762c1f8 100644 --- a/.forgejo/workflows/test.yml +++ b/.forgejo/workflows/test.yml @@ -11,10 +11,28 @@ jobs: fetch-depth: 0 - run: | scripts/check-copyright.sh + - run: | + apt-get update -qq + apt-get install -qq cvc5 z3 - run: | curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain 1.80.1 source "$HOME/.cargo/env" echo "$PATH" >> "$GITHUB_PATH" + - run: | + git clone --depth=1 --branch=yosys-0.45 https://github.com/YosysHQ/sby.git + make -C sby install + - run: | + git clone --depth=1 --branch=0.45 https://github.com/YosysHQ/yosys.git + cd yosys + autoconf -f + ./configure + make install -j6 + - run: | + wget -O firrtl.tar.gz https://github.com/llvm/circt/releases/download/firtool-1.86.0/firrtl-bin-linux-x64.tar.gz + sha256sum -c - <<<'bf6f4ab18ae76f135c944efbd81e25391c31c1bd0617c58ab0592640abefee14 firrtl.tar.gz' + tar -xvaf firrtl.tar.gz + export PATH="$(realpath firtool-1.86.0/bin):$PATH" + echo "$PATH" >> "$GITHUB_PATH" - uses: https://github.com/Swatinem/rust-cache@v2 with: save-if: ${{ github.ref == 'refs/heads/master' }}