David Shah
|
abf81c7639
|
sim: Fix handling of constant-connected cell inputs at startup
Signed-off-by: David Shah <dave@ds0.me>
|
2020-04-21 08:58:52 +01:00 |
|
David Shah
|
586739ecf3
|
qbfsat: Fix illegal use of 'stdout' identifier
Signed-off-by: David Shah <dave@ds0.me>
|
2020-04-17 08:42:39 +01:00 |
|
N. Engelhardt
|
0b7a5879e5
|
Merge pull request #1830 from boqwxp/qbfsat
Add `qbfsat` command to integrate exists-forall solving and specialization
|
2020-04-15 17:33:50 +02:00 |
|
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 |
|
Eddie Hung
|
956ecd48f7
|
kernel: big fat patch to use more ID::*, otherwise ID(*)
|
2020-04-02 09:51:32 -07: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
|
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
|
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 |
|
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
|
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 |
|
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
|
b63b2dbbc3
|
Clean up pseudo-private member usage in passes/sat/eval.cc.
|
2020-03-28 03:11:23 +00:00 |
|
Alberto Gonzalez
|
6b626c2b0f
|
Clean up pseudo-private member usage in passes/sat/miter.cc.
|
2020-03-19 07:07:22 +00:00 |
|
Eddie Hung
|
432a09af80
|
kernel: SigSpec use more const& + overloads to prevent implicit SigSpec
|
2020-03-13 08:17:39 -07:00 |
|
Eddie Hung
|
5ebdc0f8e0
|
Merge pull request #1638 from YosysHQ/eddie/fix1631
clk2fflogic: work for bit-level $_DFF_* and $_DFFSR_*
|
2020-02-05 19:31:18 +01:00 |
|
Claire Wolf
|
4ddaa70fd6
|
Merge pull request #1567 from YosysHQ/eddie/sat_init_warning
sat: suppress 'Warning: ignoring initial value on non-register: ...' when init[i] = 1'bx
|
2020-01-28 17:40:28 +01:00 |
|
Eddie Hung
|
e30b6bbbf8
|
clk2fflogic: work for bit-level $_DFF_* and $_DFFSR_*
|
2020-01-15 09:51:31 -08:00 |
|
Clifford Wolf
|
3fa374a698
|
Add fminit pass
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2020-01-09 21:22:54 +01:00 |
|
Clifford Wolf
|
41ed6ca7a5
|
Fix sim for assignments with lhs<rhs size, fixes #1565
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2019-12-17 17:36:30 +01:00 |
|
Eddie Hung
|
9a892199f7
|
Suppress warning message for init[i] = 1'bx
|
2019-12-11 11:27:10 -08:00 |
|
Eddie Hung
|
ea54b5ea61
|
Revert "Be mindful that sigmap(wire) could have dupes when checking \init"
This reverts commit f46ac1df9f.
|
2019-10-08 12:41:24 -07:00 |
|
Eddie Hung
|
f46ac1df9f
|
Be mindful that sigmap(wire) could have dupes when checking \init
|
2019-10-02 16:08:46 -07:00 |
|