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

327 Commits

Author SHA1 Message Date
Marcelina Kościelnicka 4a05cad7f8 async2sync: Support all FF types. 2020-07-30 20:22:03 +02:00
Marcelina Kościelnicka bd959d5d9e async2sync: Refactor to use FfInitVals. 2020-07-24 11:22:31 +02:00
Marcelina Kościelnicka abe4e9e607 clk2fflogic: Support all FF types. 2020-07-24 03:19:48 +02:00
Alberto Gonzalez 2f786fcfac
qbfsat: Add `-solver-option` option. 2020-07-20 21:54:56 +00:00
Marcelina Kościelnicka 03e28f7ab4 clk2fflogic: Consistently treat async control signals as negative hold. 
This fixes some dfflegalize equivalence checks, and breaks others — and
I strongly suspect the others are due to bad support for multiple
async inputs in `proc` (in particular, lack of proper support for
dlatchsr and sketchy circuits on dffsr control inputs).
 2020-07-09 18:12:47 +02:00
clairexen e4b9e64d1b
Merge pull request #2208 from boqwxp/qbfsat-cleanup 
qbfsat: Cleanup and refactoring
 2020-07-02 17:48:37 +02:00
clairexen d3422f8a5e
Merge pull request #2211 from YosysHQ/mwk/fix-fmcombine-ff 
fmcombine: use the master ff cell type list
 2020-07-02 17:43:48 +02:00
Alberto Gonzalez 56f98b9e3d
qbfsat: Remove useless comment and #ifndef guards. 2020-07-01 19:55:16 +00:00
Alberto Gonzalez 3345d39e6f
qbfsat: Specify default values for some options in the help message. 2020-07-01 19:55:16 +00:00
Alberto Gonzalez 95e8016811
qbfsat: Clean up external executable command lines and update temporary directory name. 2020-07-01 19:55:16 +00:00
Alberto Gonzalez 8cd60be654
qbfsat: Clean up and refactor data structures into `qbfsat.h`. 2020-07-01 19:55:16 +00:00
clairexen b1707407a0
Merge pull request #2138 from boqwxp/qbfsat-oflag 
qbfsat: Add `-O[012]` options to control pre-solving simplification with ABC
 2020-07-01 16:35:27 +02:00
clairexen 2b0f6e24e2
Merge pull request #2206 from boqwxp/qbfsat-fix-name-specialization 
qbfsat: Fix name-based hole specialization
 2020-07-01 16:34:32 +02:00
Marcelina Kościelnicka 7c91f13f51 fmcombine: use the master ff cell type list 2020-06-30 21:07:17 +02:00
clairexen 3fb5b4fd8a
Merge pull request #2199 from YosysHQ/mmicko/sim_memory 
sim - error when memrd and memwr detected
 2020-06-30 17:12:51 +02:00
Alberto Gonzalez 83c595aaac
qbfsat: Add `-O[012]` options to control pre-solving simplification with ABC. 
Thanks to @mwk for the gate mapping part of the ABC scripts.

Co-Authored-By: Marcelina Kościelnicka <mwk@0x04.net>
 2020-06-30 06:44:17 +00:00
Alberto Gonzalez f544a2cc84
qbfsat: Fix name-based hole specialization. 
Look for unique connections in the containing module with the $anyconst port Y SigBit on the RHS and use those. If no such connection is found, fall back to using the name of the $anyconst port Y SigBit.
 2020-06-30 01:53:21 +00:00
Miodrag Milanovic 405b4e97a1 Give error that options are exclusive 2020-06-29 14:45:49 +02:00
Miodrag Milanovic 0545a042f3 cleanup 2020-06-29 14:42:48 +02:00
Miodrag Milanovic 87717d67d1 expose pass fix 2020-06-29 11:56:43 +02:00
Miodrag Milanovic 48b6d3272c sim - error when memrd and memwr detected 2020-06-29 10:33:39 +02:00
Alberto Gonzalez a564cc806f
log, qbfsat: Include child process time in `PerformanceTimer::query()` and report the time for each call to the QBF-SAT solver. 2020-06-21 02:16:52 +00:00
Alberto Gonzalez 62a9e62a1b
qbfsat: Simplify solution recovery parsing and tweak the solution regexes. 2020-06-21 02:16:11 +00:00
Alberto Gonzalez e1fedf054e
qbfsat: Avoid instantiating `AttrObject`s directly. 
Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
 2020-06-21 02:16:11 +00:00
Alberto Gonzalez 08cede4669
qbfsat: Simplify solution format and replace `SigBit::str()` with `log_signal()`. 
Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
 2020-06-21 02:16:11 +00:00
Alberto Gonzalez 4ab41c6435
qbfsat: Fixes three bugs. 
1. Infinite loop in the optimization procedure when the first solution found while maximizing is at zero.
2. A signed-ness issue when maximizing.
3. Erroneously entering bisection mode with no wire to optimize.
 2020-06-21 02:16:11 +00:00
Alberto Gonzalez a3d1f8637a
qbfsat: Use bit precise mapping for hole value wires and a more robust hole spec for writing to and specializing from a solution file. 2020-06-21 02:16:11 +00:00
whitequark ede4b10da8
Merge pull request #2173 from whitequark/use-cxx11-final-override 
Use C++11 final/override/[[noreturn]]
 2020-06-19 06:15:33 +00:00
whitequark 7191dd16f9 Use C++11 final/override keywords. 2020-06-18 23:34:52 +00:00
Alberto Gonzalez 76dfa81790
cutpoint: Improve efficiency by iterating over module ports instead of module wires. 2020-06-18 17:42:36 +00:00
Claire Wolf 0bd70e8222 Drive-by modernization in sat.cc 
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
 2020-06-09 22:48:26 +02:00
Alberto Gonzalez 9847a4eea8
smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4. 2020-05-25 20:39:30 +00:00
Alberto Gonzalez f9eef5e3f7
qbfsat: Add support for CVC4. 2020-05-25 20:39:03 +00:00
Alberto Gonzalez 903456c267
qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default. 
Ensures that "BV" is the logic whenever solving an exists-forall problem with Yices, moves the "(set-logic ...)" directive above any non-info line, sets the `ef-max-iters` parameter to a very high number when using Yices in exists-forall mode so as not to prematurely abandon difficult problems, and does not provide the incompatible "--incremental" Yices argument when in exists-forall mode.
 2020-05-25 20:38:29 +00:00
Alberto Gonzalez ac41f8a9c7
qbfsat: Remove cruft inadvertently left untouched in commit 86fc49a9d6. 2020-05-23 00:53:09 +00:00
Alberto Gonzalez aea0fd5ed4
qbfsat: Add bisection mode and make it the default. 
Also adds `-nooptimize` and reorganizes `qbfsat.cc` a bit.
 2020-05-23 00:53:09 +00:00
whitequark b43c282e4e Add WASI platform support. 
This includes the following significant changes:
  * Patching ezsat and minisat to disable resource limiting code
    on WASM/WASI, since the POSIX functions they use are unavailable.
  * Adding a new definition, YOSYS_DISABLE_SPAWN, present if platform
    does not support spawning subprocesses (i.e. Emscripten or WASI).
    This definition hides the definition of `run_command()`.
  * Adding a new Makefile flag, DISABLE_SPAWN, present in the same
    condition. This flag disables all passes that require spawning
    subprocesses for their function.
 2020-04-30 18:56:25 +00:00
Claire Wolf dc9a72bc8d
Merge pull request #1989 from boqwxp/qbfsat_anyconst_sourcelocs 
qbfsat: Make hole name recovery from source locations more robust.
 2020-04-23 11:34:19 +02:00
Alberto Gonzalez 4ee8452d34
qbfsat: Make hole name recovery more robust. Allow multiple cell types to share the same source location as long as only one `$anyconst` or `$anyseq` has that location. 2020-04-23 05:45:44 +00:00
Alberto Gonzalez 7369e6b26b
qbfsat: Add `-assume-negative-polarity` option. 2020-04-23 04:06:15 +00:00
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