From 0cf01600b3b3883929ffb1edae914fa216c9c434 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Tue, 1 Oct 2024 19:56:17 -0700 Subject: [PATCH] add mod formal and move assert/assume/cover stuff to it --- crates/fayalite/src/firrtl.rs | 11 +- crates/fayalite/src/formal.rs | 186 ++++++++++++++++++ crates/fayalite/src/lib.rs | 1 + crates/fayalite/src/module.rs | 146 ++------------ crates/fayalite/src/module/transform/visit.rs | 5 +- crates/fayalite/src/prelude.rs | 9 +- crates/fayalite/visit_types.json | 2 +- 7 files changed, 218 insertions(+), 142 deletions(-) create mode 100644 crates/fayalite/src/formal.rs diff --git a/crates/fayalite/src/firrtl.rs b/crates/fayalite/src/firrtl.rs index 5a2cc00..ef955ea 100644 --- a/crates/fayalite/src/firrtl.rs +++ b/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, - StmtReg, StmtWire, + StmtConnect, StmtDeclaration, StmtFormal, StmtIf, StmtInstance, StmtMatch, StmtReg, + 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", - StmtFormalKind::Assume => "assume", - StmtFormalKind::Cover => "cover", + FormalKind::Assert => "assert", + FormalKind::Assume => "assume", + FormalKind::Cover => "cover", }; let text = EscapedString { value: &text, diff --git a/crates/fayalite/src/formal.rs b/crates/fayalite/src/formal.rs new file mode 100644 index 0000000..5e90b59 --- /dev/null +++ b/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, + pred: Expr, + en: Expr, + 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, + pred: Expr, + en: Expr, + 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, + pred: Expr, + 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, pred: Expr, 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, + pred: Expr, + en: Expr, + 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, + pred: Expr, + en: Expr, + text: &str, + ) { + formal_stmt_with_enable(FormalKind::$kind, clk, pred, en, text); + } + #[track_caller] + pub fn $formal_stmt_with_loc( + clk: Expr, + pred: Expr, + text: &str, + source_location: SourceLocation, + ) { + formal_stmt_with_loc(FormalKind::$kind, clk, pred, text, source_location); + } + #[track_caller] + pub fn $formal_stmt(clk: Expr, pred: Expr, 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 MakeFormalExpr for T {} + +#[hdl] +pub fn formal_global_clock() -> Expr { + #[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 { + #[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 +} diff --git a/crates/fayalite/src/lib.rs b/crates/fayalite/src/lib.rs index 6e1ccd3..eedb1bb 100644 --- a/crates/fayalite/src/lib.rs +++ b/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; diff --git a/crates/fayalite/src/module.rs b/crates/fayalite/src/module.rs index f93758a..872c75f 100644 --- a/crates/fayalite/src/module.rs +++ b/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, pub pred: Expr, pub en: Expr, @@ -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 { pub cond: Expr, @@ -2439,119 +2436,6 @@ pub fn match_with_loc( T::match_variants(expr.to_expr(), source_location) } -#[track_caller] -pub fn formal_with_enable_and_loc( - kind: StmtFormalKind, - clk: Expr, - pred: Expr, - en: Expr, - 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, - pred: Expr, - en: Expr, - 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, - pred: Expr, - 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, pred: Expr, 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, - pred: Expr, - en: Expr, - 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, pred: Expr, en: Expr, text: &str) { - formal_with_enable(StmtFormalKind::$kind, clk, pred, en, text); - } - #[track_caller] - pub fn $formal_with_loc( - clk: Expr, - pred: Expr, - text: &str, - source_location: SourceLocation, - ) { - formal_with_loc(StmtFormalKind::$kind, clk, pred, text, source_location); - } - #[track_caller] - pub fn $formal(clk: Expr, pred: Expr, 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: Lhs, diff --git a/crates/fayalite/src/module/transform/visit.rs b/crates/fayalite/src/module/transform/visit.rs index 1165a46..2e1e48f 100644 --- a/crates/fayalite/src/module/transform/visit.rs +++ b/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, - StmtFormalKind, StmtIf, StmtInstance, StmtMatch, StmtReg, StmtWire, + NormalModuleBody, ScopedNameId, Stmt, StmtConnect, StmtDeclaration, StmtFormal, StmtIf, + StmtInstance, StmtMatch, StmtReg, StmtWire, }, reg::Reg, reset::{AsyncReset, Reset, SyncReset}, diff --git a/crates/fayalite/src/prelude.rs b/crates/fayalite/src/prelude.rs index c793775..f1a9736 100644 --- a/crates/fayalite/src/prelude.rs +++ b/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, - 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, + annotate, connect, connect_any, incomplete_wire, instance, memory, memory_array, + memory_with_init, reg_builder, wire, Instance, Module, ModuleBuilder, }, reg::Reg, reset::{AsyncReset, Reset, SyncReset, ToAsyncReset, ToReset, ToSyncReset}, diff --git a/crates/fayalite/visit_types.json b/crates/fayalite/visit_types.json index 09ae23f..366ee2f 100644 --- a/crates/fayalite/visit_types.json +++ b/crates/fayalite/visit_types.json @@ -1089,7 +1089,7 @@ "source_location": "Visible" } }, - "StmtFormalKind": { + "FormalKind": { "data": { "$kind": "Enum", "Assert": null,