Alberto Gonzalez
|
e300766fb3
|
Use pool instead of std::set .
|
2020-04-11 09:41:09 +00:00 |
|
Alberto Gonzalez
|
73bd7fb01d
|
Use dict instead of std::map .
|
2020-04-11 06:53:59 +00:00 |
|
Alberto Gonzalez
|
de5e6fa56a
|
Clean up passes/sat/qbfsat.cc .
Makes various cosmetic fixes, removes superfluous `hasPort()` check, and uses `emplace_back()` instead of `push_back()`.
|
2020-04-09 07:47:44 +00:00 |
|
Alberto Gonzalez
|
194354e128
|
Remove $anyconst cells before specialization to eliminate warnings and the need to run opt_clean .
|
2020-04-07 03:29: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 |
|
Eddie Hung
|
05f74d4f31
|
Merge pull request #1783 from boqwxp/astcc_cleanup
Clean up pseudo-private member usage in `frontends/ast/ast.cc`.
|
2020-03-30 13:06:10 -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 |
|
Alberto Gonzalez
|
b538c6fbf2
|
Add explanatory comment about inefficient wire removal and remove superfluous call to fixup_ports() .
Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
|
2020-03-30 18:14:32 +00: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 |
|
Alberto Gonzalez
|
696660351f
|
Clean up more in passes/sat/expose.cc .
Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
|
2020-03-30 16:16:16 +00:00 |
|
N. Engelhardt
|
d5e2061687
|
Merge pull request #1811 from PeterCrozier/typedef_scope
Support module/package/interface/block scope for typedef names.
|
2020-03-30 13:55:39 +02:00 |
|
N. Engelhardt
|
2c847e7efe
|
Merge pull request #1778 from rswarbrick/sv-defines
Add support for SystemVerilog-style `define to Verilog frontend
|
2020-03-30 13:51:12 +02:00 |
|
Miodrag Milanovic
|
1dbc701728
|
Explicit include of csignal
|
2020-03-28 09:49:08 +01:00 |
|
Miodrag Milanovic
|
5cdcd6ec79
|
windows - there are no stopping signals
|
2020-03-28 09:09:11 +01:00 |
|
Alberto Gonzalez
|
1197a43380
|
Clean up pseudo-private member usage in passes/sat/expose.cc .
|
2020-03-28 06:18:09 +00:00 |
|
Alberto Gonzalez
|
9a0cdc3835
|
Clean up pseudo-private member usage in passes/sat/freduce.cc .
|
2020-03-28 06:08:23 +00:00 |
|
Alberto Gonzalez
|
4681f02a6e
|
Clean up pseudo-private member usage in passes/cmds/design.cc .
|
2020-03-28 05:10:18 +00:00 |
|
Alberto Gonzalez
|
b63b2dbbc3
|
Clean up pseudo-private member usage in passes/sat/eval.cc .
|
2020-03-28 03:11:23 +00:00 |
|
Claire Wolf
|
1bf2bdf05b
|
Merge pull request #1607 from whitequark/simplify-simplify-meminit
ast: avoid intermediate wires/assigns when lowering to AST_MEMINIT
|
2020-03-27 17:28:26 +01:00 |
|
Peter Crozier
|
f8c065ed1c
|
Inline productions to follow house style.
|
2020-03-27 16:21:45 +00:00 |
|