38 commits

Author	SHA1	Message	Date
Clifford Wolf	c094c53de8	Removed RTLIL::SigSpec::optimize()	2014-07-23 20:32:28 +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	3b52121d32	now ignore init attributes on non-register wires in sat command	2014-07-05 11:18:38 +02:00
Clifford Wolf	34e54cda5b	Small improvement in SAT log messages	2014-03-13 13:12:49 +01:00
Clifford Wolf	a78bba1f5c	Added "sat -dump_cnf"	2014-02-18 09:29:08 +01:00
Clifford Wolf	32af10fa9b	Coding style corrections in SatHelper::dump_model_to_vcd()	2014-02-18 09:28:05 +01:00
Clifford Wolf	13051e6acf	Added "sat -initsteps"	2014-02-18 09:03:16 +01:00
Clifford Wolf	0851c2b6ea	Renamed "sat -dump_fail_to_vcd" to "sat -dump_vcd" and some minor cleanups	2014-02-17 13:59:39 +01:00
Andrew Zonenberg	4a948d780a	Added "-dump_fail_to_vcd" argument to SAT solver	2014-02-17 13:52:36 +01:00
Clifford Wolf	fa295a4528	Added generic RTLIL::SigSpec::parse_sel() with support for selection variables	2014-02-06 19:22:46 +01:00
Clifford Wolf	d4b0f28881	Added support for sat -show @<sel_name>	2014-02-06 17:32:51 +01:00
Clifford Wolf	b1a12c5f37	Added sat -set-init-def and sat -tempinduct-def	2014-02-06 16:15:23 +01:00
Clifford Wolf	80a1cdb0e2	Added sat -set-init-zero support	2014-02-06 01:40:01 +01:00
Clifford Wolf	e915043144	Added sat -verify and -falsify support for non-prove cases	2014-02-06 00:59:41 +01:00
Clifford Wolf	6891fd79a3	added sat -falsify	2014-02-04 13:34:37 +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	9e35021585	Addred sat option -ignore_unknown_cells	2014-02-03 16:26:10 +01:00
Clifford Wolf	374674aff4	Added sat -show-inputs and -show-outputs	2014-02-01 22:52:44 +01:00
Clifford Wolf	03a876c7e8	Added sat -tempinduc and sat -prove-asserts	2014-01-19 16:35:17 +01:00
Clifford Wolf	249ef8695a	Major rewrite of "freduce" command	2014-01-02 16:52:33 +01:00
Clifford Wolf	7f71787599	Added sat -prove-x and -set-def-inputs	2013-12-28 11:24:36 +01:00
Clifford Wolf	11ffa78677	Added sat -set-def/-set-*-undef support	2013-12-27 13:27:21 +01:00
Clifford Wolf	fb31d10236	Renamed sat -set-undef to -set-any-undef	2013-12-27 13:02:46 +01:00
Clifford Wolf	2b90ba1e96	Added sat -max_undef feature	2013-12-07 23:58:55 +01:00
Clifford Wolf	8a815ac741	Added "sat" undef support and "sat -set-init" options	2013-12-07 17:28:51 +01:00
Clifford Wolf	bc3cc88719	Started implementing undef support in "sat" command	2013-11-25 21:40:00 +01:00
Clifford Wolf	223892ac28	Improved user-friendliness of "sat" and "eval" expression parsing	2013-11-09 12:02:27 +01:00
Clifford Wolf	2f3da54f26	Added sat -ignore_div_by_zero switch	2013-08-15 11:40:01 +02:00
Clifford Wolf	101491132f	Added SAT support for -all/-max with -verify	2013-06-23 13:28:30 +02:00
Clifford Wolf	8fbb5b6240	Added timout functionality to SAT solver	2013-06-20 12:49:10 +02:00
Clifford Wolf	21e38bed98	Added "eval" pass	2013-06-19 09:30:37 +02:00
Clifford Wolf	6d7b5f9064	Fixed even more ConstEval bugs found using xsthammer	2013-06-14 17:50:26 +02:00
Clifford Wolf	30db70b1ba	Added consteval testing to xsthammer and fixed bugs	2013-06-13 19:51:13 +02:00
Clifford Wolf	7f6c83a853	More xsthammer improvements (using xst 14.5 now)	2013-06-13 17:23:51 +02:00
Clifford Wolf	7d790febb0	Improvements and fixes in SAT code	2013-06-10 16:09:29 +02:00
Clifford Wolf	08e2fa978c	Renamed "sat_solve" pass to "sat"	2013-06-09 21:55:53 +02:00

Renamed from passes/sat/sat_solve.cc (Browse further)