From c0063288d699f4f3edf5e0ff6ee1bd5cfa9ac884 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
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.
---
 CHANGELOG | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'CHANGELOG')

diff --git a/CHANGELOG b/CHANGELOG
index 434872248..199d6a61a 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -4,6 +4,12 @@ List of major changes and improvements between releases
 
 Yosys 0.20 .. Yosys 0.20-dev
 --------------------------
+ * New commands and options
+    - Added "formalff" pass - transforms FFs for formal verification
+
+ * Formal Verification
+    - Added $anyinit cell to directly represent FFs with an unconstrained
+      initialization value. These can be generated by the new formalff pass.
 
 Yosys 0.19 .. Yosys 0.20
 --------------------------
-- 
cgit v1.2.3