mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-10-31 03:32:29 +00:00 
			
		
		
		
	synth_quicklogic: rearrange files to prepare for adding more architectures
This commit is contained in:
		
							parent
							
								
									031ad38b5c
								
							
						
					
					
						commit
						e230a871be
					
				
					 20 changed files with 139 additions and 113 deletions
				
			
		|  | @ -1,13 +1,12 @@ | |||
| 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,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/common,techlibs/quicklogic/common/cells_sim.v)) | ||||
| 
 | ||||
| $(eval $(call add_share_file,share/quicklogic,techlibs/quicklogic/abc9_model.v)) | ||||
| $(eval $(call add_share_file,share/quicklogic,techlibs/quicklogic/abc9_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/ffs_map.v)) | ||||
| $(eval $(call add_share_file,share/quicklogic/pp3,techlibs/quicklogic/pp3/lut_map.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 | ||||
| 
 | ||||
| (* 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"); | ||||
| 	} | ||||
| 
 | ||||
| 	string top_opt, blif_file, family, currmodule, verilog_file; | ||||
| 	string top_opt, blif_file, edif_file, family, currmodule, verilog_file, lib_path; | ||||
| 	bool abc9; | ||||
| 
 | ||||
| 	void clear_flags() override | ||||
| 	{ | ||||
| 		top_opt = "-auto-top"; | ||||
| 		blif_file = ""; | ||||
| 		edif_file = ""; | ||||
| 		verilog_file = ""; | ||||
| 		currmodule = ""; | ||||
| 		family = "pp3"; | ||||
|  | @ -81,6 +82,14 @@ struct SynthQuickLogicPass : public ScriptPass { | |||
| 		size_t 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()) { | ||||
| 				top_opt = "-top " + args[++argidx]; | ||||
| 				continue; | ||||
|  | @ -93,6 +102,10 @@ struct SynthQuickLogicPass : public ScriptPass { | |||
| 				blif_file = args[++argidx]; | ||||
| 				continue; | ||||
| 			} | ||||
| 			if (args[argidx] == "-edif" && argidx + 1 < args.size()) { | ||||
| 				edif_file = args[++argidx]; | ||||
| 				continue; | ||||
| 			} | ||||
| 			if (args[argidx] == "-verilog" && argidx+1 < args.size()) { | ||||
| 				verilog_file = args[++argidx]; | ||||
| 				continue; | ||||
|  | @ -126,13 +139,16 @@ struct SynthQuickLogicPass : public ScriptPass { | |||
| 
 | ||||
| 	void script() override | ||||
| 	{ | ||||
| 		if (help_mode) { | ||||
| 			family = "<family>"; | ||||
| 		} | ||||
| 
 | ||||
| 		if (check_label("begin")) { | ||||
| 			run(stringf("read_verilog -lib -specify +/quicklogic/cells_sim.v +/quicklogic/%s_cells_sim.v", family.c_str())); | ||||
| 			run("read_verilog -lib -specify +/quicklogic/lut_sim.v"); | ||||
| 			run(stringf("read_verilog -lib -specify +/quicklogic/common/cells_sim.v +/quicklogic/%s/cells_sim.v", family.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("flatten"); | ||||
| 			run("tribuf -logic"); | ||||
|  | @ -147,6 +163,9 @@ struct SynthQuickLogicPass : public ScriptPass { | |||
| 			run("peepopt"); | ||||
| 			run("opt_clean"); | ||||
| 			run("share"); | ||||
| 		} | ||||
| 
 | ||||
| 		if (check_label("coarse")) { | ||||
| 			run("techmap -map +/cmp2lut.v -D LUT_WIDTH=4"); | ||||
| 			run("opt_expr"); | ||||
| 			run("opt_clean"); | ||||
|  | @ -175,18 +194,18 @@ struct SynthQuickLogicPass : public ScriptPass { | |||
| 			run("opt_expr"); | ||||
| 			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"); | ||||
| 		} | ||||
| 
 | ||||
| 		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) { | ||||
| 				run("read_verilog -lib -specify -icells +/quicklogic/abc9_model.v"); | ||||
| 				run("techmap -map +/quicklogic/abc9_map.v"); | ||||
| 				run(stringf("read_verilog -lib -specify -icells +/quicklogic/%s/abc9_model.v", family.c_str())); | ||||
| 				run(stringf("techmap -map +/quicklogic/%s/abc9_map.v", family.c_str())); | ||||
| 				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 { | ||||
| 				run("abc -luts 1,2,2,4 -dress"); | ||||
| 			} | ||||
|  | @ -194,7 +213,7 @@ struct SynthQuickLogicPass : public ScriptPass { | |||
| 		} | ||||
| 
 | ||||
| 		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"); | ||||
| 		} | ||||
| 
 | ||||
|  | @ -218,17 +237,24 @@ struct SynthQuickLogicPass : public ScriptPass { | |||
| 			run("blackbox =A:whitebox"); | ||||
| 		} | ||||
| 
 | ||||
| 		if (check_label("blif")) { | ||||
| 		if (check_label("blif", "(if -blif)")) { | ||||
| 			if (!blif_file.empty() || help_mode) { | ||||
| 				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) { | ||||
| 				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; | ||||
|  |  | |||
|  | @ -1,6 +1,6 @@ | |||
| read_verilog ../common/add_sub.v | ||||
| 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) | ||||
| cd top # Constrain all select calls below inside the top module | ||||
| select -assert-count 2 t:LUT2 | ||||
|  |  | |||
|  | @ -3,7 +3,7 @@ design -save read | |||
| 
 | ||||
| hierarchy -top adff | ||||
| 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) | ||||
| cd adff # Constrain all select calls below inside the top module | ||||
| 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 | ||||
| hierarchy -top adffn | ||||
| 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) | ||||
| cd adffn # Constrain all select calls below inside the top module | ||||
| 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 | ||||
| hierarchy -top dffs | ||||
| 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) | ||||
| cd dffs # Constrain all select calls below inside the top module | ||||
| 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 | ||||
| hierarchy -top ndffnr | ||||
| 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) | ||||
| cd ndffnr # Constrain all select calls below inside the top module | ||||
| select -assert-count 1 t:LUT1 | ||||
|  |  | |||
|  | @ -2,7 +2,7 @@ read_verilog ../common/counter.v | |||
| hierarchy -top top | ||||
| proc | ||||
| 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) | ||||
| cd top # Constrain all select calls below inside the top module | ||||
| select -assert-count 1 t:LUT1 | ||||
|  |  | |||
|  | @ -5,7 +5,7 @@ design -save read | |||
| 
 | ||||
| hierarchy -top my_dff | ||||
| 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) | ||||
| cd my_dff # Constrain all select calls below inside the top module | ||||
| 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 | ||||
| hierarchy -top my_dffe | ||||
| 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) | ||||
| cd my_dffe # Constrain all select calls below inside the top module | ||||
| 
 | ||||
|  |  | |||
|  | @ -3,7 +3,7 @@ hierarchy -top fsm | |||
| proc | ||||
| 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 | ||||
| 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 | ||||
|  |  | |||
|  | @ -1,7 +1,7 @@ | |||
| read_verilog ../common/logic.v | ||||
| hierarchy -top top | ||||
| 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) | ||||
| cd top # Constrain all select calls below inside the top module | ||||
| 
 | ||||
|  |  | |||
|  | @ -3,7 +3,7 @@ design -save read | |||
| 
 | ||||
| hierarchy -top mux2 | ||||
| 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) | ||||
| cd mux2 # Constrain all select calls below inside the top module | ||||
| select -assert-count 1 t:LUT3 | ||||
|  | @ -15,7 +15,7 @@ select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D | |||
| design -load read | ||||
| hierarchy -top mux4 | ||||
| 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) | ||||
| cd mux4 # Constrain all select calls below inside the top module | ||||
| select -assert-count 3 t:LUT3 | ||||
|  | @ -27,7 +27,7 @@ select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D | |||
| design -load read | ||||
| hierarchy -top mux8 | ||||
| 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) | ||||
| cd mux8 # Constrain all select calls below inside the top module | ||||
| 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 | ||||
| hierarchy -top mux16 | ||||
| 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) | ||||
| cd mux16 # Constrain all select calls below inside the top module | ||||
| select -assert-count 1 t:LUT3 | ||||
|  |  | |||
|  | @ -4,7 +4,7 @@ proc | |||
| tribuf | ||||
| flatten | ||||
| 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) | ||||
| cd tristate # Constrain all select calls below inside the top module | ||||
| select -assert-count 2 t:inpad | ||||
|  |  | |||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue