fayalite/crates/fayalite/src/formal.rs

// SPDX-License-Identifier: LGPL-3.0-or-later
// See Notices.txt for copyright information
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");