aboutsummaryrefslogtreecommitdiffstats
path: root/CHANGELOG
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGELOG')
-rw-r--r--CHANGELOG18
1 files changed, 18 insertions, 0 deletions
diff --git a/CHANGELOG b/CHANGELOG
index 434872248..a1f4624ee 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -4,6 +4,24 @@ 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
+ - Added option "-formal" to "memory_map" pass
+ - Added option "-witness" to "rename" - give public names to all signals
+ present in yosys witness traces
+ - Added option "-hdlname" to "sim" pass - preserves hiearachy when writing
+ simulation output for a flattened design
+
+ * Formal Verification
+ - Added $anyinit cell to directly represent FFs with an unconstrained
+ initialization value. These can be generated by the new formalff pass.
+ - New JSON based yosys witness format for formal verification traces.
+ - yosys-smtbmc: Reading and writing of yosys witness traces.
+ - write_smt2: Emit inline metadata to support yosys witness trace.
+ - yosys-witness is a new tool to inspect and convert yosys witness traces.
+ - write_aiger: Option to write a map file for yosys witness trace
+ conversion.
+ - yosys-witness: Conversion from and to AIGER witness traces.
Yosys 0.19 .. Yosys 0.20
--------------------------