| 
								
								
									 Clifford Wolf | cdae8abe16 | Renamed port access function on RTLIL::Cell, added param access functions | 2014-07-31 16:38:54 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 3f0a5746ef | Using native ezSAT shift ops in satgen, fixed $shift and $shiftx SAT models | 2014-07-30 18:37:17 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 397b00252d | Added $shift and $shiftx cell types (needed for correct part select behavior) | 2014-07-29 16:35:13 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 7bd2d1064f | Using log_assert() instead of assert() | 2014-07-28 11:27:48 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | b7dda72302 | Changed users of cell->connections_ to the new API (sed command) git grep -l 'connections_' | xargs sed -i -r -e '
	s/(->|\.)connections_\["([^"]*)"\] = (.*);/\1set("\2", \3);/g;
	s/(->|\.)connections_\["([^"]*)"\]/\1get("\2")/g;
	s/(->|\.)connections_.at\("([^"]*)"\)/\1get("\2")/g;
	s/(->|\.)connections_.push_back/\1connect/g;
	s/(->|\.)connections_/\1connections()/g;' | 2014-07-26 15:58:23 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | cc4f10883b | Renamed RTLIL::{Module,Cell}::connections to connections_ | 2014-07-26 11:58:03 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | a62c21c9c6 | Removed RTLIL::SigSpec::expand() method | 2014-07-23 19:34:51 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 4b4048bc5f | SigSpec refactoring: using the accessor functions everywhere | 2014-07-22 20:39:37 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | a233762a81 | SigSpec refactoring: renamed chunks and width to __chunks and __width | 2014-07-22 20:39:37 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | c54d1f2ad1 | Bugfix in satgen for cells with wider in- than outputs. | 2014-07-21 12:03:41 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 94c1307c26 | Added libs/minisat (copy of minisat git master) | 2014-03-12 10:17:51 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 97710ffad5 | Fixed use of frozen literals in SatGen | 2014-03-06 13:08:44 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | a1bfde8c5e | Strictly zero-extend unsigned A-inputs of shift operations | 2014-03-06 11:53:37 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | aaaa604853 | Added support for $bu0 to SatGen | 2014-02-26 21:31:34 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | dab1612f81 | Added support for Minisat::SimpSolver + ezSAT frezze() API | 2014-02-23 01:35:59 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | fc3b3c4ec3 | Added $slice and $concat cell types | 2014-02-07 17:44:57 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | d267bcde4e | Fixed bug in sequential sat proofs and improved handling of asserts | 2014-02-04 12:46:16 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | c36bac0e10 | Added $assert support to satgen | 2014-01-19 15:37:56 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 7354a1718e | Fixed SAT and ConstEval undef handling for $pmux and $safe_pmux | 2014-01-03 17:30:50 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 1f80557ade | Added SAT undef model for $pmux and $safe_pmux | 2014-01-02 19:58:59 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 249ef8695a | Major rewrite of "freduce" command | 2014-01-02 16:52:33 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | bf607df6d5 | Fixed undef extend for bitwise binary ops (bugs in simplemap and satgen) | 2013-12-29 17:39:49 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 122b3c067b | Fixed sat handling of $eqx and $nex with unequal port widths | 2013-12-27 18:11:05 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 0f5ab7649e | Small cleanup in SatGen | 2013-12-27 15:18:14 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | ebf9abfeb6 | Fixed sat handling of $eqx and $nex cells | 2013-12-27 14:32:42 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 369bf81a70 | Added support for non-const === and !== (for miter circuits) | 2013-12-27 14:20:15 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 8a815ac741 | Added "sat" undef support and "sat -set-init" options | 2013-12-07 17:28:51 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 61412d167f | Improvements in satgen undef handling | 2013-11-25 16:50:45 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | bd65e67d8a | Improvements in satgen undef handling | 2013-11-25 15:12:01 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 8c3f4b3957 | Started implementing undef handling in satgen | 2013-11-25 04:51:33 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 18f9477e95 | Added verification of SAT model to "eval -vloghammer_report" command | 2013-11-09 11:38:17 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 6fcbc79b5c | Improved width extension with regard to undef propagation | 2013-11-06 21:05:11 +01:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | a860efa8ac | Implemented same div-by-zero behavior as found in other synthesis tools | 2013-08-15 21:00:06 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 2f3da54f26 | Added sat -ignore_div_by_zero switch | 2013-08-15 11:40:01 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | ccf36cb7d8 | Added SAT support for $div and $mod cells | 2013-08-11 16:27:15 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 7daeee340a | Fixed shift ops with large right hand side | 2013-07-09 18:59:59 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 0c6ffc4c65 | More fixes for bugs found using xsthammer | 2013-06-13 11:18:45 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | bf2c149329 | Another fix for a bug found using xsthammer | 2013-06-12 19:09:14 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | a5c30183b5 | Sign-extension related fixes in SatGen and AST frontend | 2013-06-10 17:10:06 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 7d790febb0 | Improvements and fixes in SAT code | 2013-06-10 16:09:29 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | a75b249427 | Implemented temporal induction proofs in sat_solve | 2013-06-09 18:07:05 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | b7ba90910d | Fixed handling of $_XOR_ in SAT generator | 2013-06-09 14:01:50 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 0efde13775 | Added sequential solving support to sat_solve | 2013-06-09 13:35:46 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 23a7973094 | Added support for shifter cells to SAT generator | 2013-06-08 15:12:08 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 1434312fdd | Various improvements in sat_solve pass and SAT generator | 2013-06-08 14:11:50 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 56b593b91c | Improved sat generator and sat_solve pass | 2013-06-07 14:37:33 +02:00 |  | 
				
					
						| 
								
								
									 Clifford Wolf | 46fbe9d262 | Added SAT generator and simple sat_solve command | 2013-06-07 13:59:13 +02:00 |  |