diff options
| -rw-r--r-- | CHANGELOG | 16 | ||||
| -rw-r--r-- | Makefile | 9 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 17 | ||||
| -rw-r--r-- | frontends/verific/verific.cc | 56 | ||||
| -rw-r--r-- | passes/cmds/stat.cc | 2 | ||||
| -rw-r--r-- | passes/techmap/muxcover.cc | 5 | ||||
| -rw-r--r-- | techlibs/fabulous/Makefile.inc | 1 | ||||
| -rw-r--r-- | techlibs/fabulous/arith_map.v | 65 | ||||
| -rw-r--r-- | techlibs/fabulous/prims.v | 14 | ||||
| -rw-r--r-- | techlibs/fabulous/synth_fabulous.cc | 15 | ||||
| -rw-r--r-- | techlibs/gatemate/cells_sim.v | 12 | ||||
| -rw-r--r-- | techlibs/gatemate/reg_map.v | 10 | ||||
| -rw-r--r-- | techlibs/gatemate/synth_gatemate.cc | 2 | ||||
| -rw-r--r-- | techlibs/gowin/cells_sim.v | 25 | ||||
| -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 |
22 files changed, 339 insertions, 37 deletions
@@ -2,9 +2,23 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.26 .. Yosys 0.26-dev +Yosys 0.27 .. Yosys 0.27-dev -------------------------- +Yosys 0.26 .. Yosys 0.27 +-------------------------- + * New commands and options + - Added option "-make_assert" to "equiv_make" pass. + - Added option "-coverenable" to "chformal" pass. + + * Verilog + - Resolve package types in interfaces. + - Handle range offsets in packed arrays within packed structs. + - Support for data and array queries on struct/union item expressions. + + * GateMate support + - Enable register initialization. + Yosys 0.25 .. Yosys 0.26 -------------------------- * New commands and options @@ -141,7 +141,7 @@ LDLIBS += -lrt endif endif -YOSYS_VER := 0.26+50 +YOSYS_VER := 0.27+0 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo @@ -157,7 +157,7 @@ endif OBJS = kernel/version_$(GIT_REV).o bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 7e58866.. | wc -l`/;" Makefile + sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 5f88c21.. | wc -l`/;" Makefile # set 'ABCREV = default' to use abc/ as it is # @@ -165,7 +165,7 @@ bumpversion: # is just a symlink to your actual ABC working directory, as 'make mrproper' # will remove the 'abc' directory and you do not want to accidentally # delete your work on ABC.. -ABCREV = a8f0ef2 +ABCREV = 2c1c83f ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) @@ -837,6 +837,9 @@ ABCOPT="" endif test: $(TARGETS) $(EXTRA_TARGETS) +ifeq ($(ENABLE_VERIFIC),1) + +cd tests/verific && bash run-test.sh $(SEEDOPT) +endif +cd tests/simple && bash run-test.sh $(SEEDOPT) +cd tests/simple_abc9 && bash run-test.sh $(SEEDOPT) +cd tests/hana && bash run-test.sh $(SEEDOPT) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index cb21eb3aa..6b81740a2 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -59,9 +59,12 @@ detect_loops = False so = SmtOpts() -def usage(): +def help(): print(os.path.basename(sys.argv[0]) + """ [options] <yosys_smt2_output> + -h, --help + show this message + -t <num_steps> -t <skip_steps>:<num_steps> -t <skip_steps>:<step_size>:<num_steps> @@ -181,19 +184,25 @@ def usage(): (this feature is experimental and incomplete) """ + so.helpmsg()) + +def usage(): + help() sys.exit(1) try: - opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + - ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", + opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:higcm:", so.longopts + + ["help", "final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops"]) except: usage() for o, a in opts: - if o == "-t": + if o in ("-h", "--help"): + help() + sys.exit(0) + elif o == "-t": got_topt = True a = a.split(":") if len(a) == 1: diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index c1e9fc7d0..ab3e55427 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1043,21 +1043,49 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr sw->signal = sig_select; current_case->switches.push_back(sw); - int select_width = inst->InputSize(); - int data_width = inst->OutputSize(); - int select_num = inst->Input1Size() / inst->InputSize(); - - int offset_select = 0; - int offset_data = 0; - - for (int i = 0; i < select_num; i++) { - RTLIL::CaseRule *cs = new RTLIL::CaseRule; - cs->compare.push_back(sig_select_values.extract(offset_select, select_width)); - cs->actions.push_back(SigSig(sig_out_val, sig_data_values.extract(offset_data, data_width))); - sw->cases.push_back(cs); - - offset_select += select_width; + unsigned select_width = inst->InputSize(); + unsigned data_width = inst->OutputSize(); + unsigned offset_data = 0; + unsigned offset_select = 0; + + OperWideCaseSelector* selector = (OperWideCaseSelector*) inst->View(); + + for (unsigned i = 0 ; i < selector->GetNumBranches() ; ++i) { + + SigSig action(sig_out_val, sig_data_values.extract(offset_data, data_width)); offset_data += data_width; + + for (unsigned j = 0 ; j < selector->GetNumConditions(i) ; ++j) { + Array left_bound, right_bound ; + selector->GetCondition(i, j, &left_bound, &right_bound); + + SigSpec sel_left = sig_select_values.extract(offset_select, select_width); + offset_select += select_width; + + if (right_bound.Size()) { + SigSpec sel_right = sig_select_values.extract(offset_select, select_width); + offset_select += select_width; + + log_assert(sel_right.is_fully_const() && sel_right.is_fully_def()); + log_assert(sel_left.is_fully_const() && sel_right.is_fully_def()); + + int32_t left = sel_left.as_int(); + int32_t right = sel_right.as_int(); + int width = sel_left.size(); + + for (int32_t i = right; i<left; i++) { + RTLIL::CaseRule *cs = new RTLIL::CaseRule; + cs->compare.push_back(RTLIL::Const(i,width)); + cs->actions.push_back(action); + sw->cases.push_back(cs); + } + } + + RTLIL::CaseRule *cs = new RTLIL::CaseRule; + cs->compare.push_back(sel_left); + cs->actions.push_back(action); + sw->cases.push_back(cs); + } } RTLIL::CaseRule *cs_default = new RTLIL::CaseRule; cs_default->actions.push_back(SigSig(sig_out_val, sig_data_default)); diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc index 522957f39..f0021cf87 100644 --- a/passes/cmds/stat.cc +++ b/passes/cmds/stat.cc @@ -316,7 +316,7 @@ statdata_t hierarchy_worker(std::map<RTLIL::IdString, statdata_t> &mod_stat, RTL if (mod_stat.count(it.first) > 0) { if (!quiet) log(" %*s%-*s %6u\n", 2*level, "", 26-2*level, log_id(it.first), it.second); - mod_data = mod_data + hierarchy_worker(mod_stat, it.first, level+1) * it.second; + mod_data = mod_data + hierarchy_worker(mod_stat, it.first, level+1, quiet) * it.second; mod_data.num_cells -= it.second; } else { mod_data.num_cells_by_type[it.first] += it.second; diff --git a/passes/techmap/muxcover.cc b/passes/techmap/muxcover.cc index a90d81985..2656f30ce 100644 --- a/passes/techmap/muxcover.cc +++ b/passes/techmap/muxcover.cc @@ -179,7 +179,7 @@ struct MuxcoverWorker int prepare_decode_mux(SigBit &A, SigBit B, SigBit sel, SigBit bit) { - if (A == B || sel == State::Sx) + if (A == B || A == State::Sx || B == State::Sx || sel == State::Sx) return 0; tuple<SigBit, SigBit, SigBit> key(A, B, sel); @@ -197,9 +197,6 @@ struct MuxcoverWorker if (std::get<2>(entry)) return 0; - if (A == State::Sx || B == State::Sx) - return 0; - return cost_dmux / GetSize(std::get<1>(entry)); } diff --git a/techlibs/fabulous/Makefile.inc b/techlibs/fabulous/Makefile.inc index 44d57542b..28b0d5ef0 100644 --- a/techlibs/fabulous/Makefile.inc +++ b/techlibs/fabulous/Makefile.inc @@ -8,3 +8,4 @@ $(eval $(call add_share_file,share/fabulous,techlibs/fabulous/ff_map.v)) $(eval $(call add_share_file,share/fabulous,techlibs/fabulous/ram_regfile.txt)) $(eval $(call add_share_file,share/fabulous,techlibs/fabulous/regfile_map.v)) $(eval $(call add_share_file,share/fabulous,techlibs/fabulous/io_map.v)) +$(eval $(call add_share_file,share/fabulous,techlibs/fabulous/arith_map.v)) diff --git a/techlibs/fabulous/arith_map.v b/techlibs/fabulous/arith_map.v new file mode 100644 index 000000000..eca968556 --- /dev/null +++ b/techlibs/fabulous/arith_map.v @@ -0,0 +1,65 @@ +`default_nettype none + +`ifdef ARITH_ha +(* techmap_celltype = "$alu" *) +module _80_fabulous_ha_alu (A, B, CI, BI, X, Y, CO); + +parameter A_SIGNED = 0; +parameter B_SIGNED = 0; +parameter A_WIDTH = 1; +parameter B_WIDTH = 1; +parameter Y_WIDTH = 1; + +parameter _TECHMAP_CONSTMSK_CI_ = 0; +parameter _TECHMAP_CONSTVAL_CI_ = 0; + +(* force_downto *) +input [A_WIDTH-1:0] A; +(* force_downto *) +input [B_WIDTH-1:0] B; +input CI, BI; +(* force_downto *) +output [Y_WIDTH-1:0] X, Y, CO; + +(* force_downto *) +wire [Y_WIDTH-1:0] A_buf, B_buf; +\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf)); +\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf)); + +(* force_downto *) +wire [Y_WIDTH-1:0] AA = A_buf; +(* force_downto *) +wire [Y_WIDTH-1:0] BB = BI ? ~B_buf : B_buf; +wire [Y_WIDTH:0] CARRY; + + +LUT4_HA #( + .INIT(16'b0), + .I0MUX(1'b1) +) carry_statrt ( + .I0(), .I1(CI), .I2(CI), .I3(), + .Ci(), + .Co(CARRY[0]) +); + +// Carry chain +genvar i; +generate for (i = 0; i < Y_WIDTH; i = i + 1) begin:slice + LUT4_HA #( + .INIT(16'b1001_0110_1001_0110), // full adder sum over (I2, I1, I0) + .I0MUX(1'b1) + ) lut_i ( + .I0(), .I1(AA[i]), .I2(BB[i]), .I3(), + .Ci(CARRY[i]), + .O(Y[i]), + .Co(CARRY[i+1]) + ); + + assign CO[i] = (AA[i] && BB[i]) || ((Y[i] ^ AA[i] ^ BB[i]) && (AA[i] || BB[i])); +end endgenerate + +assign X = AA ^ BB; + +endmodule +`endif + diff --git a/techlibs/fabulous/prims.v b/techlibs/fabulous/prims.v index bd0af906a..fe3e8536a 100644 --- a/techlibs/fabulous/prims.v +++ b/techlibs/fabulous/prims.v @@ -24,6 +24,20 @@ module LUT4(output O, input I0, I1, I2, I3); assign O = I0 ? s1[1] : s1[0]; endmodule +module LUT4_HA(output O, Co, input I0, I1, I2, I3, Ci); + parameter [15:0] INIT = 0; + parameter I0MUX = 1'b1; + + wire [ 7: 0] s3 = I3 ? INIT[15: 8] : INIT[ 7: 0]; + wire [ 3: 0] s2 = I2 ? s3[ 7: 4] : s3[ 3: 0]; + wire [ 1: 0] s1 = I1 ? s2[ 3: 2] : s2[ 1: 0]; + + wire I0_sel = I0MUX ? Ci : I0; + assign O = I0_sel ? s1[1] : s1[0]; + + assign Co = (Ci & I1) | (Ci & I2) | (I1 & I2); +endmodule + module LUTFF(input CLK, D, output reg O); initial O = 1'b0; always @ (posedge CLK) begin diff --git a/techlibs/fabulous/synth_fabulous.cc b/techlibs/fabulous/synth_fabulous.cc index d7c45e094..b4a7ab2dc 100644 --- a/techlibs/fabulous/synth_fabulous.cc +++ b/techlibs/fabulous/synth_fabulous.cc @@ -83,6 +83,9 @@ struct SynthPass : public ScriptPass log(" do not run 'alumacc' pass. i.e. keep arithmetic operators in\n"); log(" their direct form ($add, $sub, etc.).\n"); log("\n"); + log(" -carry <none|ha>\n"); + log(" carry mapping style (none, half-adders, ...) default=none\n"); + log("\n"); log(" -noregfile\n"); log(" do not map register files\n"); log("\n"); @@ -119,7 +122,7 @@ struct SynthPass : public ScriptPass log("\n"); } - string top_module, json_file, blif_file, plib, fsm_opts, memory_opts; + string top_module, json_file, blif_file, plib, fsm_opts, memory_opts, carry_mode; std::vector<string> extra_plib, extra_map; bool autotop, forvpr, noalumacc, nofsm, noshare, noregfile, iopad, complexdff, flatten; @@ -137,6 +140,7 @@ struct SynthPass : public ScriptPass noshare = false; iopad = false; complexdff = false; + carry_mode = "none"; flatten = true; json_file = ""; blif_file = ""; @@ -229,6 +233,12 @@ struct SynthPass : public ScriptPass complexdff = true; continue; } + if (args[argidx] == "-carry") { + carry_mode = args[++argidx]; + if (carry_mode != "none" && carry_mode != "ha") + log_cmd_error("Unsupported carry style: %s\n", carry_mode.c_str()); + continue; + } if (args[argidx] == "-noflatten") { flatten = false; continue; @@ -326,7 +336,8 @@ struct SynthPass : public ScriptPass if (check_label("map_gates")) { run("opt -full"); - run("techmap -map +/techmap.v"); + run(stringf("techmap -map +/techmap.v -map +/fabulous/arith_map.v -D ARITH_%s", + help_mode ? "<carry>" : carry_mode.c_str())); run("opt -fast"); } diff --git a/techlibs/gatemate/cells_sim.v b/techlibs/gatemate/cells_sim.v index 7ed6d83ff..12e01d2df 100644 --- a/techlibs/gatemate/cells_sim.v +++ b/techlibs/gatemate/cells_sim.v @@ -242,7 +242,8 @@ module CC_DFF #( parameter [0:0] CLK_INV = 1'b0,
parameter [0:0] EN_INV = 1'b0,
parameter [0:0] SR_INV = 1'b0,
- parameter [0:0] SR_VAL = 1'b0
+ parameter [0:0] SR_VAL = 1'b0,
+ parameter [0:0] INIT = 1'bx
)(
input D,
(* clkbuf_sink *)
@@ -256,7 +257,7 @@ module CC_DFF #( assign en = (EN_INV) ? ~EN : EN;
assign sr = (SR_INV) ? ~SR : SR;
- initial Q = 1'bX;
+ initial Q = INIT;
always @(posedge clk or posedge sr)
begin
@@ -272,9 +273,10 @@ endmodule module CC_DLT #(
- parameter [0:0] G_INV = 1'b0,
+ parameter [0:0] G_INV = 1'b0,
parameter [0:0] SR_INV = 1'b0,
- parameter [0:0] SR_VAL = 1'b0
+ parameter [0:0] SR_VAL = 1'b0,
+ parameter [0:0] INIT = 1'bx
)(
input D,
input G,
@@ -285,7 +287,7 @@ module CC_DLT #( assign en = (G_INV) ? ~G : G;
assign sr = (SR_INV) ? ~SR : SR;
- initial Q = 1'bX;
+ initial Q = INIT;
always @(*)
begin
diff --git a/techlibs/gatemate/reg_map.v b/techlibs/gatemate/reg_map.v index 6a2c7fb91..6ec170a9d 100644 --- a/techlibs/gatemate/reg_map.v +++ b/techlibs/gatemate/reg_map.v @@ -21,25 +21,31 @@ module \$_DFFE_xxxx_ (input D, C, R, E, output Q);
parameter _TECHMAP_CELLTYPE_ = "";
+ parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
CC_DFF #(
.CLK_INV(_TECHMAP_CELLTYPE_[39:32] == "N"),
.EN_INV(_TECHMAP_CELLTYPE_[15:8] == "N"),
.SR_INV(_TECHMAP_CELLTYPE_[31:24] == "N"),
- .SR_VAL(_TECHMAP_CELLTYPE_[23:16] == "1")
+ .SR_VAL(_TECHMAP_CELLTYPE_[23:16] == "1"),
+ .INIT(_TECHMAP_WIREINIT_Q_)
) _TECHMAP_REPLACE_ (.D(D), .EN(E), .CLK(C), .SR(R), .Q(Q));
+ wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
(* techmap_celltype = "$_DLATCH_[NP][NP][01]_" *)
module \$_DLATCH_xxx_ (input E, R, D, output Q);
parameter _TECHMAP_CELLTYPE_ = "";
+ parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
CC_DLT #(
.G_INV(_TECHMAP_CELLTYPE_[31:24] == "N"),
.SR_INV(_TECHMAP_CELLTYPE_[23:16] == "N"),
- .SR_VAL(_TECHMAP_CELLTYPE_[15:8] == "1")
+ .SR_VAL(_TECHMAP_CELLTYPE_[15:8] == "1"),
+ .INIT(_TECHMAP_WIREINIT_Q_)
) _TECHMAP_REPLACE_ (.D(D), .G(E), .SR(R), .Q(Q));
+ wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
diff --git a/techlibs/gatemate/synth_gatemate.cc b/techlibs/gatemate/synth_gatemate.cc index dd4fde643..1d46d7929 100644 --- a/techlibs/gatemate/synth_gatemate.cc +++ b/techlibs/gatemate/synth_gatemate.cc @@ -283,7 +283,7 @@ struct SynthGateMatePass : public ScriptPass if (check_label("map_regs"))
{
run("opt_clean");
- run("dfflegalize -cell $_DFFE_????_ x -cell $_DLATCH_???_ x");
+ run("dfflegalize -cell $_DFFE_????_ 01 -cell $_DLATCH_???_ 01");
run("techmap -map +/gatemate/reg_map.v");
run("opt_expr -mux_undef");
run("simplemap");
diff --git a/techlibs/gowin/cells_sim.v b/techlibs/gowin/cells_sim.v index ab8207ef1..535fd05ed 100644 --- a/techlibs/gowin/cells_sim.v +++ b/techlibs/gowin/cells_sim.v @@ -582,6 +582,14 @@ module IOBUF (O, IO, I, OEN); assign I = IO; endmodule +module ELVDS_OBUF (I, O, OB); + input I; + output O; + output OB; + assign O = I; + assign OB = ~I; +endmodule + module TLVDS_OBUF (I, O, OB); input I; output O; @@ -1632,3 +1640,20 @@ output OSCOUT; parameter FREQ_DIV = 96; endmodule + +(* blackbox *) +module OSCW(OSCOUT); +output OSCOUT; + +parameter FREQ_DIV = 80; +endmodule + +(* blackbox *) +module OSCO(OSCOUT, OSCEN); +input OSCEN; + +output OSCOUT; + +parameter FREQ_DIV = 100; +parameter REGULATOR_EN = 1'b0; +endmodule 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 |