add assert/assume/cover

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,

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<Clock>,
+    pub pred: Expr<Bool>,
+    pub en: Expr<Bool>,
+    pub text: Interned<str>,
+    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<S: ModuleBuildingStatus = ModuleBuilt> {
     pub cond: Expr<Bool>,
@@ -450,6 +496,8 @@ wrapper_enum! {
     pub enum Stmt<S: ModuleBuildingStatus = ModuleBuilt> {
         #[is = is_connect, as_ref = connect]
         Connect(StmtConnect),
+        #[is = is_formal, as_ref = formal]
+        Formal(StmtFormal),
         #[is = is_if, as_ref = if_]
         If(StmtIf<S>),
         #[is = is_match, as_ref = match_]
@@ -462,7 +510,7 @@ wrapper_enum! {
 impl<S: ModuleBuildingStatus> Stmt<S> {
     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<NormalModuleBody<ModuleBuilding>> 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: Type>(
     T::match_variants(expr.to_expr(), source_location)
 }
 
+#[track_caller]
+pub fn formal_with_enable_and_loc(
+    kind: StmtFormalKind,
+    clk: Expr<Clock>,
+    pred: Expr<Bool>,
+    en: Expr<Bool>,
+    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<Clock>,
+    pred: Expr<Bool>,
+    en: Expr<Bool>,
+    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<Clock>,
+    pred: Expr<Bool>,
+    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<Clock>, pred: Expr<Bool>, 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<Clock>,
+            pred: Expr<Bool>,
+            en: Expr<Bool>,
+            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<Clock>, pred: Expr<Bool>, en: Expr<Bool>, text: &str) {
+            formal_with_enable(StmtFormalKind::$kind, clk, pred, en, text);
+        }
+        #[track_caller]
+        pub fn $formal_with_loc(
+            clk: Expr<Clock>,
+            pred: Expr<Bool>,
+            text: &str,
+            source_location: SourceLocation,
+        ) {
+            formal_with_loc(StmtFormalKind::$kind, clk, pred, text, source_location);
+        }
+        #[track_caller]
+        pub fn $formal(clk: Expr<Clock>, pred: Expr<Bool>, 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: ToExpr, Rhs: ToExpr>(
     lhs: Lhs,

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)
+            }
         }
     }
 

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},

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},

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]
+"#,
+    };
+}

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",