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.

1 files changed, 17 insertions, 0 deletions

diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index b14488ff4..ab9bd7e1d 100644
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -1697,6 +1697,23 @@ assign Y = 'bx;
 endmodule
 
 // --------------------------------------------------------
+`ifdef SIMLIB_FF
+module \$anyinit (D, Q);
+
+parameter WIDTH = 0;
+
+input [WIDTH-1:0] D;
+output reg [WIDTH-1:0] Q;
+
+initial Q <= 'bx;
+
+always @($global_clk) begin
+	Q <= D;
+end
+
+endmodule
+`endif
+// --------------------------------------------------------
 
 module \$allconst (Y);