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 |
|
Clifford Wolf
|
10e57f3880
|
Fix $dlatch handling in async2sync
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2019-09-30 14:58:23 +02:00 |
|
Clifford Wolf
|
c499dc3e73
|
Add $dlatch support to async2sync
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2019-08-28 09:45:22 +02:00 |
|
Eddie Hung
|
28133432be
|
Ignore all 1'bx in (* init *)
|
2019-08-27 09:24:59 -07:00 |
|
Eddie Hung
|
51ffb093b5
|
In sat: 'x' in init attr should not override constant
|
2019-08-22 16:43:08 -07:00 |
|
Eddie Hung
|
4cfefae21e
|
More use of IdString::in()
|
2019-08-15 09:23:57 -07:00 |
|
Eddie Hung
|
6d77236f38
|
substr() -> compare()
|
2019-08-07 12:20:08 -07:00 |
|
Eddie Hung
|
0c78c62d6c
|
Remove std:: namespace
|
2019-08-07 11:11:14 -07:00 |
|
Eddie Hung
|
48d0f99406
|
stoi -> atoi
|
2019-08-07 11:09:17 -07:00 |
|
Eddie Hung
|
c11ad24fd7
|
Use std::stoi instead of atoi(<str>.c_str())
|
2019-08-06 16:45:48 -07:00 |
|