diff options
author | Jannis Harder <me@jix.one> | 2022-08-16 14:18:35 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-08-16 14:18:35 +0200 |
commit | 556d008ed3c2db351e93e0075ccd47bdfb634fd9 (patch) | |
tree | ab23fa7355df8f8ead24839ee7846e68cdbfb935 /kernel/ff.h | |
parent | c26b2bf543a226e65a3fb07040bb278d668accf2 (diff) | |
parent | f7023d06a2bda56467c8f07cc44d3b92f0eab2ba (diff) | |
download | yosys-556d008ed3c2db351e93e0075ccd47bdfb634fd9.tar.gz yosys-556d008ed3c2db351e93e0075ccd47bdfb634fd9.tar.bz2 yosys-556d008ed3c2db351e93e0075ccd47bdfb634fd9.zip |
Merge pull request #3434 from jix/witness_flow
Updated formal flow with new witness format
Diffstat (limited to 'kernel/ff.h')
-rw-r--r-- | kernel/ff.h | 8 |
1 files changed, 7 insertions, 1 deletions
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; |