use crate::{
int::BoolOrIntType,
intern::{Intern, Interned, Memoize},
prelude::*,
};
use std::sync::OnceLock;
#[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: en & !formal_reset().cast_to_static::<Bool>(),
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<SyncReset> {
#[hdl_module(extern)]
fn formal_reset() {
#[hdl]
let rst: SyncReset = m.output();
m.annotate_module(BlackBoxInlineAnnotation {
path: "fayalite_formal_reset.v".intern(),
text: r"module __fayalite_formal_reset(output rst);
assign rst = $initstate;
endmodule
"
.intern(),
});
m.verilog_name("__fayalite_formal_reset");
}
static MOD: OnceLock<Interned<Module<formal_reset>>> = OnceLock::new();
#[hdl]
let formal_reset = instance(*MOD.get_or_init(formal_reset));
formal_reset.rst
}
macro_rules! make_any_const_fn {
($ident:ident, $verilog_attribute:literal) => {
#[hdl]
pub fn $ident<T: BoolOrIntType>(ty: T) -> Expr<T> {
#[hdl_module(extern)]
pub(super) fn $ident<T: BoolOrIntType>(ty: T) {
#[hdl]
let out: T = m.output(ty);
let width = ty.width();
let verilog_bitslice = if width == 1 {
String::new()
} else {
format!(" [{}:0]", width - 1)
};
m.annotate_module(BlackBoxInlineAnnotation {
path: Intern::intern_owned(format!(
"fayalite_{}_{width}.v",
stringify!($ident),
)),
text: Intern::intern_owned(format!(
r"module __fayalite_{}_{width}(output{verilog_bitslice} out);
(* {} *)
reg{verilog_bitslice} out;
endmodule
",
stringify!($ident),
$verilog_attribute,
)),
});
m.verilog_name(format!("__fayalite_{}_{width}", stringify!($ident)));
}
#[derive(Copy, Clone, PartialEq, Eq, Hash)]
struct TheMemoize<T>(T);
impl<T: BoolOrIntType> Memoize for TheMemoize<T> {
type Input = ();
type InputOwned = ();
type Output = Option<Interned<Module<$ident<T>>>>;
fn inner(self, _input: &Self::Input) -> Self::Output {
if self.0.width() == 0 {
None
} else {
Some($ident(self.0))
}
}
}
let Some(module) = TheMemoize(ty).get_owned(()) else {
return 0_hdl_u0.cast_bits_to(ty);
};
#[hdl]
let $ident = instance(module);
$ident.out
}
};
}
make_any_const_fn!(any_const, "anyconst");
make_any_const_fn!(any_seq, "anyseq");
make_any_const_fn!(all_const, "allconst");
make_any_const_fn!(all_seq, "allseq");