87 commits

Author	SHA1	Message	Date
Clifford Wolf	3b52121d32	now ignore init attributes on non-register wires in sat command	2014-07-05 11:18:38 +02:00
Johann Glaser	278085fa01	added log_header to miter and expose pass, show cell type for exposed ports	2014-05-28 18:05:38 +02:00
Clifford Wolf	34e54cda5b	Small improvement in SAT log messages	2014-03-13 13:12:49 +01:00
Clifford Wolf	e3b11ea2d6	Fixed bug in freduce command	2014-03-07 18:44:23 +01:00
Clifford Wolf	6f8865d81a	Some minor code cleanups in freduce command	2014-03-07 18:29:04 +01:00
Clifford Wolf	54d74cf616	Added freduce -dump	2014-03-06 22:06:58 +01:00
Clifford Wolf	da5859a674	Added freduce -stop	2014-03-06 18:14:26 +01:00
Clifford Wolf	96e753041d	fixed freduce for Minisat::SimpSolver: use frozen_literal()	2014-03-03 02:14:27 +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	38469e7686	Various improvements in expose command (added -sep and -cut)	2014-02-09 11:07:46 +01:00
Clifford Wolf	85914c36e5	Fixed handling of async reset in expose -evert-dff	2014-02-08 21:26:40 +01:00
Clifford Wolf	0935e20003	Implemented expose -evert-dff	2014-02-08 21:08:38 +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	c526e56747	Added expose -dff	2014-02-06 15:48:42 +01:00
Clifford Wolf	eb8fd4a163	Added miter -make_outcmp	2014-02-06 02:20:55 +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	cd06055e77	Added expose command	2014-02-05 23:59:55 +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	f4f0bd6eef	Fixed a bug in miter command	2014-02-01 22:53:27 +01:00
Clifford Wolf	374674aff4	Added sat -show-inputs and -show-outputs	2014-02-01 22:52:44 +01:00
Clifford Wolf	fa92722358	Added miter command	2014-02-01 10:35:56 +01:00
Clifford Wolf	03a876c7e8	Added sat -tempinduc and sat -prove-asserts	2014-01-19 16:35:17 +01:00
Clifford Wolf	bc541b47ea	Improved performance of freduce input cone reduction	2014-01-04 13:10:51 +01:00
Clifford Wolf	b791af174e	Improved freduce performance on const signals	2014-01-04 00:06:36 +01:00
Clifford Wolf	10f45b8c8e	Performance improvements in freduce pass	2014-01-03 21:29:28 +01:00
Clifford Wolf	c44e1bec6d	More freduce cleanups	2014-01-03 18:17:28 +01:00
Clifford Wolf	03f0ab9de2	Cleanups in freduce command	2014-01-03 17:50:39 +01:00
Clifford Wolf	bf5e5429c1	Use selection in freduce command	2014-01-03 13:15:11 +01:00
Clifford Wolf	c3e9f0712f	Another small freduce cleanup/bugfix	2014-01-03 12:34:18 +01:00
Clifford Wolf	67d155078d	More freduce cleanups and bugfixes	2014-01-03 02:44:05 +01:00
Clifford Wolf	536e20bde1	Fixed more complex undef cases in freduce	2014-01-02 23:40:20 +01:00
Clifford Wolf	0759c97748	More "freduce" related fixes and improvements	2014-01-02 19:37:34 +01:00
Clifford Wolf	c6b33f81eb	Some cleanups in freduce -inv mode (and switched from -noinv to -inv)	2014-01-02 18:11:01 +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	5de57e9970	Fixed compiler warining in passes/sat/eval.cc	2013-12-07 16:19:24 +01:00
Clifford Wolf	325b764341	Added eval -set-undef and eval -table	2013-12-07 11:58:22 +01:00