mirror of https://github.com/YosysHQ/yosys.git
synth_quicklogic: rearrange files to prepare for adding more architectures
This commit is contained in:
parent
8bd681acfc
commit
98769010af
|
@ -1,13 +1,12 @@
|
||||||
OBJS += techlibs/quicklogic/synth_quicklogic.o
|
OBJS += techlibs/quicklogic/synth_quicklogic.o
|
||||||
|
|
||||||
$(eval $(call add_share_file,share/quicklogic,techlibs/quicklogic/pp3_ffs_map.v))
|
$(eval $(call add_share_file,share/quicklogic/common,techlibs/quicklogic/common/cells_sim.v))
|
||||||
$(eval $(call add_share_file,share/quicklogic,techlibs/quicklogic/pp3_lut_map.v))
|
|
||||||
$(eval $(call add_share_file,share/quicklogic,techlibs/quicklogic/pp3_latches_map.v))
|
|
||||||
$(eval $(call add_share_file,share/quicklogic,techlibs/quicklogic/pp3_cells_map.v))
|
|
||||||
$(eval $(call add_share_file,share/quicklogic,techlibs/quicklogic/cells_sim.v))
|
|
||||||
$(eval $(call add_share_file,share/quicklogic,techlibs/quicklogic/lut_sim.v))
|
|
||||||
$(eval $(call add_share_file,share/quicklogic,techlibs/quicklogic/pp3_cells_sim.v))
|
|
||||||
|
|
||||||
$(eval $(call add_share_file,share/quicklogic,techlibs/quicklogic/abc9_model.v))
|
$(eval $(call add_share_file,share/quicklogic/pp3,techlibs/quicklogic/pp3/ffs_map.v))
|
||||||
$(eval $(call add_share_file,share/quicklogic,techlibs/quicklogic/abc9_map.v))
|
$(eval $(call add_share_file,share/quicklogic/pp3,techlibs/quicklogic/pp3/lut_map.v))
|
||||||
$(eval $(call add_share_file,share/quicklogic,techlibs/quicklogic/abc9_unmap.v))
|
$(eval $(call add_share_file,share/quicklogic/pp3,techlibs/quicklogic/pp3/latches_map.v))
|
||||||
|
$(eval $(call add_share_file,share/quicklogic/pp3,techlibs/quicklogic/pp3/cells_map.v))
|
||||||
|
$(eval $(call add_share_file,share/quicklogic/pp3,techlibs/quicklogic/pp3/cells_sim.v))
|
||||||
|
$(eval $(call add_share_file,share/quicklogic/pp3,techlibs/quicklogic/pp3/abc9_model.v))
|
||||||
|
$(eval $(call add_share_file,share/quicklogic/pp3,techlibs/quicklogic/pp3/abc9_map.v))
|
||||||
|
$(eval $(call add_share_file,share/quicklogic/pp3,techlibs/quicklogic/pp3/abc9_unmap.v))
|
||||||
|
|
|
@ -1,76 +0,0 @@
|
||||||
(* abc9_lut=1, lib_whitebox *)
|
|
||||||
module LUT1 (
|
|
||||||
output O,
|
|
||||||
input I0
|
|
||||||
);
|
|
||||||
parameter [1:0] INIT = 0;
|
|
||||||
parameter EQN = "(I0)";
|
|
||||||
|
|
||||||
// These timings are for PolarPro 3E; other families will need updating.
|
|
||||||
specify
|
|
||||||
(I0 => O) = 698; // FS -> FZ
|
|
||||||
endspecify
|
|
||||||
|
|
||||||
assign O = I0 ? INIT[1] : INIT[0];
|
|
||||||
endmodule
|
|
||||||
|
|
||||||
// TZ TSL TAB
|
|
||||||
(* abc9_lut=2, lib_whitebox *)
|
|
||||||
module LUT2 (
|
|
||||||
output O,
|
|
||||||
input I0, I1
|
|
||||||
);
|
|
||||||
parameter [3:0] INIT = 4'h0;
|
|
||||||
parameter EQN = "(I0)";
|
|
||||||
|
|
||||||
// These timings are for PolarPro 3E; other families will need updating.
|
|
||||||
specify
|
|
||||||
(I0 => O) = 1251; // TAB -> TZ
|
|
||||||
(I1 => O) = 1406; // TSL -> TZ
|
|
||||||
endspecify
|
|
||||||
|
|
||||||
wire [1:0] s1 = I1 ? INIT[3:2] : INIT[1:0];
|
|
||||||
assign O = I0 ? s1[1] : s1[0];
|
|
||||||
endmodule
|
|
||||||
|
|
||||||
(* abc9_lut=2, lib_whitebox *)
|
|
||||||
module LUT3 (
|
|
||||||
output O,
|
|
||||||
input I0, I1, I2
|
|
||||||
);
|
|
||||||
parameter [7:0] INIT = 8'h0;
|
|
||||||
parameter EQN = "(I0)";
|
|
||||||
|
|
||||||
// These timings are for PolarPro 3E; other families will need updating.
|
|
||||||
specify
|
|
||||||
(I0 => O) = 1251; // TAB -> TZ
|
|
||||||
(I1 => O) = 1406; // TSL -> TZ
|
|
||||||
(I2 => O) = 1699; // ('TA1', 'TA2', 'TB1', 'TB2') -> TZ
|
|
||||||
endspecify
|
|
||||||
|
|
||||||
wire [3:0] s2 = I2 ? INIT[7:4] : INIT[3:0];
|
|
||||||
wire [1:0] s1 = I1 ? s2[3:2] : s2[1:0];
|
|
||||||
assign O = I0 ? s1[1] : s1[0];
|
|
||||||
endmodule
|
|
||||||
|
|
||||||
(* abc9_lut=4, lib_whitebox *)
|
|
||||||
module LUT4 (
|
|
||||||
output O,
|
|
||||||
input I0, I1, I2, I3
|
|
||||||
);
|
|
||||||
parameter [15:0] INIT = 16'h0;
|
|
||||||
parameter EQN = "(I0)";
|
|
||||||
|
|
||||||
// These timings are for PolarPro 3E; other families will need updating.
|
|
||||||
specify
|
|
||||||
(I0 => O) = 995; // TBS -> CZ
|
|
||||||
(I1 => O) = 1437; // ('TAB', 'BAB') -> CZ
|
|
||||||
(I2 => O) = 1593; // ('TSL', 'BSL') -> CZ
|
|
||||||
(I3 => O) = 1887; // ('TA1', 'TA2', 'TB1', 'TB2', 'BA1', 'BA2', 'BB1', 'BB2') -> CZ
|
|
||||||
endspecify
|
|
||||||
|
|
||||||
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];
|
|
||||||
assign O = I0 ? s1[1] : s1[0];
|
|
||||||
endmodule
|
|
|
@ -327,3 +327,80 @@ module qlal4s3b_cell_macro (
|
||||||
);
|
);
|
||||||
|
|
||||||
endmodule
|
endmodule
|
||||||
|
|
||||||
|
(* abc9_lut=1, lib_whitebox *)
|
||||||
|
module LUT1 (
|
||||||
|
output O,
|
||||||
|
input I0
|
||||||
|
);
|
||||||
|
parameter [1:0] INIT = 0;
|
||||||
|
parameter EQN = "(I0)";
|
||||||
|
|
||||||
|
// These timings are for PolarPro 3E; other families will need updating.
|
||||||
|
specify
|
||||||
|
(I0 => O) = 698; // FS -> FZ
|
||||||
|
endspecify
|
||||||
|
|
||||||
|
assign O = I0 ? INIT[1] : INIT[0];
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
// TZ TSL TAB
|
||||||
|
(* abc9_lut=2, lib_whitebox *)
|
||||||
|
module LUT2 (
|
||||||
|
output O,
|
||||||
|
input I0, I1
|
||||||
|
);
|
||||||
|
parameter [3:0] INIT = 4'h0;
|
||||||
|
parameter EQN = "(I0)";
|
||||||
|
|
||||||
|
// These timings are for PolarPro 3E; other families will need updating.
|
||||||
|
specify
|
||||||
|
(I0 => O) = 1251; // TAB -> TZ
|
||||||
|
(I1 => O) = 1406; // TSL -> TZ
|
||||||
|
endspecify
|
||||||
|
|
||||||
|
wire [1:0] s1 = I1 ? INIT[3:2] : INIT[1:0];
|
||||||
|
assign O = I0 ? s1[1] : s1[0];
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
(* abc9_lut=2, lib_whitebox *)
|
||||||
|
module LUT3 (
|
||||||
|
output O,
|
||||||
|
input I0, I1, I2
|
||||||
|
);
|
||||||
|
parameter [7:0] INIT = 8'h0;
|
||||||
|
parameter EQN = "(I0)";
|
||||||
|
|
||||||
|
// These timings are for PolarPro 3E; other families will need updating.
|
||||||
|
specify
|
||||||
|
(I0 => O) = 1251; // TAB -> TZ
|
||||||
|
(I1 => O) = 1406; // TSL -> TZ
|
||||||
|
(I2 => O) = 1699; // ('TA1', 'TA2', 'TB1', 'TB2') -> TZ
|
||||||
|
endspecify
|
||||||
|
|
||||||
|
wire [3:0] s2 = I2 ? INIT[7:4] : INIT[3:0];
|
||||||
|
wire [1:0] s1 = I1 ? s2[3:2] : s2[1:0];
|
||||||
|
assign O = I0 ? s1[1] : s1[0];
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
(* abc9_lut=4, lib_whitebox *)
|
||||||
|
module LUT4 (
|
||||||
|
output O,
|
||||||
|
input I0, I1, I2, I3
|
||||||
|
);
|
||||||
|
parameter [15:0] INIT = 16'h0;
|
||||||
|
parameter EQN = "(I0)";
|
||||||
|
|
||||||
|
// These timings are for PolarPro 3E; other families will need updating.
|
||||||
|
specify
|
||||||
|
(I0 => O) = 995; // TBS -> CZ
|
||||||
|
(I1 => O) = 1437; // ('TAB', 'BAB') -> CZ
|
||||||
|
(I2 => O) = 1593; // ('TSL', 'BSL') -> CZ
|
||||||
|
(I3 => O) = 1887; // ('TA1', 'TA2', 'TB1', 'TB2', 'BA1', 'BA2', 'BB1', 'BB2') -> CZ
|
||||||
|
endspecify
|
||||||
|
|
||||||
|
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];
|
||||||
|
assign O = I0 ? s1[1] : s1[0];
|
||||||
|
endmodule
|
|
@ -60,13 +60,14 @@ struct SynthQuickLogicPass : public ScriptPass {
|
||||||
log("\n");
|
log("\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
string top_opt, blif_file, family, currmodule, verilog_file;
|
string top_opt, blif_file, edif_file, family, currmodule, verilog_file, lib_path;
|
||||||
bool abc9;
|
bool abc9;
|
||||||
|
|
||||||
void clear_flags() override
|
void clear_flags() override
|
||||||
{
|
{
|
||||||
top_opt = "-auto-top";
|
top_opt = "-auto-top";
|
||||||
blif_file = "";
|
blif_file = "";
|
||||||
|
edif_file = "";
|
||||||
verilog_file = "";
|
verilog_file = "";
|
||||||
currmodule = "";
|
currmodule = "";
|
||||||
family = "pp3";
|
family = "pp3";
|
||||||
|
@ -81,6 +82,14 @@ struct SynthQuickLogicPass : public ScriptPass {
|
||||||
size_t argidx;
|
size_t argidx;
|
||||||
for (argidx = 1; argidx < args.size(); argidx++)
|
for (argidx = 1; argidx < args.size(); argidx++)
|
||||||
{
|
{
|
||||||
|
if (args[argidx] == "-run" && argidx+1 < args.size()) {
|
||||||
|
size_t pos = args[argidx+1].find(':');
|
||||||
|
if (pos == std::string::npos)
|
||||||
|
break;
|
||||||
|
run_from = args[++argidx].substr(0, pos);
|
||||||
|
run_to = args[argidx].substr(pos+1);
|
||||||
|
continue;
|
||||||
|
}
|
||||||
if (args[argidx] == "-top" && argidx+1 < args.size()) {
|
if (args[argidx] == "-top" && argidx+1 < args.size()) {
|
||||||
top_opt = "-top " + args[++argidx];
|
top_opt = "-top " + args[++argidx];
|
||||||
continue;
|
continue;
|
||||||
|
@ -93,6 +102,10 @@ struct SynthQuickLogicPass : public ScriptPass {
|
||||||
blif_file = args[++argidx];
|
blif_file = args[++argidx];
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
if (args[argidx] == "-edif" && argidx + 1 < args.size()) {
|
||||||
|
edif_file = args[++argidx];
|
||||||
|
continue;
|
||||||
|
}
|
||||||
if (args[argidx] == "-verilog" && argidx+1 < args.size()) {
|
if (args[argidx] == "-verilog" && argidx+1 < args.size()) {
|
||||||
verilog_file = args[++argidx];
|
verilog_file = args[++argidx];
|
||||||
continue;
|
continue;
|
||||||
|
@ -126,13 +139,16 @@ struct SynthQuickLogicPass : public ScriptPass {
|
||||||
|
|
||||||
void script() override
|
void script() override
|
||||||
{
|
{
|
||||||
|
if (help_mode) {
|
||||||
|
family = "<family>";
|
||||||
|
}
|
||||||
|
|
||||||
if (check_label("begin")) {
|
if (check_label("begin")) {
|
||||||
run(stringf("read_verilog -lib -specify +/quicklogic/cells_sim.v +/quicklogic/%s_cells_sim.v", family.c_str()));
|
run(stringf("read_verilog -lib -specify +/quicklogic/common/cells_sim.v +/quicklogic/%s/cells_sim.v", family.c_str()));
|
||||||
run("read_verilog -lib -specify +/quicklogic/lut_sim.v");
|
|
||||||
run(stringf("hierarchy -check %s", help_mode ? "-top <top>" : top_opt.c_str()));
|
run(stringf("hierarchy -check %s", help_mode ? "-top <top>" : top_opt.c_str()));
|
||||||
}
|
}
|
||||||
|
|
||||||
if (check_label("coarse")) {
|
if (check_label("prepare")) {
|
||||||
run("proc");
|
run("proc");
|
||||||
run("flatten");
|
run("flatten");
|
||||||
run("tribuf -logic");
|
run("tribuf -logic");
|
||||||
|
@ -147,6 +163,9 @@ struct SynthQuickLogicPass : public ScriptPass {
|
||||||
run("peepopt");
|
run("peepopt");
|
||||||
run("opt_clean");
|
run("opt_clean");
|
||||||
run("share");
|
run("share");
|
||||||
|
}
|
||||||
|
|
||||||
|
if (check_label("coarse")) {
|
||||||
run("techmap -map +/cmp2lut.v -D LUT_WIDTH=4");
|
run("techmap -map +/cmp2lut.v -D LUT_WIDTH=4");
|
||||||
run("opt_expr");
|
run("opt_expr");
|
||||||
run("opt_clean");
|
run("opt_clean");
|
||||||
|
@ -175,18 +194,18 @@ struct SynthQuickLogicPass : public ScriptPass {
|
||||||
run("opt_expr");
|
run("opt_expr");
|
||||||
run("dfflegalize -cell $_DFFSRE_PPPP_ 0 -cell $_DLATCH_?_ x");
|
run("dfflegalize -cell $_DFFSRE_PPPP_ 0 -cell $_DLATCH_?_ x");
|
||||||
|
|
||||||
run(stringf("techmap -map +/quicklogic/%s_cells_map.v -map +/quicklogic/%s_ffs_map.v", family.c_str(), family.c_str()));
|
run(stringf("techmap -map +/quicklogic/%s/cells_map.v -map +/quicklogic/%s/ffs_map.v", family.c_str(), family.c_str()));
|
||||||
|
|
||||||
run("opt_expr -mux_undef");
|
run("opt_expr -mux_undef");
|
||||||
}
|
}
|
||||||
|
|
||||||
if (check_label("map_luts")) {
|
if (check_label("map_luts")) {
|
||||||
run(stringf("techmap -map +/quicklogic/%s_latches_map.v", family.c_str()));
|
run(stringf("techmap -map +/quicklogic/%s/latches_map.v", family.c_str()));
|
||||||
if (abc9) {
|
if (abc9) {
|
||||||
run("read_verilog -lib -specify -icells +/quicklogic/abc9_model.v");
|
run(stringf("read_verilog -lib -specify -icells +/quicklogic/%s/abc9_model.v", family.c_str()));
|
||||||
run("techmap -map +/quicklogic/abc9_map.v");
|
run(stringf("techmap -map +/quicklogic/%s/abc9_map.v", family.c_str()));
|
||||||
run("abc9 -maxlut 4 -dff");
|
run("abc9 -maxlut 4 -dff");
|
||||||
run("techmap -map +/quicklogic/abc9_unmap.v");
|
run(stringf("techmap -map +/quicklogic/%s/abc9_unmap.v", family.c_str()));
|
||||||
} else {
|
} else {
|
||||||
run("abc -luts 1,2,2,4 -dress");
|
run("abc -luts 1,2,2,4 -dress");
|
||||||
}
|
}
|
||||||
|
@ -194,7 +213,7 @@ struct SynthQuickLogicPass : public ScriptPass {
|
||||||
}
|
}
|
||||||
|
|
||||||
if (check_label("map_cells")) {
|
if (check_label("map_cells")) {
|
||||||
run(stringf("techmap -map +/quicklogic/%s_lut_map.v", family.c_str()));
|
run(stringf("techmap -map +/quicklogic/%s/lut_map.v", family.c_str()));
|
||||||
run("clean");
|
run("clean");
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -218,17 +237,24 @@ struct SynthQuickLogicPass : public ScriptPass {
|
||||||
run("blackbox =A:whitebox");
|
run("blackbox =A:whitebox");
|
||||||
}
|
}
|
||||||
|
|
||||||
if (check_label("blif")) {
|
if (check_label("blif", "(if -blif)")) {
|
||||||
if (!blif_file.empty() || help_mode) {
|
if (!blif_file.empty() || help_mode) {
|
||||||
run(stringf("write_blif -attr -param %s %s", top_opt.c_str(), blif_file.c_str()));
|
run(stringf("write_blif -attr -param %s %s", top_opt.c_str(), blif_file.c_str()));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (check_label("verilog")) {
|
if (check_label("verilog", "(if -verilog)")) {
|
||||||
if (!verilog_file.empty() || help_mode) {
|
if (!verilog_file.empty() || help_mode) {
|
||||||
run(stringf("write_verilog -noattr -nohex %s", help_mode ? "<file-name>" : verilog_file.c_str()));
|
run(stringf("write_verilog -noattr -nohex %s", help_mode ? "<file-name>" : verilog_file.c_str()));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (check_label("edif", "(if -edif)")) {
|
||||||
|
if (!edif_file.empty() || help_mode) {
|
||||||
|
run("splitnets -ports -format ()");
|
||||||
|
run(stringf("write_edif -nogndvcc -attrprop -pvector par %s %s", top_opt.c_str(), edif_file.c_str()));
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
} SynthQuicklogicPass;
|
} SynthQuicklogicPass;
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
read_verilog ../common/add_sub.v
|
read_verilog ../common/add_sub.v
|
||||||
hierarchy -top top
|
hierarchy -top top
|
||||||
equiv_opt -assert -map +/quicklogic/lut_sim.v -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 # equivalency check
|
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v synth_quicklogic -family pp3 # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
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
|
cd top # Constrain all select calls below inside the top module
|
||||||
select -assert-count 2 t:LUT2
|
select -assert-count 2 t:LUT2
|
||||||
|
|
|
@ -3,7 +3,7 @@ design -save read
|
||||||
|
|
||||||
hierarchy -top adff
|
hierarchy -top adff
|
||||||
proc
|
proc
|
||||||
equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v synth_quicklogic # equivalency check
|
equiv_opt -async2sync -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
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
|
cd adff # Constrain all select calls below inside the top module
|
||||||
select -assert-count 1 t:dffepc
|
select -assert-count 1 t:dffepc
|
||||||
|
@ -19,7 +19,7 @@ select -assert-none t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:*
|
||||||
design -load read
|
design -load read
|
||||||
hierarchy -top adffn
|
hierarchy -top adffn
|
||||||
proc
|
proc
|
||||||
equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # equivalency check
|
equiv_opt -async2sync -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
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
|
cd adffn # Constrain all select calls below inside the top module
|
||||||
select -assert-count 1 t:LUT1
|
select -assert-count 1 t:LUT1
|
||||||
|
@ -36,7 +36,7 @@ select -assert-none t:LUT1 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad
|
||||||
design -load read
|
design -load read
|
||||||
hierarchy -top dffs
|
hierarchy -top dffs
|
||||||
proc
|
proc
|
||||||
equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # equivalency check
|
equiv_opt -async2sync -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
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
|
cd dffs # Constrain all select calls below inside the top module
|
||||||
select -assert-count 1 t:LUT2
|
select -assert-count 1 t:LUT2
|
||||||
|
@ -53,7 +53,7 @@ select -assert-none t:LUT2 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad
|
||||||
design -load read
|
design -load read
|
||||||
hierarchy -top ndffnr
|
hierarchy -top ndffnr
|
||||||
proc
|
proc
|
||||||
equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # equivalency check
|
equiv_opt -async2sync -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
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
|
cd ndffnr # Constrain all select calls below inside the top module
|
||||||
select -assert-count 1 t:LUT1
|
select -assert-count 1 t:LUT1
|
||||||
|
|
|
@ -2,7 +2,7 @@ read_verilog ../common/counter.v
|
||||||
hierarchy -top top
|
hierarchy -top top
|
||||||
proc
|
proc
|
||||||
flatten
|
flatten
|
||||||
equiv_opt -assert -multiclock -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # equivalency check
|
equiv_opt -assert -multiclock -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
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
|
cd top # Constrain all select calls below inside the top module
|
||||||
select -assert-count 1 t:LUT1
|
select -assert-count 1 t:LUT1
|
||||||
|
|
|
@ -5,7 +5,7 @@ design -save read
|
||||||
|
|
||||||
hierarchy -top my_dff
|
hierarchy -top my_dff
|
||||||
proc
|
proc
|
||||||
equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v synth_quicklogic # equivalency check
|
equiv_opt -async2sync -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||||
cd my_dff # Constrain all select calls below inside the top module
|
cd my_dff # Constrain all select calls below inside the top module
|
||||||
select -assert-count 1 t:ckpad
|
select -assert-count 1 t:ckpad
|
||||||
|
@ -20,7 +20,7 @@ select -assert-none t:ckpad t:dffepc t:inpad t:logic_0 t:logic_1 t:outpad %% t:*
|
||||||
design -load read
|
design -load read
|
||||||
hierarchy -top my_dffe
|
hierarchy -top my_dffe
|
||||||
proc
|
proc
|
||||||
equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v synth_quicklogic # equivalency check
|
equiv_opt -async2sync -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||||
cd my_dffe # Constrain all select calls below inside the top module
|
cd my_dffe # Constrain all select calls below inside the top module
|
||||||
|
|
||||||
|
|
|
@ -3,7 +3,7 @@ hierarchy -top fsm
|
||||||
proc
|
proc
|
||||||
flatten
|
flatten
|
||||||
|
|
||||||
equiv_opt -run :prove -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic
|
equiv_opt -run :prove -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic
|
||||||
async2sync
|
async2sync
|
||||||
miter -equiv -make_assert -flatten gold gate miter
|
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
|
sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
|
||||||
|
|
|
@ -1,7 +1,7 @@
|
||||||
read_verilog ../common/logic.v
|
read_verilog ../common/logic.v
|
||||||
hierarchy -top top
|
hierarchy -top top
|
||||||
proc
|
proc
|
||||||
equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # equivalency check
|
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
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
|
cd top # Constrain all select calls below inside the top module
|
||||||
|
|
||||||
|
|
|
@ -3,7 +3,7 @@ design -save read
|
||||||
|
|
||||||
hierarchy -top mux2
|
hierarchy -top mux2
|
||||||
proc
|
proc
|
||||||
equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # equivalency check
|
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
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
|
cd mux2 # Constrain all select calls below inside the top module
|
||||||
select -assert-count 1 t:LUT3
|
select -assert-count 1 t:LUT3
|
||||||
|
@ -15,7 +15,7 @@ select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D
|
||||||
design -load read
|
design -load read
|
||||||
hierarchy -top mux4
|
hierarchy -top mux4
|
||||||
proc
|
proc
|
||||||
equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # equivalency check
|
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
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
|
cd mux4 # Constrain all select calls below inside the top module
|
||||||
select -assert-count 3 t:LUT3
|
select -assert-count 3 t:LUT3
|
||||||
|
@ -27,7 +27,7 @@ select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D
|
||||||
design -load read
|
design -load read
|
||||||
hierarchy -top mux8
|
hierarchy -top mux8
|
||||||
proc
|
proc
|
||||||
equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # equivalency check
|
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
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
|
cd mux8 # Constrain all select calls below inside the top module
|
||||||
select -assert-count 1 t:LUT1
|
select -assert-count 1 t:LUT1
|
||||||
|
@ -41,7 +41,7 @@ select -assert-none t:LUT1 t:LUT3 t:mux4x0 t:inpad t:outpad %% t:* %D
|
||||||
design -load read
|
design -load read
|
||||||
hierarchy -top mux16
|
hierarchy -top mux16
|
||||||
proc
|
proc
|
||||||
equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # equivalency check
|
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
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
|
cd mux16 # Constrain all select calls below inside the top module
|
||||||
select -assert-count 1 t:LUT3
|
select -assert-count 1 t:LUT3
|
||||||
|
|
|
@ -4,7 +4,7 @@ proc
|
||||||
tribuf
|
tribuf
|
||||||
flatten
|
flatten
|
||||||
synth
|
synth
|
||||||
equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/simcells.v synth_quicklogic # equivalency check
|
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v -map +/simcells.v synth_quicklogic # equivalency check
|
||||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
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
|
cd tristate # Constrain all select calls below inside the top module
|
||||||
select -assert-count 2 t:inpad
|
select -assert-count 2 t:inpad
|
||||||
|
|
Loading…
Reference in New Issue