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
|
f092b50148
|
Renamed $_INV_ cell type to $_NOT_
|
2014-08-15 14:11:40 +02:00 |
Clifford Wolf
|
9d4362990f
|
Fixed "share" for complex scenarios with never-active cells
|
2014-08-09 17:07:20 +02:00 |
Clifford Wolf
|
b9811d5aff
|
Do not share any $reduce_* cells (its complicated and not worth it anyways)
|
2014-08-09 15:40:25 +02:00 |
Clifford Wolf
|
cb6ca08a53
|
Fixed sharing of reduce operator
|
2014-08-08 14:24:09 +02:00 |
Clifford Wolf
|
622ebab671
|
Added "sat -prove-skip"
|
2014-08-08 13:11:54 +02:00 |
Clifford Wolf
|
c55eb8f8a6
|
Use "-keepdc" in "miter -equiv -flatten"
|
2014-08-07 16:42:35 +02:00 |
Clifford Wolf
|
c7f99be3be
|
Fixed "share" for memory read ports
|
2014-08-03 20:22:33 +02:00 |
Clifford Wolf
|
8e7361f128
|
Removed at() method from RTLIL::IdString
|
2014-08-02 19:08:02 +02:00 |
Clifford Wolf
|
768eb846c4
|
More bugfixes related to new RTLIL::IdString
|
2014-08-02 18:14:21 +02:00 |
Clifford Wolf
|
b9bd22b8c8
|
More cleanups related to RTLIL::IdString usage
|
2014-08-02 13:19:57 +02:00 |
Clifford Wolf
|
32a1cc3efd
|
Renamed modwalker.h to modtools.h
|
2014-07-31 23:30:18 +02:00 |
Clifford Wolf
|
cdae8abe16
|
Renamed port access function on RTLIL::Cell, added param access functions
|
2014-07-31 16:38:54 +02:00 |
Clifford Wolf
|
e6d33513a5
|
Added module->design and cell->module, wire->module pointers
|
2014-07-31 14:11:39 +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
|
d68c993ed2
|
Changed more code to the new RTLIL::Wire constructors
|
2014-07-26 21:30:38 +02:00 |
Clifford Wolf
|
946ddff9ce
|
Changed a lot of code to the new RTLIL::Wire constructors
|
2014-07-26 20:12:50 +02:00 |
Clifford Wolf
|
3f4e3ca8ad
|
More RTLIL::Cell API usage cleanups
|
2014-07-26 16:14:02 +02:00 |
Clifford Wolf
|
97a59851a6
|
Added RTLIL::Cell::has(portname)
|
2014-07-26 16:11:28 +02:00 |
Clifford Wolf
|
f8fdc47d33
|
Manual fixes for new cell connections API
|
2014-07-26 15:58:23 +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
|
2bec47a404
|
Use only module->addCell() and module->remove() to create and delete cells
|
2014-07-25 17:56:19 +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
|
4e802eb7f6
|
Fixed all users of SigSpec::chunks_rw() and removed it
|
2014-07-23 15:36:09 +02:00 |
Clifford Wolf
|
ec923652e2
|
Refactoring {SigSpec|SigChunk}(RTLIL::Wire *wire, ..) constructor -- step 3/3
|
2014-07-23 09:52:55 +02:00 |
Clifford Wolf
|
a8d3a68971
|
Refactoring {SigSpec|SigChunk}(RTLIL::Wire *wire, ..) constructor -- step 2/3
|
2014-07-23 09:49:43 +02:00 |
Clifford Wolf
|
260c19ec5a
|
Refactoring {SigSpec|SigChunk}(RTLIL::Wire *wire, ..) constructor -- step 1/3
|
2014-07-23 09:34:47 +02:00 |
Clifford Wolf
|
28b3fd05fa
|
SigSpec refactoring: change RTLIL::SigSpec::chunks() to be read-only, created interim RTLIL::SigSpec::chunks_rw()
|
2014-07-22 20:58:44 +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
|
1d88f1cf9f
|
Removed deprecated module->new_wire()
|
2014-07-21 12:35:06 +02:00 |
Clifford Wolf
|
3cb61d03f8
|
Wider range of cell types supported in "share" pass
|
2014-07-21 12:18:29 +02:00 |
Clifford Wolf
|
b49beab1f3
|
Use ezSAT::non_incremental() in "share" pass
|
2014-07-21 02:08:38 +02:00 |
Clifford Wolf
|
04fcb07213
|
Added support for resource sharing in mux control logic
|
2014-07-20 20:44:14 +02:00 |
Clifford Wolf
|
e9506bb2da
|
Supercell creation for $div/$mod worked all along, fixed test benches
|
2014-07-20 18:54:06 +02:00 |
Clifford Wolf
|
ff28029fdb
|
Fixed creation of shift supercells in "share" pass
|
2014-07-20 17:06:36 +02:00 |
Clifford Wolf
|
4c38ec1cc8
|
Added "miter -equiv -flatten"
|
2014-07-20 15:33:07 +02:00 |
Clifford Wolf
|
5b3ee7a072
|
Added "share" supercell creation
|
2014-07-20 15:01:17 +02:00 |
Clifford Wolf
|
7b98e46ac3
|
Added removing of always inactive cells to "share" pass
|
2014-07-20 13:24:36 +02:00 |
Clifford Wolf
|
8819493db4
|
Progress in "share" pass
|
2014-07-20 11:04:52 +02:00 |
Clifford Wolf
|
15fd615da5
|
Progress in "share" pass
|
2014-07-20 03:03:04 +02:00 |
Clifford Wolf
|
2278995bd8
|
Started to implement real resource sharing
|
2014-07-19 20:54:32 +02:00 |
Clifford Wolf
|
3b52121d32
|
now ignore init attributes on non-register wires in sat command
|
2014-07-05 11:18:38 +02:00 |
Johann Glaser
|
278085fa01
|
added log_header to miter and expose pass, show cell type for exposed ports
|
2014-05-28 18:05:38 +02:00 |
Clifford Wolf
|
34e54cda5b
|
Small improvement in SAT log messages
|
2014-03-13 13:12:49 +01:00 |
Clifford Wolf
|
e3b11ea2d6
|
Fixed bug in freduce command
|
2014-03-07 18:44:23 +01:00 |
Clifford Wolf
|
6f8865d81a
|
Some minor code cleanups in freduce command
|
2014-03-07 18:29:04 +01:00 |
Clifford Wolf
|
54d74cf616
|
Added freduce -dump
|
2014-03-06 22:06:58 +01:00 |
Clifford Wolf
|
da5859a674
|
Added freduce -stop
|
2014-03-06 18:14:26 +01:00 |
Clifford Wolf
|
96e753041d
|
fixed freduce for Minisat::SimpSolver: use frozen_literal()
|
2014-03-03 02:14:27 +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
|
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 |
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 |