From 59b96bb1f82b6cf83e004488267e5576dbcfad4b Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 4 Jul 2022 11:09:06 +0200 Subject: Upadte documentation and changelog --- CHANGELOG | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index e32d9d053..16c746957 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -4,6 +4,21 @@ List of major changes and improvements between releases Yosys 0.18 .. Yosys 0.18-dev -------------------------- + * Various + - Added support for $pos cell in btor backend + + * New commands and options + - Added option "-rom-only" to "memory_libmap" pass + - Added option "-smtcheck" to "hierarchy" pass + - Added option "-keepdc" to "memory_libmap" pass + - Added option "-suffix" to "rename" pass + - Added "gatemate_foldinv" pass + + * GateMate support + - Added LUT tree mapping + + * Verific support + - Added option "-pp" to "verific -import" Yosys 0.17 .. Yosys 0.18 -------------------------- -- cgit v1.2.3 From 5343911263ea10dc9d0fd308297314b4b42989d2 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 4 Jul 2022 13:54:49 +0200 Subject: Mention smtlib2_module in README.md and CHANGELOG --- CHANGELOG | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 16c746957..97572c35d 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -4,9 +4,6 @@ List of major changes and improvements between releases Yosys 0.18 .. Yosys 0.18-dev -------------------------- - * Various - - Added support for $pos cell in btor backend - * New commands and options - Added option "-rom-only" to "memory_libmap" pass - Added option "-smtcheck" to "hierarchy" pass @@ -14,6 +11,10 @@ Yosys 0.18 .. Yosys 0.18-dev - Added option "-suffix" to "rename" pass - Added "gatemate_foldinv" pass + * Formal Verification + - Added support for $pos cell in btor backend + - Added the "smtlib2_module" and "smtlib2_comb_expr" attributes + * GateMate support - Added LUT tree mapping -- cgit v1.2.3 From a45c131b37ce503e6de7783939eb38f89d9d64e7 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 4 Jul 2022 14:07:01 +0200 Subject: Release version 0.19 --- CHANGELOG | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 97572c35d..8d1b76c78 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,7 +2,7 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.18 .. Yosys 0.18-dev +Yosys 0.18 .. Yosys 0.19 -------------------------- * New commands and options - Added option "-rom-only" to "memory_libmap" pass -- cgit v1.2.3 From da0682b99a48e41e606f7c0a769aaa8d770cad77 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 4 Jul 2022 14:08:53 +0200 Subject: Next dev cycle --- CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 8d1b76c78..54c385cd8 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,6 +2,9 @@ List of major changes and improvements between releases ======================================================= +Yosys 0.19 .. Yosys 0.19-dev +-------------------------- + Yosys 0.18 .. Yosys 0.19 -------------------------- * New commands and options -- cgit v1.2.3 From 6a1d98b816a15b9f06a3a4621a9ae390c30b7494 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 3 Aug 2022 10:30:58 +0200 Subject: Update manual and changelog --- CHANGELOG | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 54c385cd8..341c9957c 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -4,6 +4,12 @@ List of major changes and improvements between releases Yosys 0.19 .. Yosys 0.19-dev -------------------------- + * New commands and options + - Added option "-wb" to "read_liberty" pass + + * Various + - Added support for $modfloor operator to cxxrtl backend + - Support build on OpenBSD Yosys 0.18 .. Yosys 0.19 -------------------------- -- cgit v1.2.3 From a07b06d5e7b3f5cd9b9c8a1b1a8e7718172c8bbc Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 3 Aug 2022 13:52:01 +0200 Subject: Update Changelog --- CHANGELOG | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 341c9957c..fde400117 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -10,6 +10,13 @@ Yosys 0.19 .. Yosys 0.19-dev * Various - Added support for $modfloor operator to cxxrtl backend - Support build on OpenBSD + - Fixed smt2 backend use of $shift/$shiftx with negative shift amounts, + which affects bit/part-select assignments with a dynamic index. Shift + operators were not affected. + + * Verific support + - Proper import of port ranges into Yosys, may result in reversed + bit-order of top-level ports for some synthesis flows. Yosys 0.18 .. Yosys 0.19 -------------------------- -- cgit v1.2.3 From 4fcb95ed087263d6e55662a18ceac1722100c7d0 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 3 Aug 2022 13:53:41 +0200 Subject: Release version 0.20 --- CHANGELOG | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index fde400117..42f264686 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,7 +2,7 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.19 .. Yosys 0.19-dev +Yosys 0.19 .. Yosys 0.20 -------------------------- * New commands and options - Added option "-wb" to "read_liberty" pass -- cgit v1.2.3 From 733902c81e1be8e8eee880697ce967fb91e00d05 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 3 Aug 2022 13:57:14 +0200 Subject: Next dev cycle --- CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 42f264686..434872248 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,6 +2,9 @@ List of major changes and improvements between releases ======================================================= +Yosys 0.20 .. Yosys 0.20-dev +-------------------------- + Yosys 0.19 .. Yosys 0.20 -------------------------- * New commands and options -- cgit v1.2.3 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. --- 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 From a2f9ebe43a287233917947851e0d0dff803a4675 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 16:07:28 +0200 Subject: memory_map: Add -formal option This maps memories for a global clock based formal verification flow. This implies -keepdc, uses $ff cells for ROMs and sets hdlname attributes. --- CHANGELOG | 1 + 1 file changed, 1 insertion(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 199d6a61a..5ee3e3cc0 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -6,6 +6,7 @@ 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 * Formal Verification - Added $anyinit cell to directly represent FFs with an unconstrained -- cgit v1.2.3 From f041e36c6e142878c5bca4da5b459177c4f75e07 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 16:49:36 +0200 Subject: smtbmc: Add native json based witness format + smt2 backend support This adds a native json based witness trace format. By having a common format that includes everything we support, and providing a conversion utility (yosys-witness) we no longer need to implement every format for every tool that deals with witness traces, avoiding a quadratic opportunity to introduce subtle bugs. Included: * smt2: New yosys-smt2-witness info lines containing full hierarchical paths without lossy escaping. * yosys-smtbmc --dump-yw trace.yw: Dump results in the new format. * yosys-smtbmc --yw trace.yw: Read new format as constraints. * yosys-witness: New tool to convert witness formats. Currently this can only display traces in a human-readable-only format and do a passthrough read/write of the new format. * ywio.py: Small python lib for reading and writing the new format. Used by yosys-smtbmc and yosys-witness to avoid duplication. --- CHANGELOG | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 5ee3e3cc0..cf2a46bd3 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -11,6 +11,10 @@ Yosys 0.20 .. Yosys 0.20-dev * 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. Yosys 0.19 .. Yosys 0.20 -------------------------- -- cgit v1.2.3 From efd5b86eb9c56d293c608d378ee90beea53784b5 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 17:02:39 +0200 Subject: aiger: Add yosys-witness support Adds a new json based aiger map file and yosys-witness converters to us this to convert between native and AIGER witness files. --- CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index cf2a46bd3..a9144facf 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -15,6 +15,9 @@ Yosys 0.20 .. Yosys 0.20-dev - 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 -------------------------- -- cgit v1.2.3 From 65145db7e7bec998a194aa0f6335de50df00e550 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 3 Aug 2022 17:27:06 +0200 Subject: rename: Add -witness mode --- CHANGELOG | 2 ++ 1 file changed, 2 insertions(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index a9144facf..6403c5b9a 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -7,6 +7,8 @@ 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 * Formal Verification - Added $anyinit cell to directly represent FFs with an unconstrained -- cgit v1.2.3 From f7023d06a2bda56467c8f07cc44d3b92f0eab2ba Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 9 Aug 2022 15:43:26 +0200 Subject: sim: -hdlname option to preserve flattened hierarchy in sim output --- CHANGELOG | 2 ++ 1 file changed, 2 insertions(+) (limited to 'CHANGELOG') diff --git a/CHANGELOG b/CHANGELOG index 6403c5b9a..a1f4624ee 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -9,6 +9,8 @@ Yosys 0.20 .. Yosys 0.20-dev - 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 -- cgit v1.2.3