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 |
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 |