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
|
c54d1f2ad1
|
Bugfix in satgen for cells with wider in- than outputs.
|
2014-07-21 12:03:41 +02:00 |
Clifford Wolf
|
94c1307c26
|
Added libs/minisat (copy of minisat git master)
|
2014-03-12 10:17:51 +01:00 |
Clifford Wolf
|
97710ffad5
|
Fixed use of frozen literals in SatGen
|
2014-03-06 13:08:44 +01:00 |
Clifford Wolf
|
a1bfde8c5e
|
Strictly zero-extend unsigned A-inputs of shift operations
|
2014-03-06 11:53:37 +01:00 |
Clifford Wolf
|
aaaa604853
|
Added support for $bu0 to SatGen
|
2014-02-26 21:31:34 +01:00 |
Clifford Wolf
|
dab1612f81
|
Added support for Minisat::SimpSolver + ezSAT frezze() API
|
2014-02-23 01:35:59 +01:00 |
Clifford Wolf
|
fc3b3c4ec3
|
Added $slice and $concat cell types
|
2014-02-07 17:44:57 +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
|
c36bac0e10
|
Added $assert support to satgen
|
2014-01-19 15:37:56 +01:00 |
Clifford Wolf
|
7354a1718e
|
Fixed SAT and ConstEval undef handling for $pmux and $safe_pmux
|
2014-01-03 17:30:50 +01:00 |
Clifford Wolf
|
1f80557ade
|
Added SAT undef model for $pmux and $safe_pmux
|
2014-01-02 19:58:59 +01:00 |
Clifford Wolf
|
249ef8695a
|
Major rewrite of "freduce" command
|
2014-01-02 16:52:33 +01:00 |
Clifford Wolf
|
bf607df6d5
|
Fixed undef extend for bitwise binary ops (bugs in simplemap and satgen)
|
2013-12-29 17:39:49 +01:00 |
Clifford Wolf
|
122b3c067b
|
Fixed sat handling of $eqx and $nex with unequal port widths
|
2013-12-27 18:11:05 +01:00 |
Clifford Wolf
|
0f5ab7649e
|
Small cleanup in SatGen
|
2013-12-27 15:18:14 +01:00 |
Clifford Wolf
|
ebf9abfeb6
|
Fixed sat handling of $eqx and $nex cells
|
2013-12-27 14:32:42 +01:00 |
Clifford Wolf
|
369bf81a70
|
Added support for non-const === and !== (for miter circuits)
|
2013-12-27 14:20:15 +01:00 |
Clifford Wolf
|
8a815ac741
|
Added "sat" undef support and "sat -set-init" options
|
2013-12-07 17:28:51 +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
|
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 |