Alberto Gonzalez
438d2e0025
Clean up passes/tests/test_autotb.cc.
2020-04-06 04:25:21 +00:00
Alberto Gonzalez
f3e282a97c
Clean up passes/techmap/dfflibmap.cc.
2020-04-06 03:02:40 +00:00
Alberto Gonzalez
9168701881
Clean up pseudo-private member usage and simplify passes/techmap/abc.cc.
2020-04-05 21:31:18 +00:00
Alberto Gonzalez
64a32ead38
Clean up passes/techmap/extract.cc.
2020-04-05 19:36:23 +00:00
Alberto Gonzalez
5431ce694c
Clean up passes/hierarchy/submod.cc.
2020-04-05 04:39:54 +00:00
Alberto Gonzalez
5fedd0931c
Use newly-renamed -push-copy option.
2020-04-04 22:22:54 +00:00
Alberto Gonzalez
0ca3a8e94f
Improve style in passes/sat/qbfsat.cc.
2020-04-04 22:13:27 +00:00
Alberto Gonzalez
1db73e8dd2
Gracefully report error when module has nothing to prove.
2020-04-04 22:13:27 +00:00
Alberto Gonzalez
8f0f13cad2
Suppress yosys-smtbmc output unless the new -show-smtbmc option is provided.
2020-04-04 22:13:27 +00:00
Alberto Gonzalez
ce033a8e36
Fix handling of -sat and -unsat options when the solver returns unknown.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
6af8b767b4
Use log_push() and log_pop() and show the satisfiable model when -specialize is not specified.
...
Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
d311a80222
Clean up qbfsat command and fix AND-reduction of miter outputs.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
125a583c57
Use the -duplicate option rather than -save and -load with an explicit name.
...
Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
86fc49a9d6
Use internal run_command() API instead of popen().
...
Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
09b2264837
Clean up manual casting.
...
Co-Authored-By: David Shah <dave@ds0.me>
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
acf96b6b0b
Remove unimplemented -timeout option.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
bb101e0b3a
Implement the -assume-outputs, -sat, and -unsat options for the qbfsat` command.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
5527063f66
Add NDEBUG guards to qbfsat assertions.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
3a4fd4a999
Implement -specialize-from-file option for the qbfsat command.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
b9e79e0bb7
Implement -write-solution option for the qbfsat command.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
d07ac2612b
Clean up passes/sat/qbfsat.cc.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
437afa1f0c
Updated yosys-smtbmc to optionally dump raw bit strings, and fixed hole value recovery using that mode.
2020-04-04 22:13:25 +00:00
Alberto Gonzalez
a4598d64ef
Hole value recovery and specialization implementation for qbfsat command.
2020-04-04 22:13:25 +00:00
Alberto Gonzalez
2fff574741
Barebones implementation of qbfsat command.
2020-04-04 22:13:25 +00:00
Alberto Gonzalez
fb878b2a70
Initial skeleton for qbfsat command.
2020-04-04 22:13:25 +00:00
Alberto Gonzalez
a0416fe167
Rename -duplicate to -push-copy.
...
Co-Authored-By: whitequark <whitequark@whitequark.org>
2020-04-04 21:26:11 +00:00
Alberto Gonzalez
409e2ac09d
Add -duplicate option to the design command.
2020-04-03 16:46:35 +00:00
whitequark
745251a31f
splitnets: skip modules with processes.
2020-04-03 11:27:19 +00:00
whitequark
e0def9e4d9
memory_map: add -attr option, to respect inference attributes.
...
Before this commit, memory_map (which is always a part of a synth
script) would always pick up any $mem cell that was not processed
by a preceding pass and lower it down to $dff/$mux cells.
This is undesirable for two reasons:
* If there is an explicit inference attribute set on a $mem cell,
e.g. (* ram_block *), then it is arguably incorrect to map such
a memory to $dff/$mux cells.
* If memory_map tries to lower a memory that was intended to
be mapped to a large BRAM, it often takes extraordinarily long
time to finish, produces an extremely large log file, and outputs
an unusable design.
After this commit, properly invoked memory_map will not map any
memory that has an explicit inference attribute specified, solving
the first issue, and alleviating the second. The default behavior
is not changed.
2020-04-03 05:51:40 +00:00
Eddie Hung
5f662b1c43
Merge pull request #1767 from YosysHQ/eddie/idstrings
...
IdString: use more ID::*, make them easier to use, speed up IdString::in()
2020-04-02 11:47:25 -07:00
Eddie Hung
956ecd48f7
kernel: big fat patch to use more ID::*, otherwise ID(*)
2020-04-02 09:51:32 -07:00
Marcin Kościelnicki
2d3753d730
iopadmap: Fix z assignment to inout port
...
Fixes #1841 .
2020-04-02 18:15:04 +02:00
Claire Wolf
22ef5701c0
Merge pull request #1842 from YosysHQ/mwk/fix-deminout-xz
...
deminout: prevent any constant assignment from demoting to input
2020-04-02 18:14:34 +02:00
Eddie Hung
fdafb74eb7
kernel: use more ID::*
2020-04-02 07:14:08 -07:00
Eddie Hung
37f42fe102
Merge pull request #1845 from YosysHQ/eddie/kernel_speedup
...
kernel: speedup by using more pass-by-const-ref
2020-04-02 07:13:33 -07:00
Eddie Hung
c90324662c
Merge pull request #1828 from YosysHQ/eddie/celltypes_speedup
...
kernel: share a single CellTypes within a pass
2020-04-01 14:17:45 -07:00
Eddie Hung
4ae7f3a8ed
Merge pull request #1790 from YosysHQ/eddie/opt_expr_xor
...
opt_expr: optimise $xor/$xnor/$_XOR_/$_XNOR_ -s with constant inputs
2020-04-01 14:17:01 -07:00
Eddie Hung
e79bc45975
Merge pull request #1789 from YosysHQ/eddie/opt_expr_alu
...
opt_expr: improve performance on $alu and $sub
2020-04-01 14:11:09 -07:00
Eddie Hung
1bb5a5215f
Merge pull request #1761 from YosysHQ/eddie/opt_merge_speedup
...
opt_merge: speedup
2020-03-31 14:50:32 -07:00
Eddie Hung
3e88ede061
Merge pull request #1835 from boqwxp/cleanup_sat_expose
...
Clean up pseudo-private member usage in `passes/sat/expose.cc`.
2020-03-30 13:05:12 -07:00
Eddie Hung
0d878ca256
Merge pull request #1832 from boqwxp/cleanup_passes_cmds_design
...
Clean up pseudo-private member usage in `passes/cmds/design.cc`.
2020-03-30 11:56:17 -07:00
Eddie Hung
2c0739cbad
Merge pull request #1786 from boqwxp/hierarchycc_cleanup
...
Clean up pseudo-private member usage in `passes/hierarchy/hierarchy.cc`.
2020-03-30 11:37:51 -07:00
Eddie Hung
9f7d20a653
Merge pull request #1831 from boqwxp/cleanup_sat_eval
...
Clean up pseudo-private member usage in `passes/sat/eval.cc`.
2020-03-30 11:13:53 -07:00
Eddie Hung
769c7318e7
Merge pull request #1833 from boqwxp/cleanup_sat_freduce
...
Clean up pseudo-private member usage in `passes/sat/freduce.cc`.
2020-03-30 11:13:06 -07:00
Alberto Gonzalez
00544cffab
Remove unused function parameter.
2020-03-30 18:00:19 +00:00
Alberto Gonzalez
5a0f029e23
Simplify iterating over selected modules or cells.
...
Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
2020-03-30 17:56:07 +00:00
Alberto Gonzalez
7fc0938bb6
Replace RTLIL::id2cstr() with log_id().
...
Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
2020-03-30 16:50:36 +00:00
Alberto Gonzalez
4c92f9380c
Fix double deletion in passes/hierarchy/hierarchy.cc.
...
Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
2020-03-30 16:43:54 +00:00
Alberto Gonzalez
f4faa1514b
Further clean up passes/sat/eval.cc.
...
Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
2020-03-30 16:38:35 +00:00
Alberto Gonzalez
9f265dfd3f
Further clean up passes/sat/freduce.cc.
...
Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
2020-03-30 16:25:30 +00:00
