diff --git a/crates/fayalite/src/firrtl.rs b/crates/fayalite/src/firrtl.rs index dbbdd7d..b8ba89a 100644 --- a/crates/fayalite/src/firrtl.rs +++ b/crates/fayalite/src/firrtl.rs @@ -20,8 +20,8 @@ use crate::{ module::{ transform::simplify_memories::simplify_memories, AnnotatedModuleIO, Block, ExternModuleBody, ExternModuleParameter, ExternModuleParameterValue, Module, ModuleBody, - NameId, NormalModuleBody, Stmt, StmtConnect, StmtDeclaration, StmtIf, StmtInstance, - StmtMatch, StmtReg, StmtWire, + NameId, NormalModuleBody, Stmt, StmtConnect, StmtDeclaration, StmtFormal, StmtFormalKind, + StmtIf, StmtInstance, StmtMatch, StmtReg, StmtWire, }, reset::{AsyncReset, Reset, SyncReset}, source_location::SourceLocation, @@ -1954,6 +1954,33 @@ impl<'a> Exporter<'a> { ) .unwrap(); } + Stmt::Formal(StmtFormal { + kind, + clk, + pred, + en, + text, + source_location, + }) => { + let clk = self.expr(Expr::canonical(clk), &definitions, false); + 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", + }; + let text = EscapedString { + value: &text, + raw: false, + }; + writeln!( + body, + "{indent}{kind}({clk}, {pred}, {en}, {text}){}", + FileInfo::new(source_location), + ) + .unwrap(); + } Stmt::If(StmtIf { mut cond, mut source_location, diff --git a/crates/fayalite/src/module.rs b/crates/fayalite/src/module.rs index 3a17343..2b7534c 100644 --- a/crates/fayalite/src/module.rs +++ b/crates/fayalite/src/module.rs @@ -5,7 +5,7 @@ use crate::{ annotations::{Annotation, IntoAnnotations, TargetedAnnotation}, array::ArrayType, bundle::{Bundle, BundleField, BundleType}, - clock::ClockDomain, + clock::{Clock, ClockDomain}, enum_::{Enum, EnumMatchVariantsIter, EnumType}, expr::{ ops::VariantAccess, @@ -199,6 +199,52 @@ 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 clk: Expr, + pub pred: Expr, + pub en: Expr, + pub text: Interned, + pub source_location: SourceLocation, +} + +impl fmt::Debug for StmtFormal { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + let Self { + kind, + clk, + pred, + en, + text, + source_location: _, + } = self; + f.debug_struct(kind.as_str()) + .field("clk", clk) + .field("pred", pred) + .field("en", en) + .field("text", text) + .finish_non_exhaustive() + } +} + #[derive(Clone, PartialEq, Eq, Hash)] pub struct StmtIf { pub cond: Expr, @@ -450,6 +496,8 @@ wrapper_enum! { pub enum Stmt { #[is = is_connect, as_ref = connect] Connect(StmtConnect), + #[is = is_formal, as_ref = formal] + Formal(StmtFormal), #[is = is_if, as_ref = if_] If(StmtIf), #[is = is_match, as_ref = match_] @@ -462,7 +510,7 @@ wrapper_enum! { impl Stmt { pub fn sub_stmt_blocks(&self) -> &[S::Block] { match self { - Stmt::Connect(_) => &[], + Stmt::Connect(_) | Stmt::Formal(_) => &[], Stmt::If(v) => &v.blocks, Stmt::Match(v) => &v.blocks, Stmt::Declaration(v) => v.sub_stmt_blocks(), @@ -609,6 +657,14 @@ impl NameIdGen { rhs: _, source_location: _, }) + | Stmt::Formal(StmtFormal { + kind: _, + clk: _, + pred: _, + en: _, + text: _, + source_location: _, + }) | Stmt::If(StmtIf { cond: _, source_location: _, @@ -888,6 +944,7 @@ impl From> for NormalModuleBody { let stmts = Interned::from_iter(stmts.into_iter().map(|stmt| { match stmt { Stmt::Connect(stmt) => stmt.into(), + Stmt::Formal(stmt) => stmt.into(), Stmt::If(StmtIf { cond, source_location, @@ -1608,6 +1665,7 @@ impl AssertValidityState { self.set_connect_side_written(lhs, source_location, true, block); self.set_connect_side_written(rhs, source_location, false, block); } + Stmt::Formal(_) => {} Stmt::If(if_stmt) => { let sub_blocks = if_stmt.blocks.map(|block| self.make_block_index(block)); self.process_conditional_sub_blocks(block, sub_blocks) @@ -2336,6 +2394,119 @@ 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/simplify_enums.rs b/crates/fayalite/src/module/transform/simplify_enums.rs index 9e1e552..c817e45 100644 --- a/crates/fayalite/src/module/transform/simplify_enums.rs +++ b/crates/fayalite/src/module/transform/simplify_enums.rs @@ -538,7 +538,9 @@ impl Folder for State { } .into()), }, - Stmt::Connect(_) | Stmt::If(_) | Stmt::Declaration(_) => stmt.default_fold(self), + Stmt::Connect(_) | Stmt::Formal(_) | Stmt::If(_) | Stmt::Declaration(_) => { + stmt.default_fold(self) + } } } diff --git a/crates/fayalite/src/module/transform/visit.rs b/crates/fayalite/src/module/transform/visit.rs index 7edfe04..440eecb 100644 --- a/crates/fayalite/src/module/transform/visit.rs +++ b/crates/fayalite/src/module/transform/visit.rs @@ -21,8 +21,8 @@ use crate::{ module::{ AnnotatedModuleIO, Block, BlockId, ExternModuleBody, ExternModuleParameter, ExternModuleParameterValue, Instance, Module, ModuleBody, ModuleIO, NameId, - NormalModuleBody, ScopedNameId, Stmt, StmtConnect, StmtDeclaration, StmtIf, StmtInstance, - StmtMatch, StmtReg, StmtWire, + NormalModuleBody, ScopedNameId, Stmt, StmtConnect, StmtDeclaration, StmtFormal, + StmtFormalKind, 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 7b7d718..16dccb9 100644 --- a/crates/fayalite/src/prelude.rs +++ b/crates/fayalite/src/prelude.rs @@ -14,8 +14,9 @@ pub use crate::{ int::{Bool, DynSize, KnownSize, SInt, SIntType, Size, UInt, UIntType}, memory::{Mem, MemBuilder, ReadUnderWrite}, module::{ - annotate, connect, connect_any, incomplete_wire, instance, memory, memory_array, - memory_with_init, reg_builder, wire, Instance, Module, ModuleBuilder, + 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, }, reg::Reg, reset::{AsyncReset, Reset, SyncReset, ToAsyncReset, ToReset, ToSyncReset}, diff --git a/crates/fayalite/tests/module.rs b/crates/fayalite/tests/module.rs index c135f51..4139ee1 100644 --- a/crates/fayalite/tests/module.rs +++ b/crates/fayalite/tests/module.rs @@ -3182,3 +3182,55 @@ circuit check_uninit_1: ", }; } + +#[hdl_module(outline_generated)] +pub fn check_formal() { + #[hdl] + let clk: Clock = m.input(); + #[hdl] + let en1: Bool = m.input(); + #[hdl] + let en2: Bool = m.input(); + #[hdl] + let en3: Bool = m.input(); + #[hdl] + let pred1: Bool = m.input(); + #[hdl] + let pred2: Bool = m.input(); + #[hdl] + let pred3: Bool = m.input(); + hdl_assert_with_enable(clk, pred1, en1, "en check 1"); + hdl_assume_with_enable(clk, pred2, en2, "en check 2"); + hdl_cover_with_enable(clk, pred3, en3, "en check 3"); + hdl_assert(clk, pred1, "check 1"); + hdl_assume(clk, pred2, "check 2"); + hdl_cover(clk, pred3, "check 3"); +} + +#[test] +fn test_formal() { + let _n = SourceLocation::normalize_files_for_tests(); + let m = check_formal(); + dbg!(m); + #[rustfmt::skip] // work around https://github.com/rust-lang/rustfmt/issues/6161 + assert_export_firrtl! { + m => + "/test/check_formal.fir": r#"FIRRTL version 3.2.0 +circuit check_formal: + module check_formal: @[module-XXXXXXXXXX.rs 1:1] + input clk: Clock @[module-XXXXXXXXXX.rs 2:1] + input en1: UInt<1> @[module-XXXXXXXXXX.rs 3:1] + input en2: UInt<1> @[module-XXXXXXXXXX.rs 4:1] + input en3: UInt<1> @[module-XXXXXXXXXX.rs 5:1] + 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] + assert(clk, pred1, en1, "en check 1") @[module-XXXXXXXXXX.rs 9:1] + assume(clk, pred2, en2, "en check 2") @[module-XXXXXXXXXX.rs 10:1] + cover(clk, pred3, en3, "en check 3") @[module-XXXXXXXXXX.rs 11:1] + assert(clk, pred1, UInt<1>(0h1), "check 1") @[module-XXXXXXXXXX.rs 12:1] + assume(clk, pred2, UInt<1>(0h1), "check 2") @[module-XXXXXXXXXX.rs 13:1] + cover(clk, pred3, UInt<1>(0h1), "check 3") @[module-XXXXXXXXXX.rs 14:1] +"#, + }; +} diff --git a/crates/fayalite/visit_types.json b/crates/fayalite/visit_types.json index cbaae05..f1969eb 100644 --- a/crates/fayalite/visit_types.json +++ b/crates/fayalite/visit_types.json @@ -1067,6 +1067,7 @@ "data": { "$kind": "Enum", "Connect": "Visible", + "Formal": "Visible", "If": "Visible", "Match": "Visible", "Declaration": "Visible" @@ -1088,6 +1089,25 @@ "source_location": "Visible" } }, + "StmtFormalKind": { + "data": { + "$kind": "Enum", + "Assert": null, + "Assume": null, + "Cover": null + } + }, + "StmtFormal": { + "data": { + "$kind": "Struct", + "kind": "Visible", + "clk": "Visible", + "pred": "Visible", + "en": "Visible", + "text": "Visible", + "source_location": "Visible" + } + }, "StmtIf": { "data": { "$kind": "Struct",