54 commits

Author	SHA1	Message	Date
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
Clifford Wolf	bc3cc88719	Started implementing undef support in "sat" command	2013-11-25 21:40:00 +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	223892ac28	Improved user-friendliness of "sat" and "eval" expression parsing	2013-11-09 12:02:27 +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	f485962c5e	Added handling of unconnected/unspecified signals to eval -vloghammer_report	2013-11-06 22:42:07 +01:00
Clifford Wolf	031a91dc94	Added correct RTL undef handling to eval vloghammer mode	2013-11-06 13:16:47 +01:00
Clifford Wolf	f94266bb42	Added eval -vloghammer_report mode	2013-11-06 04:14:56 +01:00
Clifford Wolf	2f3da54f26	Added sat -ignore_div_by_zero switch	2013-08-15 11:40:01 +02:00
Clifford Wolf	d0e93e04d1	Added eval -brute_force_equiv_checker_x mode	2013-08-15 11:09:30 +02:00
Clifford Wolf	6068b8902f	freduce performance fix	2013-08-10 15:03:13 +02:00
Clifford Wolf	6a40e46a04	Added -try option to freduce pass	2013-08-08 10:56:27 +02:00
Clifford Wolf	56e01ce389	Fixed topological ordering in freduce pass	2013-08-07 19:38:19 +02:00
Clifford Wolf	653750faac	Small bugfixes in freduce pass	2013-08-06 15:53:09 +02:00
Clifford Wolf	6efca9ea5a	Added freduce command	2013-08-06 15:04:52 +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
Clifford Wolf	a75b249427	Implemented temporal induction proofs in sat_solve	2013-06-09 18:07:05 +02:00
Clifford Wolf	b210234612	Added support for non-temporal proofs to sat_solve	2013-06-09 16:30:37 +02:00
Clifford Wolf	1349b845e3	Re-organization in sat_solver pass for temporal induction	2013-06-09 15:49:32 +02:00
Clifford Wolf	41932e8b64	Added ezSAT api support for don't care values in models	2013-06-09 14:21:18 +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	4b7f070b69	Fixed typo is sat_solve help msg	2013-06-08 15:36:32 +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