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 |