From c0063288d699f4f3edf5e0ff6ee1bd5cfa9ac884 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 21 Jul 2022 14:22:15 +0200 Subject: Add the $anyinit cell and the formalff pass These can be used to protect undefined flip-flop initialization values from optimizations that are not sound for formal verification and can help mapping all solver-provided values in witness traces for flows that use different backends simultaneously. --- kernel/ff.h | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'kernel/ff.h') diff --git a/kernel/ff.h b/kernel/ff.h index 41721b4a1..e684d3c43 100644 --- a/kernel/ff.h +++ b/kernel/ff.h @@ -28,7 +28,10 @@ YOSYS_NAMESPACE_BEGIN // Describes a flip-flop or a latch. // // If has_gclk, this is a formal verification FF with implicit global clock: -// Q is simply previous cycle's D. +// Q is simply previous cycle's D. Additionally if is_anyinit is true, this is +// an $anyinit cell which always has an undefined initialization value. Note +// that $anyinit is not considered to be among the FF celltypes, so a pass has +// to explicitly opt-in to process $anyinit cells with FfData. // // Otherwise, the FF/latch can have any number of features selected by has_* // attributes that determine Q's value (in order of decreasing priority): @@ -126,6 +129,8 @@ struct FfData { // True if this FF is a fine cell, false if it is a coarse cell. // If true, width must be 1. bool is_fine; + // True if this FF is an $anyinit cell. Depends on has_gclk. + bool is_anyinit; // Polarities, corresponding to sig_*. True means active-high, false // means active-low. bool pol_clk; @@ -156,6 +161,7 @@ struct FfData { has_sr = false; ce_over_srst = false; is_fine = false; + is_anyinit = false; pol_clk = false; pol_aload = false; pol_ce = false; -- cgit v1.2.3