riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
9,261 Commits 76 Branches 48 Tags 62 MiB
Commit Graph

285 Commits

Author SHA1 Message Date
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
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