mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-11-03 21:09:12 +00:00 
			
		
		
		
	write_xaiger: fix for (* keep *) on flop output
This commit is contained in:
		
							parent
							
								
									d4e188299b
								
							
						
					
					
						commit
						cd8f55a911
					
				
					 2 changed files with 18 additions and 3 deletions
				
			
		| 
						 | 
				
			
			@ -14,6 +14,7 @@ design -import gate -as gate
 | 
			
		|||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
			
		||||
sat -verify -prove-asserts -show-ports miter
 | 
			
		||||
 | 
			
		||||
 | 
			
		||||
design -load read
 | 
			
		||||
hierarchy -top abc9_test028
 | 
			
		||||
proc
 | 
			
		||||
| 
						 | 
				
			
			@ -23,6 +24,7 @@ select -assert-count 1 t:$lut r:LUT=2'b01 r:WIDTH=1 %i %i
 | 
			
		|||
select -assert-count 1 t:unknown
 | 
			
		||||
select -assert-none t:$lut t:unknown %% t: %D
 | 
			
		||||
 | 
			
		||||
 | 
			
		||||
design -load read
 | 
			
		||||
hierarchy -top abc9_test032
 | 
			
		||||
proc
 | 
			
		||||
| 
						 | 
				
			
			@ -38,3 +40,16 @@ design -import gate -as gate
 | 
			
		|||
 | 
			
		||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
			
		||||
sat -seq 10 -verify -prove-asserts -show-ports miter
 | 
			
		||||
 | 
			
		||||
 | 
			
		||||
design -reset
 | 
			
		||||
read_verilog -icells <<EOT
 | 
			
		||||
module abc9_test036(input clk, d, output q);
 | 
			
		||||
(* keep *) reg w;
 | 
			
		||||
$__ABC9_FF_ ff(.D(d), .Q(w));
 | 
			
		||||
wire \ff.clock = clk;
 | 
			
		||||
wire \ff.init = 1'b0;
 | 
			
		||||
assign q = w;
 | 
			
		||||
endmodule
 | 
			
		||||
EOT
 | 
			
		||||
abc9 -lut 4 -dff
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue