aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
Commit message (Collapse)AuthorAgeFilesLines
...
| * Implement `-write-solution` option for the `qbfsat` command.Alberto Gonzalez2020-04-041-7/+28
| |
| * Clean up `passes/sat/qbfsat.cc`.Alberto Gonzalez2020-04-041-86/+101
| |
| * Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole ↵Alberto Gonzalez2020-04-041-29/+39
| | | | | | | | value recovery using that mode.
| * Hole value recovery and specialization implementation for `qbfsat` command.Alberto Gonzalez2020-04-041-20/+63
| |
| * Barebones implementation of `qbfsat` command.Alberto Gonzalez2020-04-041-32/+157
| |
| * Initial skeleton for `qbfsat` command.Alberto Gonzalez2020-04-042-0/+207
| |
* | kernel: big fat patch to use more ID::*, otherwise ID(*)Eddie Hung2020-04-0212-272/+272
| |
* | kernel: use more ID::*Eddie Hung2020-04-029-60/+60
| |
* | Merge pull request #1845 from YosysHQ/eddie/kernel_speedupEddie Hung2020-04-021-8/+8
|\ \ | |/ |/| kernel: speedup by using more pass-by-const-ref
| * kernel: SigSpec use more const& + overloads to prevent implicit SigSpecEddie Hung2020-03-131-8/+8
| |
* | Merge pull request #1835 from boqwxp/cleanup_sat_exposeEddie Hung2020-03-301-85/+66
|\ \ | | | | | | Clean up pseudo-private member usage in `passes/sat/expose.cc`.
| * | Remove unused function parameter.Alberto Gonzalez2020-03-301-2/+2
| | |
| * | Simplify iterating over selected modules or cells.Alberto Gonzalez2020-03-301-16/+4
| | | | | | | | | | | | Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
| * | Clean up more in `passes/sat/expose.cc`.Alberto Gonzalez2020-03-301-64/+59
| | | | | | | | | | | | Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
| * | Clean up pseudo-private member usage in `passes/sat/expose.cc`.Alberto Gonzalez2020-03-281-11/+9
| | |
* | | Merge pull request #1831 from boqwxp/cleanup_sat_evalEddie Hung2020-03-301-46/+44
|\ \ \ | | | | | | | | Clean up pseudo-private member usage in `passes/sat/eval.cc`.
| * | | Further clean up `passes/sat/eval.cc`.Alberto Gonzalez2020-03-301-16/+15
| | | | | | | | | | | | | | | | Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
| * | | Clean up pseudo-private member usage in `passes/sat/eval.cc`.Alberto Gonzalez2020-03-281-35/+34
| |/ /
* | | Further clean up `passes/sat/freduce.cc`.Alberto Gonzalez2020-03-301-3/+2
| | | | | | | | | | | | Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
* | | Clean up pseudo-private member usage in `passes/sat/freduce.cc`.Alberto Gonzalez2020-03-281-13/+12
|/ /
* / Clean up pseudo-private member usage in `passes/sat/miter.cc`.Alberto Gonzalez2020-03-191-60/+56
|/
* Merge pull request #1638 from YosysHQ/eddie/fix1631Eddie Hung2020-02-051-6/+77
|\ | | | | clk2fflogic: work for bit-level $_DFF_* and $_DFFSR_*
| * clk2fflogic: work for bit-level $_DFF_* and $_DFFSR_*Eddie Hung2020-01-151-6/+77
| |
* | Merge pull request #1567 from YosysHQ/eddie/sat_init_warningClaire Wolf2020-01-281-1/+2
|\ \ | | | | | | sat: suppress 'Warning: ignoring initial value on non-register: ...' when init[i] = 1'bx
| * | Suppress warning message for init[i] = 1'bxEddie Hung2019-12-111-1/+2
| | |
* | | Add fminit passClifford Wolf2020-01-092-0/+198
| |/ |/| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Fix sim for assignments with lhs<rhs size, fixes #1565Clifford Wolf2019-12-171-1/+1
|/ | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Revert "Be mindful that sigmap(wire) could have dupes when checking \init"Eddie Hung2019-10-081-4/+1
| | | | This reverts commit f46ac1df9f8847dac9d9851f2f948d93a1064ff1.
* Be mindful that sigmap(wire) could have dupes when checking \initEddie Hung2019-10-021-1/+4
|
* Fix $dlatch handling in async2syncClifford Wolf2019-09-301-0/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add $dlatch support to async2syncClifford Wolf2019-08-281-1/+36
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Ignore all 1'bx in (* init *)Eddie Hung2019-08-271-3/+1
|
* In sat: 'x' in init attr should not override constantEddie Hung2019-08-221-0/+2
|
* More use of IdString::in()Eddie Hung2019-08-151-1/+1
|
* substr() -> compare()Eddie Hung2019-08-073-6/+6
|
* Remove std:: namespaceEddie Hung2019-08-071-5/+5
|
* stoi -> atoiEddie Hung2019-08-074-33/+33
|
* Use std::stoi instead of atoi(<str>.c_str())Eddie Hung2019-08-064-33/+33
|
* Use State::S{0,1}Eddie Hung2019-08-062-3/+3
|
* Fix tests/various/async FFL testClifford Wolf2019-07-091-0/+7
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add a few more filename rewritesBen Widawsky2019-06-201-0/+4
| | | | | | | | | | This now allows a full pipeline to work, something such as: yosys -p "synth_ecp5 -json ~/work/fpga/prjtrellis/examples/ecp5_evn/blinky.v" Otherwise, you will get something along the lines of: ERROR: Can't open output file `~/work/fpga/prjtrellis/examples/ecp5_evn/blinky.v' for writing: No such file or directory Signed-off-by: Ben Widawsky <ben@bwidawsk.net>
* Fixed the help summary line for a few commandsacw12512019-06-192-4/+4
|
* Error out if no top module given before 'sim'Eddie Hung2019-06-051-0/+5
|
* Fix typo in fmcombine log message, fixes #1063Clifford Wolf2019-06-051-2/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add "fmcombine -initeq -anyeq"Clifford Wolf2019-05-111-3/+38
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix bug in "expose -input"Clifford Wolf2019-05-061-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add missing enable_undef to "sat -tempinduct-def", fixes #883Clifford Wolf2019-05-021-0/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add "techmap -wb", use in formal flowsClifford Wolf2019-04-201-4/+4
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Added missing argument checking to "mutate" commandClifford Wolf2019-04-041-0/+32
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add "cutpoint -undef"Clifford Wolf2019-03-261-10/+14
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>