Clifford Wolf
|
1f1deda888
|
Added non-std verilog assume() statement
|
2015-02-26 18:47:39 +01:00 |
Clifford Wolf
|
39d25b212c
|
Fixed "sat -initsteps" off-by-one bug
|
2015-02-22 12:42:05 +01:00 |
Clifford Wolf
|
fae0e75ace
|
Added "sat -stepsize" and "sat -tempinduct-step"
|
2015-02-21 22:52:49 +01:00 |
Clifford Wolf
|
b19c926af8
|
sat docu change
|
2015-02-21 22:03:54 +01:00 |
Clifford Wolf
|
9237fb924e
|
When "sat -tempinduct-baseonly -maxsteps N" reaches maxsteps it is a good thing.
|
2015-02-21 20:05:16 +01:00 |
Clifford Wolf
|
1688b9b464
|
Added "sat -tempinduct-baseonly -tempinduct-inductonly"
|
2015-02-21 17:53:22 +01:00 |
Clifford Wolf
|
dcbd00c101
|
Fixed basecase init for "sat -tempinduct"
|
2015-02-21 17:43:49 +01:00 |
Clifford Wolf
|
4e6ca7760f
|
Replaced ezDefaultSAT with ezSatPtr
|
2015-02-21 12:15:41 +01:00 |
Clifford Wolf
|
08c0fe164f
|
format fixes in "sat -dump_json"
|
2015-02-19 13:19:04 +01:00 |
Clifford Wolf
|
1ecee6c49c
|
Added "sat -dump_json" (WaveJSON format)
|
2015-02-19 10:53:40 +01:00 |
Clifford Wolf
|
9ebf803cbe
|
Improved an error message
|
2015-01-28 00:46:00 +01:00 |
Clifford Wolf
|
23e54bda81
|
Added "sat -show-ports"
|
2015-01-27 23:04:28 +00:00 |
Clifford Wolf
|
fe829bdbdc
|
Added log_warning() API
|
2014-11-09 10:44:23 +01:00 |
Clifford Wolf
|
4569a747f8
|
Renamed SIZE() to GetSize() because of name collision on Win32
|
2014-10-10 17:07:24 +02:00 |
Clifford Wolf
|
f9a307a50b
|
namespace Yosys
|
2014-09-27 16:17:53 +02:00 |
Ruben Undheim
|
79cbf9067c
|
Corrected spelling mistakes found by lintian
|
2014-09-06 08:47:06 +02:00 |
Clifford Wolf
|
9c5a63c52c
|
azonenberg: Make dump_vcd save model when temporal induction fails due to step limit
|
2014-08-24 13:27:40 +02:00 |
Clifford Wolf
|
622ebab671
|
Added "sat -prove-skip"
|
2014-08-08 13:11:54 +02:00 |
Clifford Wolf
|
b9bd22b8c8
|
More cleanups related to RTLIL::IdString usage
|
2014-08-02 13:19:57 +02:00 |
Clifford Wolf
|
7bd2d1064f
|
Using log_assert() instead of assert()
|
2014-07-28 11:27:48 +02:00 |
Clifford Wolf
|
10e5791c5e
|
Refactoring: Renamed RTLIL::Design::modules to modules_
|
2014-07-27 11:18:30 +02:00 |
Clifford Wolf
|
4c4b602156
|
Refactoring: Renamed RTLIL::Module::cells to cells_
|
2014-07-27 01:51:45 +02:00 |
Clifford Wolf
|
f9946232ad
|
Refactoring: Renamed RTLIL::Module::wires to wires_
|
2014-07-27 01:49:51 +02:00 |
Clifford Wolf
|
b7dda72302
|
Changed users of cell->connections_ to the new API (sed command)
git grep -l 'connections_' | xargs sed -i -r -e '
s/(->|\.)connections_\["([^"]*)"\] = (.*);/\1set("\2", \3);/g;
s/(->|\.)connections_\["([^"]*)"\]/\1get("\2")/g;
s/(->|\.)connections_.at\("([^"]*)"\)/\1get("\2")/g;
s/(->|\.)connections_.push_back/\1connect/g;
s/(->|\.)connections_/\1connections()/g;'
|
2014-07-26 15:58:23 +02:00 |
Clifford Wolf
|
cc4f10883b
|
Renamed RTLIL::{Module,Cell}::connections to connections_
|
2014-07-26 11:58:03 +02:00 |
Clifford Wolf
|
c094c53de8
|
Removed RTLIL::SigSpec::optimize()
|
2014-07-23 20:32:28 +02:00 |
Clifford Wolf
|
a62c21c9c6
|
Removed RTLIL::SigSpec::expand() method
|
2014-07-23 19:34:51 +02:00 |
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
|
3b52121d32
|
now ignore init attributes on non-register wires in sat command
|
2014-07-05 11:18:38 +02:00 |
Clifford Wolf
|
34e54cda5b
|
Small improvement in SAT log messages
|
2014-03-13 13:12:49 +01:00 |
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
|
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
|
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
|
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
|
374674aff4
|
Added sat -show-inputs and -show-outputs
|
2014-02-01 22:52:44 +01:00 |
Clifford Wolf
|
03a876c7e8
|
Added sat -tempinduc and sat -prove-asserts
|
2014-01-19 16:35:17 +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 |