mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-10-31 11:42:30 +00:00 
			
		
		
		
	
		
			
				
	
	
		
			23 lines
		
	
	
	
		
			540 B
		
	
	
	
		
			Text
		
	
	
	
	
	
			
		
		
	
	
			23 lines
		
	
	
	
		
			540 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 $lut cells
 | |
| 
 |