aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/arch/intel_alm/add_sub.ys8
-rw-r--r--tests/arch/intel_alm/adffs.ys48
-rw-r--r--tests/arch/intel_alm/counter.ys13
-rw-r--r--tests/arch/intel_alm/dffs.ys22
-rw-r--r--tests/arch/intel_alm/fsm.ys18
-rw-r--r--tests/arch/intel_alm/logic.ys11
-rw-r--r--tests/arch/intel_alm/mux.ys45
-rwxr-xr-xtests/arch/intel_alm/run-test.sh20
-rw-r--r--tests/arch/intel_alm/shifter.ys10
-rw-r--r--tests/arch/intel_alm/tribuf.ys13
-rw-r--r--tests/opt/opt_expr_alu.ys74
-rw-r--r--tests/techmap/zinit.ys98
-rw-r--r--tests/various/bug1876.ys60
-rw-r--r--tests/various/global_scope.ys18
14 files changed, 448 insertions, 10 deletions
diff --git a/tests/arch/intel_alm/add_sub.ys b/tests/arch/intel_alm/add_sub.ys
new file mode 100644
index 000000000..4cb2c2e0d
--- /dev/null
+++ b/tests/arch/intel_alm/add_sub.ys
@@ -0,0 +1,8 @@
+read_verilog ../common/add_sub.v
+hierarchy -top top
+equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+stat
+select -assert-count 8 t:MISTRAL_ALUT_ARITH
+select -assert-none t:MISTRAL_ALUT_ARITH %% t:* %D
diff --git a/tests/arch/intel_alm/adffs.ys b/tests/arch/intel_alm/adffs.ys
new file mode 100644
index 000000000..5d8d3a220
--- /dev/null
+++ b/tests/arch/intel_alm/adffs.ys
@@ -0,0 +1,48 @@
+read_verilog ../common/adffs.v
+design -save read
+
+hierarchy -top adff
+proc
+equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd adff # Constrain all select calls below inside the top module
+select -assert-count 1 t:MISTRAL_FF
+select -assert-count 1 t:MISTRAL_NOT
+
+select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D
+
+
+design -load read
+hierarchy -top adffn
+proc
+equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd adffn # Constrain all select calls below inside the top module
+select -assert-count 1 t:MISTRAL_FF
+
+select -assert-none t:MISTRAL_FF %% t:* %D
+
+
+design -load read
+hierarchy -top dffs
+proc
+equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd dffs # Constrain all select calls below inside the top module
+select -assert-count 1 t:MISTRAL_FF
+select -assert-count 1 t:MISTRAL_ALUT2
+
+select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 %% t:* %D
+
+
+design -load read
+hierarchy -top ndffnr
+proc
+equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd ndffnr # Constrain all select calls below inside the top module
+select -assert-count 1 t:MISTRAL_FF
+select -assert-count 1 t:MISTRAL_NOT
+select -assert-count 1 t:MISTRAL_ALUT2
+
+select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 %% t:* %D
diff --git a/tests/arch/intel_alm/counter.ys b/tests/arch/intel_alm/counter.ys
new file mode 100644
index 000000000..945c318d8
--- /dev/null
+++ b/tests/arch/intel_alm/counter.ys
@@ -0,0 +1,13 @@
+read_verilog ../common/counter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+
+select -assert-count 2 t:MISTRAL_NOT
+select -assert-count 8 t:MISTRAL_ALUT_ARITH
+select -assert-count 8 t:MISTRAL_FF
+
+select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT_ARITH t:MISTRAL_FF %% t:* %D
diff --git a/tests/arch/intel_alm/dffs.ys b/tests/arch/intel_alm/dffs.ys
new file mode 100644
index 000000000..cf29ad8e0
--- /dev/null
+++ b/tests/arch/intel_alm/dffs.ys
@@ -0,0 +1,22 @@
+read_verilog ../common/dffs.v
+design -save read
+
+hierarchy -top dff
+proc
+equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd dff # Constrain all select calls below inside the top module
+select -assert-count 1 t:MISTRAL_FF
+
+select -assert-none t:MISTRAL_FF %% t:* %D
+
+design -load read
+hierarchy -top dffe
+proc
+equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd dffe # Constrain all select calls below inside the top module
+select -assert-count 1 t:MISTRAL_FF
+select -assert-count 1 t:MISTRAL_ALUT3
+
+select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT3 %% t:* %D
diff --git a/tests/arch/intel_alm/fsm.ys b/tests/arch/intel_alm/fsm.ys
new file mode 100644
index 000000000..8bb0ebab2
--- /dev/null
+++ b/tests/arch/intel_alm/fsm.ys
@@ -0,0 +1,18 @@
+read_verilog ../common/fsm.v
+hierarchy -top fsm
+proc
+flatten
+
+equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev
+async2sync
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd fsm # Constrain all select calls below inside the top module
+
+select -assert-count 6 t:MISTRAL_FF
+select -assert-max 2 t:MISTRAL_ALUT2 # Clang returns 2, GCC returns 1
+select -assert-count 5 t:MISTRAL_ALUT5
+select -assert-count 1 t:MISTRAL_ALUT6
+select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D
diff --git a/tests/arch/intel_alm/logic.ys b/tests/arch/intel_alm/logic.ys
new file mode 100644
index 000000000..fad45db74
--- /dev/null
+++ b/tests/arch/intel_alm/logic.ys
@@ -0,0 +1,11 @@
+read_verilog ../common/logic.v
+hierarchy -top top
+proc
+equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+
+select -assert-count 1 t:MISTRAL_NOT
+select -assert-count 6 t:MISTRAL_ALUT2
+select -assert-count 2 t:MISTRAL_ALUT4
+select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT4 %% t:* %D
diff --git a/tests/arch/intel_alm/mux.ys b/tests/arch/intel_alm/mux.ys
new file mode 100644
index 000000000..308e45268
--- /dev/null
+++ b/tests/arch/intel_alm/mux.ys
@@ -0,0 +1,45 @@
+read_verilog ../common/mux.v
+design -save read
+
+hierarchy -top mux2
+proc
+equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux2 # Constrain all select calls below inside the top module
+select -assert-count 1 t:MISTRAL_ALUT3
+
+select -assert-none t:MISTRAL_ALUT3 %% t:* %D
+
+design -load read
+hierarchy -top mux4
+proc
+equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux4 # Constrain all select calls below inside the top module
+select -assert-count 1 t:MISTRAL_ALUT6
+
+select -assert-none t:MISTRAL_ALUT6 %% t:* %D
+
+design -load read
+hierarchy -top mux8
+proc
+equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux8 # Constrain all select calls below inside the top module
+select -assert-count 1 t:MISTRAL_ALUT3
+select -assert-count 1 t:MISTRAL_ALUT5
+select -assert-count 2 t:MISTRAL_ALUT6
+
+select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D
+
+design -load read
+hierarchy -top mux16
+proc
+equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux16 # Constrain all select calls below inside the top module
+select -assert-count 1 t:MISTRAL_ALUT3
+select -assert-count 2 t:MISTRAL_ALUT5
+select -assert-count 4 t:MISTRAL_ALUT6
+
+select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D
diff --git a/tests/arch/intel_alm/run-test.sh b/tests/arch/intel_alm/run-test.sh
new file mode 100755
index 000000000..bf19b887d
--- /dev/null
+++ b/tests/arch/intel_alm/run-test.sh
@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+set -e
+{
+echo "all::"
+for x in *.ys; do
+ echo "all:: run-$x"
+ echo "run-$x:"
+ echo " @echo 'Running $x..'"
+ echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x"
+done
+for s in *.sh; do
+ if [ "$s" != "run-test.sh" ]; then
+ echo "all:: run-$s"
+ echo "run-$s:"
+ echo " @echo 'Running $s..'"
+ echo " @bash $s"
+ fi
+done
+} > run-test.mk
+exec ${MAKE:-make} -f run-test.mk
diff --git a/tests/arch/intel_alm/shifter.ys b/tests/arch/intel_alm/shifter.ys
new file mode 100644
index 000000000..014dbd1a8
--- /dev/null
+++ b/tests/arch/intel_alm/shifter.ys
@@ -0,0 +1,10 @@
+read_verilog ../common/shifter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+select -assert-count 8 t:MISTRAL_FF
+
+select -assert-none t:MISTRAL_FF %% t:* %D
diff --git a/tests/arch/intel_alm/tribuf.ys b/tests/arch/intel_alm/tribuf.ys
new file mode 100644
index 000000000..71b05a747
--- /dev/null
+++ b/tests/arch/intel_alm/tribuf.ys
@@ -0,0 +1,13 @@
+read_verilog ../common/tribuf.v
+hierarchy -top tristate
+proc
+tribuf
+flatten
+synth
+equiv_opt -assert -map +/simcells.v synth_intel_alm -family cyclonev # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd tristate # Constrain all select calls below inside the top module
+#Internal cell type used. Need support it.
+select -assert-count 1 t:$_TBUF_
+
+select -assert-none t:$_TBUF_ %% t:* %D
diff --git a/tests/opt/opt_expr_alu.ys b/tests/opt/opt_expr_alu.ys
index e288bcea6..9121c0096 100644
--- a/tests/opt/opt_expr_alu.ys
+++ b/tests/opt/opt_expr_alu.ys
@@ -8,7 +8,7 @@ alumacc
equiv_opt -assert opt_expr -fine
design -load postopt
select -assert-count 1 t:$pos
-select -assert-count none t:$pos t:* %D
+select -assert-none t:$pos t:* %D
design -reset
@@ -20,7 +20,7 @@ EOT
alumacc
select -assert-count 1 t:$alu
-select -assert-count none t:$alu t:* %D
+select -assert-none t:$alu t:* %D
design -reset
@@ -33,7 +33,7 @@ EOT
equiv_opt -assert opt_expr -fine
design -load postopt
select -assert-count 1 t:$pos
-select -assert-count none t:$pos t:* %D
+select -assert-none t:$pos t:* %D
design -reset
@@ -46,7 +46,7 @@ EOT
equiv_opt -assert opt_expr -fine
design -load postopt
select -assert-count 1 t:$pos
-select -assert-count none t:$pos t:* %D
+select -assert-none t:$pos t:* %D
design -reset
@@ -60,7 +60,8 @@ alumacc
equiv_opt -assert opt_expr -fine
design -load postopt
select -assert-count 1 t:$pos
-select -assert-count none t:$pos t:* %D
+select -assert-count 1 t:$not
+select -assert-none t:$pos t:$not %% t:* %D
design -reset
@@ -76,7 +77,7 @@ design -load postopt
select -assert-count 1 t:$alu
select -assert-count 1 t:$alu r:Y_WIDTH=3 %i
select -assert-count 1 t:$not
-select -assert-count none t:$alu t:$not t:* %D %D
+select -assert-none t:$alu t:$not t:* %D %D
design -reset
@@ -93,7 +94,7 @@ dump
select -assert-count 2 t:$alu
select -assert-count 1 t:$alu r:Y_WIDTH=2 %i
select -assert-count 1 t:$alu r:Y_WIDTH=3 %i
-select -assert-count none t:$alu t:* %D
+select -assert-none t:$alu t:* %D
design -reset
@@ -108,4 +109,61 @@ equiv_opt -assert opt -fine
design -load postopt
select -assert-count 2 t:$alu
select -assert-count 2 t:$alu r:Y_WIDTH=3 %i
-select -assert-count none t:$alu t:* %D
+select -assert-none t:$alu t:* %D
+
+
+design -reset
+read_verilog -icells <<EOT
+module test(input [3:0] a, output [3:0] y, output [3:0] x, output [3:0] co);
+$alu #(
+ .A_WIDTH(4), .B_WIDTH(4), .Y_WIDTH(4),
+ .A_SIGNED(0), .B_SIGNED(0),
+) alu (
+ .A(a), .B(4'h0),
+ .BI(1'b0), .CI(1'b0),
+ .Y(y), .X(x), .CO(co),
+);
+endmodule
+EOT
+
+equiv_opt -assert opt
+design -load postopt
+select -assert-none t:$alu
+
+
+design -reset
+read_verilog -icells <<EOT
+module test(input [3:0] a, output [3:0] y, output [3:0] x, output [3:0] co);
+$alu #(
+ .A_WIDTH(4), .B_WIDTH(4), .Y_WIDTH(4),
+ .A_SIGNED(0), .B_SIGNED(0),
+) alu (
+ .A(a), .B(4'h0),
+ .BI(1'b1), .CI(1'b1),
+ .Y(y), .X(x), .CO(co),
+);
+endmodule
+EOT
+
+equiv_opt -assert opt
+design -load postopt
+select -assert-none t:$alu
+
+
+design -reset
+read_verilog -icells <<EOT
+module test(input [3:0] a, output [3:0] y, output [3:0] x, output [3:0] co);
+$alu #(
+ .A_WIDTH(4), .B_WIDTH(4), .Y_WIDTH(4),
+ .A_SIGNED(0), .B_SIGNED(0),
+) alu (
+ .A(4'h0), .B(a),
+ .BI(1'b0), .CI(1'b0),
+ .Y(y), .X(x), .CO(co),
+);
+endmodule
+EOT
+
+equiv_opt -assert opt
+design -load postopt
+select -assert-none t:$alu
diff --git a/tests/techmap/zinit.ys b/tests/techmap/zinit.ys
index 18b17621f..d0e41b4d2 100644
--- a/tests/techmap/zinit.ys
+++ b/tests/techmap/zinit.ys
@@ -17,7 +17,7 @@ $adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) d
$adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11]));
endmodule
EOT
-equiv_opt -assert -map +/simcells.v -multiclock zinit
+equiv_opt -assert -multiclock zinit
design -load postopt
select -assert-count 20 t:$_NOT_
@@ -47,7 +47,7 @@ $adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) d
$adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11]));
endmodule
EOT
-equiv_opt -assert -map +/simcells.v -multiclock zinit
+equiv_opt -assert -multiclock zinit
design -load postopt
select -assert-count 0 t:$_NOT_
@@ -55,3 +55,97 @@ select -assert-count 1 w:unused a:init %i
select -assert-count 1 w:Q a:init=13'bxxxx1xxxxxxxx %i
select -assert-count 4 c:dff0 c:dff2 c:dff4 c:dff6 %% t:$_DFF_??0_ %i
select -assert-count 4 c:dff1 c:dff3 c:dff5 c:dff7 %% t:$_DFF_??1_ %i
+
+
+design -reset
+read_verilog -icells <<EOT
+module top(input C, R, D, E, (* init = {24{1'b1}} *) output [23:0] Q);
+
+$__DFFE_NN0 dff0 (.C(C), .D(D), .E(E), .R(R), .Q(Q[0]));
+$__DFFE_NN1 dff1 (.C(C), .D(D), .E(E), .R(R), .Q(Q[1]));
+$__DFFE_NP0 dff2 (.C(C), .D(D), .E(E), .R(R), .Q(Q[2]));
+$__DFFE_NP1 dff3 (.C(C), .D(D), .E(E), .R(R), .Q(Q[3]));
+$__DFFE_PN0 dff4 (.C(C), .D(D), .E(E), .R(R), .Q(Q[4]));
+$__DFFE_PN1 dff5 (.C(C), .D(D), .E(E), .R(R), .Q(Q[5]));
+$__DFFE_PP0 dff6 (.C(C), .D(D), .E(E), .R(R), .Q(Q[6]));
+$__DFFE_PP1 dff7 (.C(C), .D(D), .E(E), .R(R), .Q(Q[7]));
+
+$__DFFS_NN0_ dff8 (.C(C), .D(D[0]), .R(R), .Q(Q[8]));
+$__DFFS_NN1_ dff9 (.C(C), .D(D[0]), .R(R), .Q(Q[9]));
+$__DFFS_NP0_ dff10(.C(C), .D(D[0]), .R(R), .Q(Q[10]));
+$__DFFS_NP1_ dff11(.C(C), .D(D[0]), .R(R), .Q(Q[11]));
+$__DFFS_PN0_ dff12(.C(C), .D(D[0]), .R(R), .Q(Q[12]));
+$__DFFS_PN1_ dff13(.C(C), .D(D[0]), .R(R), .Q(Q[13]));
+$__DFFS_PP0_ dff14(.C(C), .D(D[0]), .R(R), .Q(Q[14]));
+$__DFFS_PP1_ dff15(.C(C), .D(D[0]), .R(R), .Q(Q[15]));
+
+$__DFFSE_NN0 dff16(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[16]));
+$__DFFSE_NN1 dff17(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[17]));
+$__DFFSE_NP0 dff18(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[18]));
+$__DFFSE_NP1 dff19(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[19]));
+$__DFFSE_PN0 dff20(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[20]));
+$__DFFSE_PN1 dff21(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[21]));
+$__DFFSE_PP0 dff22(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[22]));
+$__DFFSE_PP1 dff23(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[23]));
+
+endmodule
+EOT
+#equiv_opt -assert -multiclock zinit
+#design -load postopt
+zinit
+
+select -assert-count 48 t:$_NOT_
+select -assert-count 1 w:Q a:init=24'bx %i
+select -assert-count 4 c:dff0 c:dff2 c:dff4 c:dff6 %% t:$__DFFE_??1 %i
+select -assert-count 4 c:dff1 c:dff3 c:dff5 c:dff7 %% t:$__DFFE_??0 %i
+select -assert-count 4 c:dff8 c:dff10 c:dff12 c:dff14 %% t:$__DFFS_??1_ %i
+select -assert-count 4 c:dff9 c:dff11 c:dff13 c:dff15 %% t:$__DFFS_??0_ %i
+select -assert-count 4 c:dff16 c:dff18 c:dff20 c:dff22 %% t:$__DFFSE_??1 %i
+select -assert-count 4 c:dff17 c:dff19 c:dff21 c:dff23 %% t:$__DFFSE_??0 %i
+
+
+design -reset
+read_verilog -icells <<EOT
+module top(input C, R, D, E, (* init = {24{1'b0}} *) output [23:0] Q);
+
+$__DFFE_NN0 dff0 (.C(C), .D(D), .E(E), .R(R), .Q(Q[0]));
+$__DFFE_NN1 dff1 (.C(C), .D(D), .E(E), .R(R), .Q(Q[1]));
+$__DFFE_NP0 dff2 (.C(C), .D(D), .E(E), .R(R), .Q(Q[2]));
+$__DFFE_NP1 dff3 (.C(C), .D(D), .E(E), .R(R), .Q(Q[3]));
+$__DFFE_PN0 dff4 (.C(C), .D(D), .E(E), .R(R), .Q(Q[4]));
+$__DFFE_PN1 dff5 (.C(C), .D(D), .E(E), .R(R), .Q(Q[5]));
+$__DFFE_PP0 dff6 (.C(C), .D(D), .E(E), .R(R), .Q(Q[6]));
+$__DFFE_PP1 dff7 (.C(C), .D(D), .E(E), .R(R), .Q(Q[7]));
+
+$__DFFS_NN0_ dff8 (.C(C), .D(D[0]), .R(R), .Q(Q[8]));
+$__DFFS_NN1_ dff9 (.C(C), .D(D[0]), .R(R), .Q(Q[9]));
+$__DFFS_NP0_ dff10(.C(C), .D(D[0]), .R(R), .Q(Q[10]));
+$__DFFS_NP1_ dff11(.C(C), .D(D[0]), .R(R), .Q(Q[11]));
+$__DFFS_PN0_ dff12(.C(C), .D(D[0]), .R(R), .Q(Q[12]));
+$__DFFS_PN1_ dff13(.C(C), .D(D[0]), .R(R), .Q(Q[13]));
+$__DFFS_PP0_ dff14(.C(C), .D(D[0]), .R(R), .Q(Q[14]));
+$__DFFS_PP1_ dff15(.C(C), .D(D[0]), .R(R), .Q(Q[15]));
+
+$__DFFSE_NN0 dff16(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[16]));
+$__DFFSE_NN1 dff17(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[17]));
+$__DFFSE_NP0 dff18(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[18]));
+$__DFFSE_NP1 dff19(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[19]));
+$__DFFSE_PN0 dff20(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[20]));
+$__DFFSE_PN1 dff21(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[21]));
+$__DFFSE_PP0 dff22(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[22]));
+$__DFFSE_PP1 dff23(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[23]));
+
+endmodule
+EOT
+#equiv_opt -assert -multiclock zinit
+#design -load postopt
+zinit
+
+select -assert-count 0 t:$_NOT_
+select -assert-count 1 w:Q a:init=24'bx %i
+select -assert-count 4 c:dff0 c:dff2 c:dff4 c:dff6 %% t:$__DFFE_??0 %i
+select -assert-count 4 c:dff1 c:dff3 c:dff5 c:dff7 %% t:$__DFFE_??1 %i
+select -assert-count 4 c:dff8 c:dff10 c:dff12 c:dff14 %% t:$__DFFS_??0_ %i
+select -assert-count 4 c:dff9 c:dff11 c:dff13 c:dff15 %% t:$__DFFS_??1_ %i
+select -assert-count 4 c:dff16 c:dff18 c:dff20 c:dff22 %% t:$__DFFSE_??0 %i
+select -assert-count 4 c:dff17 c:dff19 c:dff21 c:dff23 %% t:$__DFFSE_??1 %i
diff --git a/tests/various/bug1876.ys b/tests/various/bug1876.ys
new file mode 100644
index 000000000..7995eedcf
--- /dev/null
+++ b/tests/various/bug1876.ys
@@ -0,0 +1,60 @@
+read_verilog <<EOT
+module expression_00032(b5, y15);
+ input signed [5:0] b5;
+ output [3:0] y15;
+ assign y15 = (0 ? b5 : b5) > 0;
+endmodule
+EOT
+
+
+design -reset
+read_verilog <<EOT
+module expression_00057(a0, a1, a2, a3, a4, a5, b0, b1, b2, b3, b4, b5, y8);
+ input [3:0] a0;
+ input [4:0] a1;
+ input [5:0] a2;
+ input signed [3:0] a3;
+ input signed [4:0] a4;
+ input signed [5:0] a5;
+
+ input [3:0] b0;
+ input [4:0] b1;
+ input [5:0] b2;
+ input signed [3:0] b3;
+ input signed [4:0] b4;
+ input signed [5:0] b5;
+
+ output [5:0] y8;
+
+ localparam signed [4:0] p4 = ((2'd3)||(-4'sd1));
+ localparam signed [3:0] p9 = {3{(((2'sd0)^~(5'd20))>((-3'sd0)>>(4'sd2)))}};
+
+ assign y8 = (-(!($signed({3{p9}})<(p4?b4:b5))));
+endmodule
+EOT
+
+
+design -reset
+read_verilog <<EOT
+module expression_00354(a0, a1, a2, a3, a4, a5, b0, b1, b2, b3, b4, b5, y4);
+ input [3:0] a0;
+ input [4:0] a1;
+ input [5:0] a2;
+ input signed [3:0] a3;
+ input signed [4:0] a4;
+ input signed [5:0] a5;
+
+ input [3:0] b0;
+ input [4:0] b1;
+ input [5:0] b2;
+ input signed [3:0] b3;
+ input signed [4:0] b4;
+ input signed [5:0] b5;
+
+ output wire signed [4:0] y4;
+
+ localparam signed [4:0] p10 = ((3'd0)?(2'd1):(-2'sd1));
+
+ assign y4 = ((p10?a4:b4)&$signed(b3));
+endmodule
+EOT
diff --git a/tests/various/global_scope.ys b/tests/various/global_scope.ys
new file mode 100644
index 000000000..8c8618e10
--- /dev/null
+++ b/tests/various/global_scope.ys
@@ -0,0 +1,18 @@
+read_verilog -sv <<EOT
+parameter A = 10;
+parameter B = A;
+
+typedef enum {
+ CONST_A = A,
+ CONST_B = A+1
+} enum_t;
+
+module top(output [3:0] q, output [3:0] r);
+assign q = 10;
+assign r = CONST_B;
+endmodule
+EOT
+
+hierarchy -top top
+sat -verify -prove q 10 top
+sat -verify -prove r 11 top