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 |
Clifford Wolf
|
99957a825f
|
Added -all and -max options to sat_solve
|
2013-06-08 12:17:30 +02:00 |
Clifford Wolf
|
c681c17038
|
Improved auto-detection of -show signals in sat_solve
|
2013-06-08 09:34:36 +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 |