add mod formal and move assert/assume/cover stuff to it

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,
+        StmtConnect, StmtDeclaration, StmtFormal, StmtIf, StmtInstance, StmtMatch, StmtReg,
-        StmtReg, StmtWire,
+        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",
+                        FormalKind::Assert => "assert",
-                        StmtFormalKind::Assume => "assume",
+                        FormalKind::Assume => "assume",
-                        StmtFormalKind::Cover => "cover",
+                        FormalKind::Cover => "cover",
                     };
                     let text = EscapedString {
                         value: &text,

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<Clock>,
+    pred: Expr<Bool>,
+    en: Expr<Bool>,
+    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<Clock>,
+    pred: Expr<Bool>,
+    en: Expr<Bool>,
+    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<Clock>,
+    pred: Expr<Bool>,
+    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<Clock>, pred: Expr<Bool>, 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<Clock>,
+            pred: Expr<Bool>,
+            en: Expr<Bool>,
+            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<Clock>,
+            pred: Expr<Bool>,
+            en: Expr<Bool>,
+            text: &str,
+        ) {
+            formal_stmt_with_enable(FormalKind::$kind, clk, pred, en, text);
+        }
+        #[track_caller]
+        pub fn $formal_stmt_with_loc(
+            clk: Expr<Clock>,
+            pred: Expr<Bool>,
+            text: &str,
+            source_location: SourceLocation,
+        ) {
+            formal_stmt_with_loc(FormalKind::$kind, clk, pred, text, source_location);
+        }
+        #[track_caller]
+        pub fn $formal_stmt(clk: Expr<Clock>, pred: Expr<Bool>, 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<T: Type> MakeFormalExpr for T {}
+
+#[hdl]
+pub fn formal_global_clock() -> Expr<Clock> {
+    #[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<AsyncReset> {
+    #[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
+}

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;

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<Clock>,
     pub pred: Expr<Bool>,
     pub en: Expr<Bool>,
@@ -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<S: ModuleBuildingStatus = ModuleBuilt> {
     pub cond: Expr<Bool>,
@@ -2439,119 +2436,6 @@ 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/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,
+        NormalModuleBody, ScopedNameId, Stmt, StmtConnect, StmtDeclaration, StmtFormal, StmtIf,
-        StmtFormalKind, StmtIf, StmtInstance, StmtMatch, StmtReg, StmtWire,
+        StmtInstance, StmtMatch, StmtReg, StmtWire,
     },
     reg::Reg,
     reset::{AsyncReset, Reset, SyncReset},

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,
+        annotate, connect, connect_any, incomplete_wire, instance, memory, memory_array,
-        hdl_assume_with_enable, hdl_cover, hdl_cover_with_enable, incomplete_wire, instance,
+        memory_with_init, reg_builder, wire, Instance, Module, ModuleBuilder,
-        memory, memory_array, memory_with_init, reg_builder, wire, Instance, Module, ModuleBuilder,
     },
     reg::Reg,
     reset::{AsyncReset, Reset, SyncReset, ToAsyncReset, ToReset, ToSyncReset},

crates/fayalite/visit_types.json

@@ -1089,7 +1089,7 @@
                 "source_location": "Visible"
             }
         },
-        "StmtFormalKind": {
+        "FormalKind": {
             "data": {
                 "$kind": "Enum",
                 "Assert": null,