aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile5
-rw-r--r--frontends/verific/verific.cc56
-rw-r--r--passes/cmds/stat.cc2
-rw-r--r--passes/techmap/muxcover.cc5
-rw-r--r--techlibs/fabulous/Makefile.inc1
-rw-r--r--techlibs/fabulous/arith_map.v65
-rw-r--r--techlibs/fabulous/prims.v14
-rw-r--r--techlibs/fabulous/synth_fabulous.cc15
-rw-r--r--techlibs/gatemate/cells_sim.v12
-rw-r--r--techlibs/gatemate/reg_map.v10
-rw-r--r--techlibs/gatemate/synth_gatemate.cc2
-rw-r--r--techlibs/gowin/cells_sim.v25
-rw-r--r--tests/arch/fabulous/carry.ys9
-rw-r--r--tests/various/muxcover.ys40
-rw-r--r--tests/verific/.gitignore3
-rw-r--r--tests/verific/case.sv28
-rw-r--r--tests/verific/case.ys16
-rw-r--r--tests/verific/range_case.sv11
-rw-r--r--tests/verific/range_case.ys16
-rwxr-xr-xtests/verific/run-test.sh4
20 files changed, 309 insertions, 30 deletions
diff --git a/Makefile b/Makefile
index 2b5f2c079..d7c2afacc 100644
--- a/Makefile
+++ b/Makefile
@@ -141,7 +141,7 @@ LDLIBS += -lrt
endif
endif
-YOSYS_VER := 0.26+50
+YOSYS_VER := 0.26+62
# Note: We arrange for .gitcommit to contain the (short) commit hash in
# tarballs generated with git-archive(1) using .gitattributes. The git repo
@@ -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/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
generated by cgit v1.2.3 (git 2.25.1) at 2024-05-28 22:39:12 +0000