mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	Added BTOR backend README file
This commit is contained in:
		
							parent
							
								
									f6e6e9b844
								
							
						
					
					
						commit
						583636f0ad
					
				
					 2 changed files with 24 additions and 1 deletions
				
			
		
							
								
								
									
										23
									
								
								backends/btor/README
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										23
									
								
								backends/btor/README
									
										
									
									
									
										Normal file
									
								
							| 
						 | 
				
			
			@ -0,0 +1,23 @@
 | 
			
		|||
 | 
			
		||||
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
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -960,7 +960,7 @@ struct BtorBackend : public Backend {
 | 
			
		|||
				continue;
 | 
			
		||||
 | 
			
		||||
			if (module->processes.size() != 0)
 | 
			
		||||
				log_error("Found unmapped processes in module %s: unmapped processes are not supported in BLIF backend!\n", RTLIL::id2cstr(module->name));
 | 
			
		||||
				log_error("Found unmapped processes in module %s: unmapped processes are not supported in BTOR backend!\n", RTLIL::id2cstr(module->name));
 | 
			
		||||
 | 
			
		||||
			if (module->name == RTLIL::escape_id(top_module_name)) {
 | 
			
		||||
				BtorDumper::dump(f, module, design, config);
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue