move FormalMode to crate::testing and add to prelude

crates/fayalite/src/build/formal.rs

@@ -13,9 +13,10 @@ use crate::{
     },
     intern::{Intern, InternSlice, Interned},
     module::NameId,
+    testing::FormalMode,
     util::job_server::AcquiredJob,
 };
-use clap::{Args, ValueEnum};
+use clap::Args;
 use eyre::Context;
 use serde::{Deserialize, Serialize};
 use std::{
@@ -24,33 +25,6 @@ use std::{
     path::Path,
 };
 
-#[derive(ValueEnum, Copy, Clone, Debug, PartialEq, Eq, Hash, Default, Deserialize, Serialize)]
-#[non_exhaustive]
-pub enum FormalMode {
-    #[default]
-    BMC,
-    Prove,
-    Live,
-    Cover,
-}
-
-impl FormalMode {
-    pub fn as_str(self) -> &'static str {
-        match self {
-            FormalMode::BMC => "bmc",
-            FormalMode::Prove => "prove",
-            FormalMode::Live => "live",
-            FormalMode::Cover => "cover",
-        }
-    }
-}
-
-impl fmt::Display for FormalMode {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        f.write_str(self.as_str())
-    }
-}
-
 #[derive(Args, Clone, Debug, PartialEq, Eq, Hash)]
 #[non_exhaustive]
 pub struct FormalArgs {

crates/fayalite/src/prelude.rs

@@ -37,7 +37,7 @@ pub use crate::{
         value::{SimOnly, SimOnlyValue, SimValue, ToSimValue, ToSimValueWithType},
     },
     source_location::SourceLocation,
-    testing::assert_formal,
+    testing::{FormalMode, assert_formal},
     ty::{AsMask, CanonicalType, Type},
     util::{ConstUsize, GenericConstUsize},
     wire::Wire,

crates/fayalite/src/testing.rs

@@ -6,7 +6,7 @@ use crate::{
         NoArgs, RunBuild,
         external::{ExternalCommandArgs, ExternalCommandJobKind},
         firrtl::{FirrtlArgs, FirrtlJobKind},
-        formal::{Formal, FormalAdditionalArgs, FormalArgs, FormalMode, WriteSbyFileJobKind},
+        formal::{Formal, FormalAdditionalArgs, FormalArgs, WriteSbyFileJobKind},
         verilog::{UnadjustedVerilogArgs, VerilogJobArgs, VerilogJobKind},
     },
     bundle::BundleType,
@@ -14,14 +14,43 @@ use crate::{
     module::Module,
     util::HashMap,
 };
-use serde::Deserialize;
+use serde::{Deserialize, Serialize};
 use std::{
-    fmt::Write,
+    fmt::{self, Write},
     path::{Path, PathBuf},
     process::Command,
     sync::{Mutex, OnceLock},
 };
 
+#[derive(
+    clap::ValueEnum, Copy, Clone, Debug, PartialEq, Eq, Hash, Default, Deserialize, Serialize,
+)]
+#[non_exhaustive]
+pub enum FormalMode {
+    #[default]
+    BMC,
+    Prove,
+    Live,
+    Cover,
+}
+
+impl FormalMode {
+    pub fn as_str(self) -> &'static str {
+        match self {
+            FormalMode::BMC => "bmc",
+            FormalMode::Prove => "prove",
+            FormalMode::Live => "live",
+            FormalMode::Cover => "cover",
+        }
+    }
+}
+
+impl fmt::Display for FormalMode {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.write_str(self.as_str())
+    }
+}
+
 #[derive(Deserialize)]
 struct CargoMetadata {
     target_directory: String,

crates/fayalite/src/util/ready_valid.rs

@@ -212,9 +212,7 @@ pub fn queue<T: Type>(
 mod tests {
     use super::*;
     use crate::{
-        build::formal::FormalMode, firrtl::ExportOptions,
-        module::transform::simplify_enums::SimplifyEnumsKind, testing::assert_formal,
-        ty::StaticType,
+        firrtl::ExportOptions, module::transform::simplify_enums::SimplifyEnumsKind, ty::StaticType,
     };
     use std::num::NonZero;
 

crates/fayalite/tests/formal.rs

@@ -2,19 +2,7 @@
 // See Notices.txt for copyright information
 //! Formal tests in Fayalite
 
-use fayalite::{
-    build::formal::FormalMode,
-    clock::{Clock, ClockDomain},
-    expr::{CastTo, HdlPartialEq},
-    firrtl::ExportOptions,
-    formal::{any_const, any_seq, formal_reset, hdl_assert, hdl_assume},
-    hdl, hdl_module,
-    int::{Bool, DynSize, Size, UInt, UIntType},
-    module::{connect, connect_any, instance, memory, reg_builder, wire},
-    reset::ToReset,
-    testing::assert_formal,
-    ty::StaticType,
-};
+use fayalite::prelude::*;
 
 /// Test hidden state
 ///
@@ -119,7 +107,7 @@ mod hidden_state {
             FormalMode::Prove,
             16,
             None,
-            ExportOptions::default(),
+            Default::default(),
         );
         // here a couple of cycles is enough
         assert_formal(
@@ -128,7 +116,7 @@ mod hidden_state {
             FormalMode::Prove,
             2,
             None,
-            ExportOptions::default(),
+            Default::default(),
         );
     }
 }
@@ -242,7 +230,7 @@ mod memory {
             #[hdl]
             let wr: WritePort<DynSize> = wire(WritePort[n]);
             connect(wr.addr, any_seq(UInt[n]));
-            connect(wr.data, any_seq(UInt::<8>::TYPE));
+            connect(wr.data, any_seq(UInt::<8>::new_static()));
             connect(wr.en, any_seq(Bool));
             #[hdl]
             let dut = instance(example_sram(n));
@@ -289,7 +277,7 @@ mod memory {
             FormalMode::Prove,
             2,
             None,
-            ExportOptions::default(),
+            Default::default(),
         );
     }
 }