mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-11-04 13:29:12 +00:00 
			
		
		
		
	
		
			
				
	
	
		
			23 lines
		
	
	
	
		
			550 B
		
	
	
	
		
			Text
		
	
	
	
	
	
			
		
		
	
	
			23 lines
		
	
	
	
		
			550 B
		
	
	
	
		
			Text
		
	
	
	
	
	
 | 
						|
This is the Yosys BTOR backend.
 | 
						|
It is developed by Ahmed Irfan <irfan@fbk.eu> - Fondazione Bruno Kessler, Trento, Italy
 | 
						|
 | 
						|
Master git repository for the BTOR backend:
 | 
						|
https://github.com/ahmedirfan1983/yosys/tree/btor
 | 
						|
 | 
						|
 | 
						|
[[CITE]] BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking 
 | 
						|
Johannes Kepler University, Linz, Austria
 | 
						|
http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf
 | 
						|
 | 
						|
 | 
						|
Todos:
 | 
						|
------
 | 
						|
 | 
						|
- Add checks for unsupported stuff
 | 
						|
    - unsupported cell types
 | 
						|
    - async resets
 | 
						|
    - etc..
 | 
						|
 | 
						|
- Add support for $pmux and $lut cells
 | 
						|
 |