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. --- techlibs/common/simlib.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'techlibs/common') 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 @@ -1696,6 +1696,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); -- cgit v1.2.3