mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-10-27 01:39:23 +00:00 
			
		
		
		
	Update tests
This commit is contained in:
		
							parent
							
								
									262ad03cd3
								
							
						
					
					
						commit
						3848563600
					
				
					 10 changed files with 25 additions and 25 deletions
				
			
		|  | @ -1,7 +1,7 @@ | |||
| read_verilog ../common/add_sub.v | ||||
| hierarchy -top top | ||||
| proc | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad | ||||
| opt -full | ||||
| 
 | ||||
| miter -equiv -flatten -make_assert -make_outputs gold gate miter | ||||
|  | @ -30,7 +30,7 @@ EOT | |||
| 
 | ||||
| hierarchy -top top | ||||
| proc | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad | ||||
| opt -full | ||||
| 
 | ||||
| miter -equiv -flatten -make_assert -make_outputs gold gate miter | ||||
|  | @ -58,7 +58,7 @@ EOT | |||
| 
 | ||||
| hierarchy -top top | ||||
| proc | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad | ||||
| opt -full | ||||
| 
 | ||||
| miter -equiv -flatten -make_assert -make_outputs gold gate miter | ||||
|  |  | |||
|  | @ -3,7 +3,7 @@ design -save read | |||
| 
 | ||||
| hierarchy -top adff | ||||
| proc | ||||
| equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore # equivalency check | ||||
| equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # 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:NX_DFF | ||||
|  | @ -14,7 +14,7 @@ select -assert-none t:NX_DFF %% t:* %D | |||
| design -load read | ||||
| hierarchy -top adffn | ||||
| proc | ||||
| equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore # equivalency check | ||||
| equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # 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:NX_DFF | ||||
|  | @ -26,7 +26,7 @@ select -assert-none t:NX_DFF t:NX_LUT %% t:* %D | |||
| design -load read | ||||
| hierarchy -top dffs | ||||
| proc | ||||
| equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore # equivalency check | ||||
| equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # 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:NX_DFF | ||||
|  | @ -38,7 +38,7 @@ select -assert-none t:NX_DFF t:NX_LUT %% t:* %D | |||
| design -load read | ||||
| hierarchy -top ndffnr | ||||
| proc | ||||
| equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore # equivalency check | ||||
| equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # 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:NX_DFF | ||||
|  |  | |||
|  | @ -3,7 +3,7 @@ design -save read | |||
| 
 | ||||
| hierarchy -top dff | ||||
| proc | ||||
| equiv_opt -assert -async2sync -map +/nanoxplore/cells_sim.v synth_nanoxplore # equivalency check | ||||
| equiv_opt -assert -async2sync -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check | ||||
| design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) | ||||
| cd dff # Constrain all select calls below inside the top module | ||||
| select -assert-count 1 t:NX_DFF | ||||
|  | @ -13,7 +13,7 @@ select -assert-none t:NX_DFF %% t:* %D | |||
| design -load read | ||||
| hierarchy -top dffe | ||||
| proc | ||||
| equiv_opt -assert -async2sync -map +/nanoxplore/cells_sim.v synth_nanoxplore # equivalency check | ||||
| equiv_opt -assert -async2sync -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # equivalency check | ||||
| design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) | ||||
| cd dffe # Constrain all select calls below inside the top module | ||||
| select -assert-count 1 t:NX_DFF | ||||
|  |  | |||
|  | @ -3,7 +3,7 @@ hierarchy -top fsm | |||
| proc | ||||
| flatten | ||||
| 
 | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v synth_nanoxplore | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad | ||||
| 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 | ||||
|  |  | |||
|  | @ -4,7 +4,7 @@ design -save read | |||
| hierarchy -top latchp | ||||
| proc | ||||
| # Can't run any sort of equivalence check because latches are blown to LUTs | ||||
| synth_nanoxplore | ||||
| synth_nanoxplore -noiopad | ||||
| cd latchp # Constrain all select calls below inside the top module | ||||
| select -assert-count 1 t:NX_LUT | ||||
| 
 | ||||
|  | @ -15,7 +15,7 @@ design -load read | |||
| hierarchy -top latchn | ||||
| proc | ||||
| # Can't run any sort of equivalence check because latches are blown to LUTs | ||||
| synth_nanoxplore | ||||
| synth_nanoxplore -noiopad | ||||
| cd latchn # Constrain all select calls below inside the top module | ||||
| select -assert-count 1 t:NX_LUT | ||||
| 
 | ||||
|  | @ -26,7 +26,7 @@ design -load read | |||
| hierarchy -top latchsr | ||||
| proc | ||||
| # Can't run any sort of equivalence check because latches are blown to LUTs | ||||
| synth_nanoxplore | ||||
| synth_nanoxplore -noiopad | ||||
| cd latchsr # Constrain all select calls below inside the top module | ||||
| select -assert-count 2 t:NX_LUT | ||||
| 
 | ||||
|  |  | |||
|  | @ -1,7 +1,7 @@ | |||
| read_verilog ../common/logic.v | ||||
| hierarchy -top top | ||||
| proc | ||||
| equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore # equivalency check | ||||
| equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # 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 | ||||
| 
 | ||||
|  |  | |||
|  | @ -26,7 +26,7 @@ EOT | |||
| hierarchy -top lutram_dpreg | ||||
| proc | ||||
| memory -nomap | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad | ||||
| memory | ||||
| opt -full | ||||
| 
 | ||||
|  | @ -48,7 +48,7 @@ read_verilog ../common/lutram.v | |||
| hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 18 | ||||
| proc | ||||
| memory -nomap | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad | ||||
| memory | ||||
| opt -full | ||||
| 
 | ||||
|  | @ -68,7 +68,7 @@ read_verilog ../common/lutram.v | |||
| hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 18 | ||||
| proc | ||||
| memory -nomap | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad | ||||
| memory | ||||
| opt -full | ||||
| 
 | ||||
|  | @ -88,7 +88,7 @@ read_verilog ../common/lutram.v | |||
| hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 36 | ||||
| proc | ||||
| memory -nomap | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad | ||||
| memory | ||||
| opt -full | ||||
| 
 | ||||
|  | @ -131,7 +131,7 @@ EOT | |||
| hierarchy -top lutram_1w2r -chparam A_WIDTH 5 -chparam D_WIDTH 18 | ||||
| proc | ||||
| memory -nomap | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore | ||||
| equiv_opt -run :prove -map +/nanoxplore/cells_sim.v -map +/nanoxplore/cells_sim_u.v synth_nanoxplore -noiopad | ||||
| memory | ||||
| opt -full | ||||
| 
 | ||||
|  |  | |||
|  | @ -3,7 +3,7 @@ design -save read | |||
| 
 | ||||
| hierarchy -top mux2 | ||||
| proc | ||||
| equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore # equivalency check | ||||
| equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # 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:NX_LUT | ||||
|  | @ -13,7 +13,7 @@ select -assert-none t:NX_LUT %% t:* %D | |||
| design -load read | ||||
| hierarchy -top mux4 | ||||
| proc | ||||
| equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore # equivalency check | ||||
| equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # 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 2 t:NX_LUT | ||||
|  | @ -23,7 +23,7 @@ select -assert-none t:NX_LUT %% t:* %D | |||
| design -load read | ||||
| hierarchy -top mux8 | ||||
| proc | ||||
| equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore # equivalency check | ||||
| equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # 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 5 t:NX_LUT | ||||
|  | @ -33,7 +33,7 @@ select -assert-none t:NX_LUT %% t:* %D | |||
| design -load read | ||||
| hierarchy -top mux16 | ||||
| proc | ||||
| equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore # equivalency check | ||||
| equiv_opt -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # 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-max 13 t:NX_LUT | ||||
|  |  | |||
|  | @ -2,7 +2,7 @@ read_verilog ../common/shifter.v | |||
| hierarchy -top top | ||||
| proc | ||||
| flatten | ||||
| equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore # equivalency check | ||||
| equiv_opt -async2sync -assert -map +/nanoxplore/cells_sim.v synth_nanoxplore -noiopad # 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 | ||||
| 
 | ||||
|  |  | |||
|  | @ -4,7 +4,7 @@ proc | |||
| tribuf | ||||
| flatten | ||||
| synth | ||||
| equiv_opt -assert -map +/nanoxplore/cells_sim.v -map +/simcells.v synth_nanoxplore -iopad # equivalency check | ||||
| equiv_opt -assert -map +/nanoxplore/cells_sim.v -map +/simcells.v synth_nanoxplore # 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 | ||||
| #Internal cell type used. Need support it. | ||||
|  |  | |||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue