Merge branch 'master' of https://github.com/ALGCDG/yosys

3 files changed, 46 insertions, 0 deletions

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
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
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