diff options
Diffstat (limited to 'tests')
-rw-r--r-- | tests/arch/intel_alm/add_sub.ys | 8 | ||||
-rw-r--r-- | tests/arch/intel_alm/adffs.ys | 48 | ||||
-rw-r--r-- | tests/arch/intel_alm/counter.ys | 13 | ||||
-rw-r--r-- | tests/arch/intel_alm/dffs.ys | 22 | ||||
-rw-r--r-- | tests/arch/intel_alm/fsm.ys | 18 | ||||
-rw-r--r-- | tests/arch/intel_alm/logic.ys | 11 | ||||
-rw-r--r-- | tests/arch/intel_alm/mux.ys | 45 | ||||
-rwxr-xr-x | tests/arch/intel_alm/run-test.sh | 20 | ||||
-rw-r--r-- | tests/arch/intel_alm/shifter.ys | 10 | ||||
-rw-r--r-- | tests/arch/intel_alm/tribuf.ys | 13 | ||||
-rw-r--r-- | tests/opt/opt_expr_alu.ys | 56 | ||||
-rw-r--r-- | tests/svtypes/typedef_package.sv | 11 | ||||
-rw-r--r-- | tests/techmap/dffinit.ys | 25 | ||||
-rw-r--r-- | tests/techmap/zinit.ys | 151 | ||||
-rw-r--r-- | tests/various/bug1876.ys | 60 |
15 files changed, 504 insertions, 7 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 a3361ca43..e288bcea6 100644 --- a/tests/opt/opt_expr_alu.ys +++ b/tests/opt/opt_expr_alu.ys @@ -5,7 +5,7 @@ endmodule EOT alumacc -equiv_opt opt_expr -fine +equiv_opt -assert opt_expr -fine design -load postopt select -assert-count 1 t:$pos select -assert-count none t:$pos t:* %D @@ -30,7 +30,7 @@ assign y = {a,1'b1} - 1'b1; endmodule EOT -equiv_opt opt_expr -fine +equiv_opt -assert opt_expr -fine design -load postopt select -assert-count 1 t:$pos select -assert-count none t:$pos t:* %D @@ -43,7 +43,7 @@ assign y = {a,3'b101} - 1'b1; endmodule EOT -equiv_opt opt_expr -fine +equiv_opt -assert opt_expr -fine design -load postopt select -assert-count 1 t:$pos select -assert-count none t:$pos t:* %D @@ -57,7 +57,55 @@ endmodule EOT alumacc -equiv_opt opt_expr -fine +equiv_opt -assert opt_expr -fine design -load postopt select -assert-count 1 t:$pos select -assert-count none t:$pos t:* %D + + +design -reset +read_verilog <<EOT +module test(input [1:0] a, output [3:0] y); +assign y = -{a[1], 2'b10, a[0]}; +endmodule +EOT + +alumacc +equiv_opt -assert opt -fine +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 + + +design -reset +read_verilog <<EOT +module test(input [3:0] a, input [2:0] b, output [5:0] y); +assign y = {a[3:2], 1'b1, a[1:0]} + {b[2], 2'b11, b[1:0]}; +endmodule +EOT + +alumacc +equiv_opt -assert opt -fine +design -load postopt +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 + + +design -reset +read_verilog <<EOT +module test(input [3:0] a, input [3:0] b, output [5:0] y); +assign y = {a[3:2], 1'b0, a[1:0]} + {b[3:2], 1'b0, b[1:0]}; +endmodule +EOT + +alumacc +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 diff --git a/tests/svtypes/typedef_package.sv b/tests/svtypes/typedef_package.sv index 57a78c53a..2d83742c5 100644 --- a/tests/svtypes/typedef_package.sv +++ b/tests/svtypes/typedef_package.sv @@ -1,6 +1,9 @@ package pkg; typedef logic [7:0] uint8_t; - typedef enum logic [7:0] {bb=8'hBB} enum8_t; + typedef enum logic [7:0] {bb=8'hBB, cc=8'hCC} enum8_t; + + localparam uint8_t PCONST = cc; + parameter uint8_t PCONST_COPY = PCONST; endpackage module top; @@ -8,7 +11,9 @@ module top; (* keep *) pkg::uint8_t a = 8'hAA; (* keep *) pkg::enum8_t b_enum = pkg::bb; - always @* assert(a == 8'hAA); - always @* assert(b_enum == 8'hBB); + always_comb assert(a == 8'hAA); + always_comb assert(b_enum == 8'hBB); + always_comb assert(pkg::PCONST == pkg::cc); + always_comb assert(pkg::PCONST_COPY == pkg::cc); endmodule diff --git a/tests/techmap/dffinit.ys b/tests/techmap/dffinit.ys new file mode 100644 index 000000000..218d411f8 --- /dev/null +++ b/tests/techmap/dffinit.ys @@ -0,0 +1,25 @@ +read_verilog <<EOT + +module ff(...); +input d; +output q; + +endmodule + +module top(...); +input d; +output q1; +(* init = 1'b1 *) +output q2; + +ff my_ff1(.d(d), .q(q1)); +ff my_ff2(.d(d), .q(q2)); + +endmodule + +EOT + +dffinit -ff ff q init +select -assert-count 2 t:ff +select -assert-count 1 t:ff r:init %i +select -assert-count 1 t:ff r:init=1'b1 %i diff --git a/tests/techmap/zinit.ys b/tests/techmap/zinit.ys new file mode 100644 index 000000000..d0e41b4d2 --- /dev/null +++ b/tests/techmap/zinit.ys @@ -0,0 +1,151 @@ +read_verilog -icells <<EOT +module top(input C, R, input [1:0] D, (* init = {2'b10, 2'b01, 1'b1, {8{1'b1}}} *) output [12:0] Q); + +(* init = 1'b1 *) +wire unused; + +$_DFF_NN0_ dff0 (.C(C), .D(D[0]), .R(R), .Q(Q[0])); +$_DFF_NN1_ dff1 (.C(C), .D(D[0]), .R(R), .Q(Q[1])); +$_DFF_NP0_ dff2 (.C(C), .D(D[0]), .R(R), .Q(Q[2])); +$_DFF_NP1_ dff3 (.C(C), .D(D[0]), .R(R), .Q(Q[3])); +$_DFF_PN0_ dff4 (.C(C), .D(D[0]), .R(R), .Q(Q[4])); +$_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5])); +$_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6])); +$_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7])); + +$adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9])); +$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 -multiclock zinit +design -load postopt + +select -assert-count 20 t:$_NOT_ +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_??1_ %i +select -assert-count 4 c:dff1 c:dff3 c:dff5 c:dff7 %% t:$_DFF_??0_ %i + + +design -reset +read_verilog -icells <<EOT +module top(input C, R, input [1:0] D, (* init = {2'bx0, 2'b0x, 1'b1, {8{1'b0}}} *) output [12:0] Q); + +(* init = 1'b1 *) +wire unused; + +$_DFF_NN0_ dff0 (.C(C), .D(D[0]), .R(R), .Q(Q[0])); +$_DFF_NN1_ dff1 (.C(C), .D(D[0]), .R(R), .Q(Q[1])); +$_DFF_NP0_ dff2 (.C(C), .D(D[0]), .R(R), .Q(Q[2])); +$_DFF_NP1_ dff3 (.C(C), .D(D[0]), .R(R), .Q(Q[3])); +$_DFF_PN0_ dff4 (.C(C), .D(D[0]), .R(R), .Q(Q[4])); +$_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5])); +$_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6])); +$_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7])); + +$adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9])); +$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 -multiclock zinit +design -load postopt + +select -assert-count 0 t:$_NOT_ +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 |