mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-26 09:24:37 +00:00
Code Activity
12561 commits 122 branches 59 tags 72 MiB
Commit graph

479 commits

Author SHA1 Message Date
N. Engelhardt
668d5253a5 sim -vcd: add date, version, and option for timescale 2020-10-16 18:19:58 +02:00
N. Engelhardt
3238190797 use the new isPublic() in a few places 2020-09-14 12:43:18 +02:00
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 AttrObjects 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