rafaeltp 
								
							 
						 
						
							
							
							
							
								
							
							
								609f46eeb7 
								
							 
						 
						
							
							
								
								adding offset info to memories  
							
							
							
						 
						
							2018-10-18 16:20:21 -07:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								f4ad05e133 
								
							 
						 
						
							
							
								
								Merge pull request  #663  from aman-goel/master  
							
							... 
							
							
							
							Update to .smv backend 
							
						 
						
							2018-10-17 12:18:57 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Aman Goel 
								
							 
						 
						
							
							
							
							
								
							
							
								749b3ed62a 
								
							 
						 
						
							
							
								
								Minor update  
							
							
							
						 
						
							2018-10-15 13:54:12 -04:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								115ca57647 
								
							 
						 
						
							
							
								
								Add "write_edif -attrprop"  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-10-05 09:41:30 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Aman Goel 
								
							 
						 
						
							
							
							
							
								
							
							
								90e0938f9a 
								
							 
						 
						
							
							
								
								Update to .smv backend  
							
							... 
							
							
							
							Splitting VAR and ASSIGN into IVAR, VAR, DEFINE and ASSIGN. This allows better handling by nuXmv for post-processing (since now only state variables are listed under VAR). 
							
						 
						
							2018-10-01 19:03:10 -04:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Miodrag Milanovic 
								
							 
						 
						
							
							
							
							
								
							
							
								41affeeeb9 
								
							 
						 
						
							
							
								
								added prefix to FDirection constants, fixing windows build  
							
							
							
						 
						
							2018-09-21 20:43:49 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									acw1251 
								
							 
						 
						
							
							
							
							
								
							
							
								efac8a45a6 
								
							 
						 
						
							
							
								
								Fixed typo in "verilog_write" help message  
							
							
							
						 
						
							2018-09-18 13:34:30 -04:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								12440fcc8f 
								
							 
						 
						
							
							
								
								Add $lut support to Verilog back-end  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-09-06 00:18:01 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Jim Lawson 
								
							 
						 
						
							
							
							
							
								
							
							
								380c6f0e97 
								
							 
						 
						
							
							
								
								Remove unused functions.  
							
							
							
						 
						
							2018-08-27 10:18:33 -07:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Jim Lawson 
								
							 
						 
						
							
							
							
							
								
							
							
								93d19dc2fb 
								
							 
						 
						
							
							
								
								Add support for module instances.  
							
							... 
							
							
							
							Don't pad logical operands to one bit.
Use operand width and signedness in $reduce_bool.
Shift amounts are unsigned and shouldn't be padded.
Group "is invalid" with the wire declaration, not its use (otherwise it is incorrectly wired to 0). 
							
						 
						
							2018-08-23 14:35:11 -07:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								67b1026297 
								
							 
						 
						
							
							
								
								Merge pull request  #591  from hzeller/virtual-override  
							
							... 
							
							
							
							Consistent use of 'override' for virtual methods in derived classes. 
							
						 
						
							2018-08-15 14:05:38 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								dfc0c8ffc8 
								
							 
						 
						
							
							
								
								Merge pull request  #576  from cr1901/no-resource  
							
							... 
							
							
							
							Gate POSIX-only signals and resource module to only run on POSIX Pyth… 
							
						 
						
							2018-08-15 14:00:19 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								1dd156f516 
								
							 
						 
						
							
							
								
								Fix use of signed integers in JSON back-end  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-08-14 23:31:25 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									jpathy 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								7db05b2cc1 
								
							 
						 
						
							
							
								
								Use realpath  
							
							... 
							
							
							
							Use `os.path.realpath` instead to make sure symlinks are followed. This is also required to work for nix package manager. 
							
						 
						
							2018-08-06 06:51:07 +00:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Henner Zeller 
								
							 
						 
						
							
							
							
							
								
							
							
								3aa4484a3c 
								
							 
						 
						
							
							
								
								Consistent use of 'override' for virtual methods in derived classes.  
							
							... 
							
							
							
							o Not all derived methods were marked 'override', but it is a great
  feature of C++11 that we should make use of.
o While at it: touched header files got a -*- c++ -*- for emacs to
  provide support for that language.
o use YS_OVERRIDE for all override keywords (though we should probably
  use the plain keyword going forward now that C++11 is established) 
							
						 
						
							2018-07-20 23:51:06 -07:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									William D. Jones 
								
							 
						 
						
							
							
							
							
								
							
							
								0caa62802c 
								
							 
						 
						
							
							
								
								Gate POSIX-only signals and resource module to only run on POSIX Python implementations.  
							
							
							
						 
						
							2018-07-06 01:44:34 -04:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Sergiusz Bazanski 
								
							 
						 
						
							
							
							
							
								
							
							
								1690dafde1 
								
							 
						 
						
							
							
								
								Fix protobuf build  
							
							
							
						 
						
							2018-06-20 19:28:43 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Serge Bazanski 
								
							 
						 
						
							
							
							
							
								
							
							
								53e9a1549c 
								
							 
						 
						
							
							
								
								Add Protobuf backend  
							
							... 
							
							
							
							Signed-off-by: Serge Bazanski <q3k@symbioticeda.com> 
							
						 
						
							2018-06-19 13:34:56 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								d9a2b43014 
								
							 
						 
						
							
							
								
								Add $dlatch support to write_verilog  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-04-22 16:03:26 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								5ca91ca019 
								
							 
						 
						
							
							
								
								Add "write_blif -inames -iattr"  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-04-15 14:07:21 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								4d6af2969c 
								
							 
						 
						
							
							
								
								Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-04-04 18:12:27 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								25a864fc73 
								
							 
						 
						
							
							
								
								Fixed -stbv handling in SMT2 back-end  
							
							
							
						 
						
							2018-04-04 17:28:07 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								dd5fab69c1 
								
							 
						 
						
							
							
								
								Add smtio status msgs when --progress is inactive  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-29 21:59:30 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								a48c7e5abf 
								
							 
						 
						
							
							
								
								Bugfix in smtio.py VCD file generator  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-29 12:45:31 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								77bd645c35 
								
							 
						 
						
							
							
								
								Add $mem support to SMT2 clock tagging  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-27 02:11:20 +02:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								3f00702475 
								
							 
						 
						
							
							
								
								Improve yosys-smtbmc log output and error handling  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-17 18:06:17 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								4d4e3a8ca6 
								
							 
						 
						
							
							
								
								Improve handling of invalid check-sat result in smtio.py  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-17 12:17:53 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								3545c0fffb 
								
							 
						 
						
							
							
								
								Remove debug prints from yosys-smtbmc VCD writer  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-08 16:24:35 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								8b604004da 
								
							 
						 
						
							
							
								
								Check results of (check-sat) in yosys-smtbmc  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-07 22:54:19 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								cedbc35f4b 
								
							 
						 
						
							
							
								
								Imporove yosys-smtbmc error handling, Improve VCD output  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-05 12:17:22 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								8b7602e660 
								
							 
						 
						
							
							
								
								Improve SMT2 encoding of $reduce_{and,or,bool}  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-04 21:22:20 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								45a6fce92c 
								
							 
						 
						
							
							
								
								Fix a hangup in yosys-smtbmc error handling  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-04 21:13:30 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								ae4e204c76 
								
							 
						 
						
							
							
								
								Improved error handling in yosys-smtbmc  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-03 20:00:07 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								a44e1edaa3 
								
							 
						 
						
							
							
								
								Terminate running SMT solver when smtbmc is terminated  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-03 14:50:40 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								3ced2cca6e 
								
							 
						 
						
							
							
								
								Fix smtbmc smtc/aiw parser for wire names containing []  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-03 14:15:49 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								90ae426078 
								
							 
						 
						
							
							
								
								Mangle names with square brackets in VCD files to work around issues in gtkwave  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-01 14:15:27 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								675dd5347a 
								
							 
						 
						
							
							
								
								Small fixes and improvements in $allconst/$allseq handling  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-02-26 11:58:44 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								b13e6bd375 
								
							 
						 
						
							
							
								
								Add smtbmc support for exist-forall problems  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-02-23 19:33:30 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								17583b6a21 
								
							 
						 
						
							
							
								
								Add support for mockup clock signals in yosys-smtbmc vcd output  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-02-20 17:45:22 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								c9672e2e2e 
								
							 
						 
						
							
							
								
								Fix handling of zero-length cell connections in SMT2 back-end  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-02-08 19:12:12 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								e4f0218907 
								
							 
						 
						
							
							
								
								Fixed gcc 7.2 "statement will never be executed" warning  
							
							
							
						 
						
							2018-02-03 14:31:47 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								e97f10b142 
								
							 
						 
						
							
							
								
								Fix smtio.py for large SMT2 S-expressions  
							
							
							
						 
						
							2018-01-29 12:34:28 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								54aeca0983 
								
							 
						 
						
							
							
								
								Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output  
							
							
							
						 
						
							2018-01-18 14:25:22 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								9804ebedbf 
								
							 
						 
						
							
							
								
								Add "no driver for signal bit" error msg to btor back-end  
							
							
							
						 
						
							2017-12-24 17:30:36 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								292984896b 
								
							 
						 
						
							
							
								
								Simple fix BTOR memory encoding  
							
							
							
						 
						
							2017-12-17 18:57:54 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								bbdcc1f9d4 
								
							 
						 
						
							
							
								
								Improve BTOR memory encoding  
							
							
							
						 
						
							2017-12-17 18:55:17 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								30f23281ed 
								
							 
						 
						
							
							
								
								Add array support to btor back-end  
							
							
							
						 
						
							2017-12-15 02:19:06 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								ad901671c5 
								
							 
						 
						
							
							
								
								Add $anyconst/$anyseq support to btor back-end  
							
							
							
						 
						
							2017-12-15 00:40:24 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								162c29bd6b 
								
							 
						 
						
							
							
								
								Merge branch 'master' into btor-ng  
							
							
							
						 
						
							2017-12-14 03:13:47 +01:00 
							
								 
							
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								9419de3e37 
								
							 
						 
						
							
							
								
								Add yosys-smtbmc VCD writer support for memories with async writes  
							
							
							
						 
						
							2017-12-14 03:06:00 +01:00