mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-11-04 13:29:12 +00:00 
			
		
		
		
	fixup! quicklogic: Add basic k6n10f tests
This commit is contained in:
		
							parent
							
								
									6066115d5b
								
							
						
					
					
						commit
						e70122b74e
					
				
					 2 changed files with 11 additions and 33 deletions
				
			
		| 
						 | 
				
			
			@ -3,32 +3,27 @@ design -save read
 | 
			
		|||
 | 
			
		||||
hierarchy -top latchp
 | 
			
		||||
proc
 | 
			
		||||
# Can't run any sort of equivalence check because latches are blown to LUTs
 | 
			
		||||
synth_quicklogic -family qlf_k6n10f
 | 
			
		||||
cd latchp # Constrain all select calls below inside the top module
 | 
			
		||||
equiv_opt -assert -async2sync -map +/quicklogic/qlf_k6n10f/cells_sim.v synth_quicklogic -family qlf_k6n10f
 | 
			
		||||
design -load postopt
 | 
			
		||||
cd latchp
 | 
			
		||||
select -assert-count 1 t:latchsre
 | 
			
		||||
 | 
			
		||||
select -assert-none t:latchsre %% t:* %D
 | 
			
		||||
 | 
			
		||||
 | 
			
		||||
design -load read
 | 
			
		||||
hierarchy -top latchn
 | 
			
		||||
proc
 | 
			
		||||
# Can't run any sort of equivalence check because latches are blown to LUTs
 | 
			
		||||
synth_quicklogic -family qlf_k6n10f
 | 
			
		||||
cd latchn # Constrain all select calls below inside the top module
 | 
			
		||||
equiv_opt -assert -async2sync -map +/quicklogic/qlf_k6n10f/cells_sim.v synth_quicklogic -family qlf_k6n10f
 | 
			
		||||
design -load postopt
 | 
			
		||||
cd latchn
 | 
			
		||||
select -assert-count 1 t:latchnsre
 | 
			
		||||
 | 
			
		||||
select -assert-none t:latchnsre %% t:* %D
 | 
			
		||||
 | 
			
		||||
 | 
			
		||||
design -load read
 | 
			
		||||
hierarchy -top latchsr
 | 
			
		||||
proc
 | 
			
		||||
# Can't run any sort of equivalence check because latches are blown to LUTs
 | 
			
		||||
synth_quicklogic -family qlf_k6n10f
 | 
			
		||||
cd latchsr # Constrain all select calls below inside the top module
 | 
			
		||||
equiv_opt -assert -async2sync -map +/quicklogic/qlf_k6n10f/cells_sim.v synth_quicklogic -family qlf_k6n10f
 | 
			
		||||
design -load postopt
 | 
			
		||||
cd latchsr
 | 
			
		||||
select -assert-count 2 t:$lut
 | 
			
		||||
select -assert-count 1 t:dffsr
 | 
			
		||||
 | 
			
		||||
select -assert-none t:$lut t:dffsr %% t:* %D
 | 
			
		||||
select -assert-count 1 t:latchnsre
 | 
			
		||||
select -assert-none t:$lut t:latchnsre %% t:* %D
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -1,17 +0,0 @@
 | 
			
		|||
read_verilog ../../common/fsm.v
 | 
			
		||||
hierarchy -top fsm
 | 
			
		||||
proc
 | 
			
		||||
flatten
 | 
			
		||||
 | 
			
		||||
synth_quicklogic -family qlf_k6n10f
 | 
			
		||||
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
 | 
			
		||||
 | 
			
		||||
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 9 t:$lut
 | 
			
		||||
select -assert-count 6 t:sdffsre
 | 
			
		||||
 | 
			
		||||
select -assert-none t:$lut t:sdffsre %% t:* %D
 | 
			
		||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue