mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-08 18:31:51 +00:00
Code Activity
9352 commits 94 branches 52 tags 62 MiB
Commit graph

286 commits

Author SHA1 Message Date
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
Clifford Wolf 10e57f3880 Fix $dlatch handling in async2sync 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-09-30 14:58:23 +02:00