riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

fabulous: improvements to the pass 

Signed-off-by: gatecat <gatecat@ds0.me>
This commit is contained in:
gatecat 2022-11-10 09:53:07 +01:00 committed by myrtle
parent e3f9ff2679
commit f111bbdf40
13 changed files with 335 additions and 134 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
techlibs/fabulous/Makefile.inc
View File

@ -2,11 +2,9 @@
OBJS += techlibs/fabulous/synth_fabulous.o
$(eval $(call add_share_file,share/fabulous,techlibs/fabulous/cells_map.v))
$(eval $(call add_share_file,share/fabulous,techlibs/fabulous/cells_map_ff.v))
$(eval $(call add_share_file,share/fabulous,techlibs/fabulous/prims.v))
$(eval $(call add_share_file,share/fabulous,techlibs/fabulous/prims_ff.v))
$(eval $(call add_share_file,share/fabulous,techlibs/fabulous/latches_map.v))
$(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))

54
techlibs/fabulous/cells_map_ff.v
View File

@ -1,54 +0,0 @@
module \$lut (A, Y);
parameter WIDTH = 0;
parameter LUT = 0;
input [WIDTH-1:0] A;
output Y;
generate
if (WIDTH == 1) begin
LUT1 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.O(Y), .I0(A[0]));
end else
if (WIDTH == 2) begin
LUT2 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.O(Y), .I0(A[0]), .I1(A[1]));
end else
if (WIDTH == 3) begin
LUT3 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.O(Y), .I0(A[0]), .I1(A[1]), .I2(A[2]));
end else
if (WIDTH == 4) begin
LUT4 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.O(Y), .I0(A[0]), .I1(A[1]), .I2(A[2]), .I3(A[3]));
end else begin
wire _TECHMAP_FAIL_ = 1;
end
endgenerate
endmodule
/* module \$_DFF_P_ (input D, C, output Q); LUTFF _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C)); endmodule
module \$_DFF_N_ (input D, C, output Q); SB_DFFN _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C)); endmodule
module \$_DFF_P_ (input D, C, output Q); SB_DFF _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C)); endmodule
module \$_DFFE_NP_ (input D, C, E, output Q); SB_DFFNE _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .E(E)); endmodule
module \$_DFFE_PP_ (input D, C, E, output Q); SB_DFFE _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .E(E)); endmodule
module \$_DFF_NP0_ (input D, C, R, output Q); SB_DFFNR _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(R)); endmodule
module \$_DFF_NP1_ (input D, C, R, output Q); SB_DFFNS _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .S(R)); endmodule
module \$_DFF_PP0_ (input D, C, R, output Q); SB_DFFR _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(R)); endmodule
module \$_DFF_PP1_ (input D, C, R, output Q); SB_DFFS _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .S(R)); endmodule
module \$_DFFE_NP0P_ (input D, C, E, R, output Q); SB_DFFNER _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .E(E), .R(R)); endmodule
module \$_DFFE_NP1P_ (input D, C, E, R, output Q); SB_DFFNES _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .E(E), .S(R)); endmodule
module \$_DFFE_PP0P_ (input D, C, E, R, output Q); SB_DFFER _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .E(E), .R(R)); endmodule
module \$_DFFE_PP1P_ (input D, C, E, R, output Q); SB_DFFES _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .E(E), .S(R)); endmodule
module \$_SDFF_NP0_ (input D, C, R, output Q); SB_DFFNSR _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(R)); endmodule
module \$_SDFF_NP1_ (input D, C, R, output Q); SB_DFFNSS _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .S(R)); endmodule
module \$_SDFF_PP0_ (input D, C, R, output Q); SB_DFFSR _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(R)); endmodule
module \$_SDFF_PP1_ (input D, C, R, output Q); SB_DFFSS _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .S(R)); endmodule
module \$_SDFFCE_NP0P_ (input D, C, E, R, output Q); SB_DFFNESR _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .E(E), .R(R)); endmodule
module \$_SDFFCE_NP1P_ (input D, C, E, R, output Q); SB_DFFNESS _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .E(E), .S(R)); endmodule
module \$_SDFFCE_PP0P_ (input D, C, E, R, output Q); SB_DFFESR _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .E(E), .R(R)); endmodule
module \$_SDFFCE_PP1P_ (input D, C, E, R, output Q); SB_DFFESS _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .E(E), .S(R)); endmodule */

19
techlibs/fabulous/ff_map.v
View File

@ -1,26 +1,9 @@
module \$_DFF_P_ (input D, C, output Q); LUTFF _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C)); endmodule
//module \$_DFF_N_ (input D, C, output Q); SB_DFFN _TECHMAP_REPLACE_ (.D(D), .O(Q), .C(C)); endmodule
//module \$_DFF_P_ (input D, C, output Q); SB_DFF _TECHMAP_REPLACE_ (.D(D), .O(Q), .C(C)); endmodule
//module \$_DFFE_NP_ (input D, C, E, output Q); SB_DFFNE _TECHMAP_REPLACE_ (.D(D), .O(Q), .C(C), .E(E)); endmodule
module \$_DFFE_PP_ (input D, C, E, output Q); LUTFF_E _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .E(E)); endmodule
//module \$_DFF_NP0_ (input D, C, R, output Q); SB_DFFNR _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .R(R)); endmodule
//module \$_DFF_NP1_ (input D, C, R, output Q); SB_DFFNS _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .S(R)); endmodule
//module \$_DFF_PP0_ (input D, C, R, output Q); LUTFF_R _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .R(R)); endmodule
//module \$_DFF_PP1_ (input D, C, R, output Q); LUTFF_S _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .S(R)); endmodule
//module \$_DFFE_NP0P_ (input D, C, E, R, output Q); SB_DFFNER _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .E(E), .R(R)); endmodule
//module \$_DFFE_NP1P_ (input D, C, E, R, output Q); SB_DFFNES _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .E(E), .S(R)); endmodule
//module \$_DFFE_PP0P_ (input D, C, E, R, output Q); LUTFF_ER _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .E(E), .R(R)); endmodule
//module \$_DFFE_PP1P_ (input D, C, E, R, output Q); LUTFF_ES _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .E(E), .S(R)); endmodule
//module \$_SDFF_NP0_ (input D, C, R, output Q); SB_DFFNSR _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .R(R)); endmodule
//module \$_SDFF_NP1_ (input D, C, R, output Q); SB_DFFNSS _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .S(R)); endmodule
module \$_SDFF_PP0_ (input D, C, R, output Q); LUTFF_SR _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .R(R)); endmodule
module \$_SDFF_PP1_ (input D, C, R, output Q); LUTFF_SS _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .S(R)); endmodule
//module \$_SDFFCE_NP0P_ (input D, C, E, R, output Q); SB_DFFNESR _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .E(E), .R(R)); endmodule
//module \$_SDFFCE_NP1P_ (input D, C, E, R, output Q); SB_DFFNESS _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .E(E), .S(R)); endmodule
module \$_SDFFCE_PP0P_ (input D, C, E, R, output Q); LUTFF_ESR _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .E(E), .R(R)); endmodule
module \$_SDFFCE_PP1P_ (input D, C, E, R, output Q); LUTFF_ESS _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .E(E), .S(R)); endmodule
module \$_SDFFCE_PP1P_ (input D, C, E, R, output Q); LUTFF_ESS _TECHMAP_REPLACE_ (.D(D), .O(Q), .CLK(C), .E(E), .S(R)); endmodule

8
techlibs/fabulous/io_map.v Normal file
View File

@ -0,0 +1,8 @@
module \$__FABULOUS_IBUF (input PAD, output O);
IO_1_bidirectional_frame_config_pass _TECHMAP_REPLACE_ (.PAD(PAD), .O(O), .T(1'b1));
endmodule
module \$__FABULOUS_OBUF (output PAD, input I);
IO_1_bidirectional_frame_config_pass _TECHMAP_REPLACE_ (.PAD(PAD), .I(I), .T(1'b0));
endmodule

16
techlibs/fabulous/prims.v
View File

@ -66,16 +66,16 @@ module FABULOUS_LC #(
//LUT #(.K(K), .INIT(INIT)) lut_i(.I(I), .Q(f_wire));
generate
if (K == 1) begin
LUT1 #(.INIT(INIT)) lut1 (.O(f_wire), .I0(A[0]));
LUT1 #(.INIT(INIT)) lut1 (.O(f_wire), .I0(I[0]));
end else
if (K == 2) begin
LUT2 #(.INIT(INIT)) lut2 (.O(f_wire), .I0(A[0]), .I1(A[1]));
LUT2 #(.INIT(INIT)) lut2 (.O(f_wire), .I0(I[0]), .I1(I[1]));
end else
if (K == 3) begin
LUT3 #(.INIT(INIT)) lut3 (.O(f_wire), .I0(A[0]), .I1(A[1]), .I2(A[2]));
LUT3 #(.INIT(INIT)) lut3 (.O(f_wire), .I0(I[0]), .I1(I[1]), .I2(I[2]));
end else
if (K == 4) begin
LUT4 #(.INIT(INIT)) lut4 (.O(f_wire), .I0(A[0]), .I1(A[1]), .I2(A[2]), .I3(A[3]));
LUT4 #(.INIT(INIT)) lut4 (.O(f_wire), .I0(I[0]), .I1(I[1]), .I2(I[2]), .I3(I[3]));
end
endgenerate
@ -348,7 +348,11 @@ module RegFile_32x4 (D0, D1, D2, D3, W_ADR0, W_ADR1, W_ADR2, W_ADR3, W_ADR4, W_e
endmodule
`ifdef COMPLEX_FLOP
`ifdef EQUIV
`define COMPLEX_DFF
`endif
`ifdef COMPLEX_DFF
module LUTFF_E (
output reg O,
input CLK, E, D
@ -410,4 +414,4 @@ module LUTFF_ESS (
O <= D;
end
endmodule
`endif // COMPLEX_FLOP
`endif // COMPLEX_DFF

227
techlibs/fabulous/synth_fabulous.cc
View File

@ -44,6 +44,18 @@ struct SynthPass : public ScriptPass
log(" -auto-top\n");
log(" automatically determine the top of the design hierarchy\n");
log("\n");
log(" -blif <file>\n");
log(" write the design to the specified BLIF file. writing of an output file\n");
log(" is omitted if this parameter is not specified.\n");
log("\n");
log(" -edif <file>\n");
log(" write the design to the specified EDIF file. writing of an output file\n");
log(" is omitted if this parameter is not specified.\n");
log("\n");
log(" -json <file>\n");
log(" write the design to the specified JSON file. writing of an output file\n");
log(" is omitted if this parameter is not specified.\n");
log("\n");
log(" -lut <k>\n");
log(" perform synthesis for a k-LUT architecture (default 4).\n");
log("\n");
@ -63,6 +75,20 @@ 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(" -noregfile\n");
log(" do not map register files\n");
log("\n");
log(" -iopad\n");
log(" enable automatic insertion of IO buffers (otherwise a wrapper\n");
log(" with manually inserted and constrained IO should be used.)\n");
log("\n");
log(" -complex-dff\n");
log(" enable support for FFs with enable and synchronous SR (must also be\n");
log(" supported by the target fabric.)\n");
log("\n");
log(" -noflatten\n");
log(" do not flatten design after elaboration\n");
log("\n");
log(" -nordff\n");
log(" passed to 'memory'. prohibits merging of FFs into memory read ports\n");
log("\n");
@ -85,8 +111,8 @@ struct SynthPass : public ScriptPass
log("\n");
}
string top_module, plib, fsm_opts, memory_opts;
bool autotop, forvpr, noalumacc, nofsm, noshare;
string top_module, json_file, blif_file, plib, fsm_opts, memory_opts;
bool autotop, forvpr, noalumacc, nofsm, noshare, noregfile, iopad, complexdff, flatten;
int lut;
void clear_flags() override
@ -99,6 +125,11 @@ struct SynthPass : public ScriptPass
noalumacc = false;
nofsm = false;
noshare = false;
iopad = false;
complexdff = false;
flatten = true;
json_file = "";
blif_file = "";
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
@ -113,6 +144,14 @@ struct SynthPass : public ScriptPass
top_module = args[++argidx];
continue;
}
if (args[argidx] == "-json" && argidx+1 < args.size()) {
json_file = args[++argidx];
continue;
}
if (args[argidx] == "-blif" && argidx+1 < args.size()) {
blif_file = args[++argidx];
continue;
}
if (args[argidx] == "-run" && argidx+1 < args.size()) {
size_t pos = args[argidx+1].find(':');
if (pos == std::string::npos) {
@ -160,6 +199,22 @@ struct SynthPass : public ScriptPass
memory_opts += " -no-rw-check";
continue;
}
if (args[argidx] == "-noregfile") {
noregfile = true;
continue;
}
if (args[argidx] == "-iopad") {
iopad = true;
continue;
}
if (args[argidx] == "-complex-dff") {
complexdff = true;
continue;
}
if (args[argidx] == "-noflatten") {
flatten = false;
continue;
}
break;
}
extra_args(args, argidx, design);
@ -178,65 +233,131 @@ struct SynthPass : public ScriptPass
void script() override
{
if (plib.empty())
run("read_verilog -lib +/fabulous/prims.v");
run(stringf("read_verilog %s -lib +/fabulous/prims.v", complexdff ? "-DCOMPLEX_DFF" : ""));
else
run("read_verilog -lib " + plib);
if (top_module.empty()) {
if (autotop)
run("hierarchy -check -auto-top");
else
run("hierarchy -check");
} else
run(stringf("hierarchy -check -top %s", top_module.c_str()));
if (check_label("begin")) {
if (top_module.empty()) {
if (autotop)
run("hierarchy -check -auto-top");
else
run("hierarchy -check");
} else
run(stringf("hierarchy -check -top %s", top_module.c_str()));
run("proc");
}
run("proc");
run("tribuf -logic");
run("deminout");
// synth pass
run("opt_expr");
run("opt_clean");
run("check");
run("opt -nodffe -nosdff");
if (!nofsm)
run("fsm" + fsm_opts, " (unless -nofsm)");
run("opt");
run("wreduce");
run("peepopt");
run("opt_clean");
if (help_mode)
run("techmap -map +/cmp2lut.v -map +/cmp2lcu.v", " (if -lut)");
else if (lut)
run(stringf("techmap -map +/cmp2lut.v -map +/cmp2lcu.v -D LUT_WIDTH=%d", lut));
if (!noalumacc)
run("alumacc", " (unless -noalumacc)");
if (!noshare)
run("share", " (unless -noshare)");
run("opt");
run("memory -nomap" + memory_opts);
run("opt_clean");
if (check_label("flatten", "(unless -noflatten)"))
{
if (flatten) {
run("flatten");
run("tribuf -logic");
run("deminout");
}
}
// RegFile extraction
if (check_label("coarse")) {
run("tribuf -logic");
run("deminout");
run("memory_libmap -lib +/fabulous/ram_regfile.txt");
run("techmap -map +/fabulous/regfile_map.v");
run("opt -fast -mux_undef -undriven -fine");
// synth pass
run("opt_expr");
run("opt_clean");
run("check");
run("opt -nodffe -nosdff");
if (!nofsm)
run("fsm" + fsm_opts, " (unless -nofsm)");
run("opt");
run("wreduce");
run("peepopt");
run("opt_clean");
if (help_mode)
run("techmap -map +/cmp2lut.v -map +/cmp2lcu.v", " (if -lut)");
else if (lut)
run(stringf("techmap -map +/cmp2lut.v -map +/cmp2lcu.v -D LUT_WIDTH=%d", lut));
if (!noalumacc)
run("alumacc", " (unless -noalumacc)");
if (!noshare)
run("share", " (unless -noshare)");
run("opt");
run("memory -nomap" + memory_opts);
run("opt_clean");
}
run("memory_map");
run("opt -undriven -fine");
run("opt -full");
run("techmap -map +/techmap.v");
run("opt -fast");
run("dfflegalize -cell $_DFF_P_ 0 -cell $_DLATCH_?_ x");
run("techmap -map +/fabulous/latches_map.v");
run("abc -lut $LUT_K -dress");
run("clean");
if (!forvpr)
run("techmap -D LUT_K=$LUT_K -map +/fabulous/cells_map.v");
run("clean");
run("hierarchy -check");
run("stat");
if (check_label("map_ram")) {
// RegFile extraction
if (!noregfile) {
run("memory_libmap -lib +/fabulous/ram_regfile.txt");
run("techmap -map +/fabulous/regfile_map.v");
}
}
if (check_label("map_ffram")) {
run("opt -fast -mux_undef -undriven -fine");
run("memory_map");
run("opt -undriven -fine");
}
if (check_label("map_gates")) {
run("opt -full");
run("techmap -map +/techmap.v");
run("opt -fast");
}
if (check_label("map_iopad", "(if -iopad)")) {
if (iopad) {
run("opt -full");
run("iopadmap -bits -outpad $__FABULOUS_OBUF I:PAD -inpad $__FABULOUS_IBUF O:PAD "
"-toutpad IO_1_bidirectional_frame_config_pass ~T:I:PAD "
"-tinoutpad IO_1_bidirectional_frame_config_pass ~T:O:I:PAD A:top", "(skip if '-noiopad')");
run("techmap -map +/fabulous/io_map.v");
}
}
if (check_label("map_ffs")) {
if (complexdff) {
run("dfflegalize -cell $_DFF_P_ 0 -cell $_SDFF_PP?_ 0 -cell $_SDFFCE_PP?P_ 0 -cell $_DLATCH_?_ x", "with -complex-dff");
} else {
run("dfflegalize -cell $_DFF_P_ 0 -cell $_DLATCH_?_ x", "without -complex-dff");
}
run("techmap -map +/fabulous/latches_map.v");
run("techmap -map +/fabulous/ff_map.v");
run("clean");
}
if (check_label("map_luts")) {
run(stringf("abc -lut %d -dress", lut));
run("clean");
}
if (check_label("map_cells")) {
if (!forvpr)
run(stringf("techmap -D LUT_K=%d -map +/fabulous/cells_map.v", lut));
run("clean");
}
if (check_label("check")) {
run("hierarchy -check");
run("stat");
}
if (check_label("blif"))
{
if (!blif_file.empty() || help_mode)
{
run("opt_clean -purge");
run(stringf("write_blif -attr -cname -conn -param %s",
help_mode ? "<file-name>" : blif_file.c_str()));
}
}
if (check_label("json"))
{
if (!json_file.empty() || help_mode)
run(stringf("write_json %s", help_mode ? "<file-name>" : json_file.c_str()));
}
}
} SynthPass;

4
tests/arch/fabulous/.gitignore vendored Normal file
View File

@ -0,0 +1,4 @@
*.log
/run-test.mk
+*_synth.v
+*_testbench

37
tests/arch/fabulous/complexflop.ys Normal file
View File

@ -0,0 +1,37 @@
read_verilog <<EOT
module top ( input d0, d1, d2, d3, ce, sr, clk, output reg q0, q1, q2, q3 );
always @(posedge clk)
begin
if (sr) begin
q0 <= 1'b0;
q1 <= 1'b1;
end else begin
q0 <= d0;
q1 <= d1;
end
if (ce) begin
if (sr) begin
q2 <= 1'b0;
q3 <= 1'b1;
end else begin
q2 <= d2;
q3 <= d3;
end
end
end
endmodule
EOT
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/fabulous/prims.v synth_fabulous -complex-dff # 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:LUTFF_SR
select -assert-count 1 t:LUTFF_SS
select -assert-count 1 t:LUTFF_ESR
select -assert-count 1 t:LUTFF_ESS
select -assert-none t:LUTFF_SR t:LUTFF_SS t:LUTFF_ESR t:LUTFF_ESS %% t:* %D

26
tests/arch/fabulous/counter.ys Normal file
View File

@ -0,0 +1,26 @@
read_verilog <<EOT
module top ( out, clk, reset );
output [7:0] out;
input clk, reset;
reg [7:0] out;
always @(posedge clk)
if (reset)
out <= 8'b0;
else
out <= out + 1;
endmodule
EOT
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/fabulous/prims.v synth_fabulous # 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:LUT2
select -assert-count 7 t:LUT3
select -assert-count 4 t:LUT4
select -assert-count 8 t:LUTFF
select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUTFF %% t:* %D

19
tests/arch/fabulous/fsm.ys Normal file
View File

@ -0,0 +1,19 @@
read_verilog ../common/fsm.v
hierarchy -top fsm
proc
flatten
equiv_opt -run :prove -map +/fabulous/prims.v synth_fabulous
async2sync
miter -equiv -make_assert -flatten gold gate miter
stat
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:LUTFF
select -assert-max 4 t:LUT2
select -assert-max 2 t:LUT3
select -assert-max 9 t:LUT4
select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUTFF %% t:* %D

10
tests/arch/fabulous/logic.ys Normal file
View File

@ -0,0 +1,10 @@
read_verilog ../common/logic.v
hierarchy -top top
proc
equiv_opt -assert -map +/fabulous/prims.v synth_fabulous # 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 1 t:LUT1
select -assert-max 6 t:LUT2
select -assert-max 2 t:LUT4
select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D

33
tests/arch/fabulous/regfile.ys Normal file
View File

@ -0,0 +1,33 @@
read_verilog <<EOT
module sync_sync(input clk, we, input [4:0] aw, aa, ab, input [3:0] wd, output reg [3:0] ra, rb);
reg [3:0] mem[0:31];
always @(posedge clk)
if (we) mem[aw] <= wd;
always @(posedge clk)
ra <= mem[aa];
always @(posedge clk)
rb <= mem[ab];
endmodule
EOT
synth_fabulous -top sync_sync
cd sync_sync
select -assert-count 1 t:RegFile_32x4
design -reset
read_verilog <<EOT
module async_sync(input clk, we, input [4:0] aw, aa, ab, input [3:0] wd, output reg [3:0] ra, rb);
reg [3:0] mem[0:31];
always @(posedge clk)
if (we) mem[aw] <= wd;
always @(posedge clk)
ra <= mem[aa];
always @(*)
rb <= mem[ab];
endmodule
EOT
synth_fabulous -top async_sync
cd async_sync
select -assert-count 1 t:RegFile_32x4

12
tests/arch/fabulous/tribuf.ys Normal file
View File

@ -0,0 +1,12 @@
read_verilog ../common/tribuf.v
hierarchy -top tristate
proc
tribuf
flatten
synth
equiv_opt -assert -map +/fabulous/prims.v -map +/simcells.v synth_fabulous -iopad # 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
select -assert-count 3 t:IO_1_bidirectional_frame_config_pass
select -assert-max 1 t:LUT1
select -assert-none t:IO_1_bidirectional_frame_config_pass t:LUT1 %% t:* %D