From a48dcd1d40a845cfb8b18cbe986faf0b780880be Mon Sep 17 00:00:00 2001
From: Lofty <dan.ravensloft@gmail.com>
Date: Mon, 11 Apr 2022 13:21:47 +0100
Subject: rename: add -scramble-name option to randomly rename selections

---
 tests/various/rename_scramble_name.ys | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 tests/various/rename_scramble_name.ys

(limited to 'tests/various')

diff --git a/tests/various/rename_scramble_name.ys b/tests/various/rename_scramble_name.ys
new file mode 100644
index 000000000..9a36d0922
--- /dev/null
+++ b/tests/various/rename_scramble_name.ys
@@ -0,0 +1,31 @@
+read_verilog <<EOF
+module top();
+    wire a, b, c;
+endmodule
+EOF
+
+proc
+hierarchy -top top
+rename -seed 2 -scramble-name w:*
+select -assert-none w:a w:b w:c
+select -assert-count 3 w:$_*_
+select -assert-none w:$_*_ %% %n
+design -reset
+
+read_verilog <<EOF
+module foo(input a, b, output c);
+    assign c = a + b;
+endmodule
+
+module top();
+    wire a, b, c;
+    foo bar(.a(a), .b(b), .c(c));
+endmodule
+EOF
+
+proc
+hierarchy -top top
+rename -seed 2 -scramble-name c:bar
+select -assert-none c:bar
+select -assert-count 1 c:$_*_
+select -assert-none c:$_*_ w:* foo/c:$add$<<EOF:2$1 %% %n
-- 
cgit v1.2.3


From f041e36c6e142878c5bca4da5b459177c4f75e07 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
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.
---
 tests/various/smtlib2_module-expected.smt2 | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'tests/various')

diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2
index ace858ca8..74e2f3fca 100644
--- a/tests/various/smtlib2_module-expected.smt2
+++ b/tests/various/smtlib2_module-expected.smt2
@@ -4,11 +4,14 @@
 (declare-fun |smtlib2_is| (|smtlib2_s|) Bool)
 (declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
 ; yosys-smt2-input a 8
+; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "type": "input", "width": 8}
 (define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
 (declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
 ; yosys-smt2-input b 8
+; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "type": "input", "width": 8}
 (define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
 ; yosys-smt2-output add 8
+; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "type": "blackbox", "width": 8}
 (define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
 (|a| (|smtlib2_n a| state))
 (|b| (|smtlib2_n b| state))
@@ -16,6 +19,7 @@
 (bvadd a b)
 ))
 ; yosys-smt2-output eq 1
+; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "type": "blackbox", "width": 1}
 (define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
 (|a| (|smtlib2_n a| state))
 (|b| (|smtlib2_n b| state))
@@ -23,6 +27,7 @@
 (= a b)
 ))
 ; yosys-smt2-output sub 8
+; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "type": "blackbox", "width": 8}
 (define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let (
 (|a| (|smtlib2_n a| state))
 (|b| (|smtlib2_n b| state))
@@ -38,13 +43,16 @@
 (declare-sort |uut_s| 0)
 (declare-fun |uut_is| (|uut_s|) Bool)
 ; yosys-smt2-cell smtlib2 s
+; yosys-smt2-witness {"path": ["\\s"], "smtname": "s", "type": "cell"}
 (declare-fun |uut#0| (|uut_s|) (_ BitVec 8)) ; \add
 (declare-fun |uut#1| (|uut_s|) Bool) ; \eq
 (declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub
 (declare-fun |uut_h s| (|uut_s|) |smtlib2_s|)
 ; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26
+; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "type": "init", "width": 8}
 (declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a
 ; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41
+; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "type": "init", "width": 8}
 (declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b
 (define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2
 (define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9
-- 
cgit v1.2.3


From 5142fb3b5c6e7ed89fe74fcdff7775d6f09c34f5 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Thu, 18 Aug 2022 13:56:22 +0200
Subject: write_aiger: Fix non-$_FF_ FFs

This broke while switching sby's formal flows to always use $_FF_'s.
---
 tests/various/aiger_dff.ys | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 tests/various/aiger_dff.ys

(limited to 'tests/various')

diff --git a/tests/various/aiger_dff.ys b/tests/various/aiger_dff.ys
new file mode 100644
index 000000000..057f3d774
--- /dev/null
+++ b/tests/various/aiger_dff.ys
@@ -0,0 +1,7 @@
+read_verilog -icells <<EOT
+module top(input clk, d, output q);
+\$_DFF_N_ dffn(.C(clk), .D(d), .Q(q));
+endmodule
+EOT
+write_aiger -zinit -ywmap aiger_dff.out /dev/null
+!grep -qF negedge aiger_dff.out
-- 
cgit v1.2.3