diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/arch/fabulous/carry.ys | 9 | ||||
| -rw-r--r-- | tests/various/muxcover.ys | 40 | ||||
| -rw-r--r-- | tests/verific/.gitignore | 3 | ||||
| -rw-r--r-- | tests/verific/case.sv | 28 | ||||
| -rw-r--r-- | tests/verific/case.ys | 16 | ||||
| -rw-r--r-- | tests/verific/range_case.sv | 11 | ||||
| -rw-r--r-- | tests/verific/range_case.ys | 16 | ||||
| -rwxr-xr-x | tests/verific/run-test.sh | 4 |
8 files changed, 127 insertions, 0 deletions
diff --git a/tests/arch/fabulous/carry.ys b/tests/arch/fabulous/carry.ys new file mode 100644 index 000000000..bba969d37 --- /dev/null +++ b/tests/arch/fabulous/carry.ys @@ -0,0 +1,9 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +proc +equiv_opt -assert -map +/fabulous/prims.v synth_fabulous -carry ha # 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-max 10 t:LUT4_HA +select -assert-max 4 t:LUT1 +select -assert-none t:LUT1 t:LUT4_HA %% t:* %D diff --git a/tests/various/muxcover.ys b/tests/various/muxcover.ys index 67e9625e6..37a90dcb0 100644 --- a/tests/various/muxcover.ys +++ b/tests/various/muxcover.ys @@ -508,3 +508,43 @@ design -import gate -as gate miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter sat -verify -prove-asserts -show-ports miter + +## implement a mux6 as a mux8 :: https://github.com/YosysHQ/yosys/issues/3591 + +design -reset +read_verilog << EOF +module test (A, S, Y); + parameter INPUTS = 6; + + input [INPUTS-1:0] A; + input [$clog2(INPUTS)-1:0] S; + + wire [15:0] AA = {{(16-INPUTS){1'b0}}, A}; + wire [3:0] SS = {{(4-$clog2(INPUTS)){1'b0}}, S}; + + output Y = SS[3] ? (SS[2] ? SS[1] ? (SS[0] ? AA[15] : AA[14]) + : (SS[0] ? AA[13] : AA[12]) + : SS[1] ? (SS[0] ? AA[11] : AA[10]) + : (SS[0] ? AA[9] : AA[8])) + : (SS[2] ? SS[1] ? (SS[0] ? AA[7] : AA[6]) + : (SS[0] ? AA[5] : AA[4]) + : SS[1] ? (SS[0] ? AA[3] : AA[2]) + : (SS[0] ? AA[1] : AA[0])); +endmodule +EOF + +prep +design -save gold +simplemap t:\$mux +muxcover +opt_clean -purge +select -assert-count 1 t:$_MUX8_ +select -assert-none t:$_MUX8_ %% t:* %D +techmap -map +/simcells.v t:$_MUX8_ +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter +sat -verify -prove-asserts -show-ports miter diff --git a/tests/verific/.gitignore b/tests/verific/.gitignore new file mode 100644 index 000000000..b48f808a1 --- /dev/null +++ b/tests/verific/.gitignore @@ -0,0 +1,3 @@ +/*.log +/*.out +/run-test.mk diff --git a/tests/verific/case.sv b/tests/verific/case.sv new file mode 100644 index 000000000..ed8529b91 --- /dev/null +++ b/tests/verific/case.sv @@ -0,0 +1,28 @@ +module top ( + input clk, + input [5:0] currentstate, + output reg [1:0] o + ); + always @ (posedge clk) + begin + case (currentstate) + 5'd1,5'd2, 5'd3: + begin + o <= 2'b01; + end + 5'd4: + begin + o <= 2'b10; + end + 5'd5,5'd6,5'd7: + begin + o <= 2'b11; + end + default : + begin + o <= 2'b00; + end + endcase + end +endmodule + diff --git a/tests/verific/case.ys b/tests/verific/case.ys new file mode 100644 index 000000000..a181b39cf --- /dev/null +++ b/tests/verific/case.ys @@ -0,0 +1,16 @@ +verific -cfg db_abstract_case_statement_synthesis 0 +read -sv case.sv +verific -import top +prep +rename top gold + +verific -cfg db_abstract_case_statement_synthesis 1 +read -sv case.sv +verific -import top +prep +rename top gate + +miter -equiv -flatten -make_assert gold gate miter +prep -top miter +clk2fflogic +sat -set-init-zero -tempinduct -prove-asserts -verify diff --git a/tests/verific/range_case.sv b/tests/verific/range_case.sv new file mode 100644 index 000000000..9843feafe --- /dev/null +++ b/tests/verific/range_case.sv @@ -0,0 +1,11 @@ +module top(input clk, input signed [3:0] sel_w , output reg out); + +always @ (posedge clk) +begin + case (sel_w) inside + [-4:3] : out <= 1'b1; + [4:5] : out <= 1'b0; + endcase +end + +endmodule diff --git a/tests/verific/range_case.ys b/tests/verific/range_case.ys new file mode 100644 index 000000000..27afbbc17 --- /dev/null +++ b/tests/verific/range_case.ys @@ -0,0 +1,16 @@ +verific -cfg db_abstract_case_statement_synthesis 0 +read -sv range_case.sv +verific -import top +proc +rename top gold + +verific -cfg db_abstract_case_statement_synthesis 1 +read -sv range_case.sv +verific -import top +proc +rename top gate + +miter -equiv -flatten -make_assert gold gate miter +prep -top miter +clk2fflogic +sat -set-init-zero -tempinduct -prove-asserts -verify diff --git a/tests/verific/run-test.sh b/tests/verific/run-test.sh new file mode 100755 index 000000000..2f91cf0fd --- /dev/null +++ b/tests/verific/run-test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +set -eu +source ../gen-tests-makefile.sh +run_tests --yosys-scripts --bash |