Commit Graph

487 Commits

Author SHA1 Message Date
Marcelina Kościelnicka 4746ffd7b2 assertpmux: Fix crash on unused $pmux output.
Fixes #2595.
2021-02-22 23:30:28 +01:00
Gabriel Somlo 150b729b6f Add #include needed to build with gcc-11
Suggested by Jeff Law <law@redhat.com>
2020-11-26 06:12:12 -05:00
Chris Dailey cdc802e4b7
Add rewrite_filename for sim -vcd argument. 2020-11-24 15:17:16 -05:00
N. Engelhardt 3b86b5da5f
Merge pull request #2403 from nakengelhardt/sim_timescale
sim -vcd: add date, version, and option for timescale
2020-10-22 14:01:24 +02:00
Marcelina Kościelnicka b065e09045 sim: Use Mem helper. 2020-10-21 17:51:20 +02:00
Marcelina Kościelnicka e759e301a8 clk2fflogic: Use Mem helper. 2020-10-21 17:51:20 +02:00
N. Engelhardt 1c96a0b1d5 use strftime instead of put_time for gcc 4.8 compatibility 2020-10-21 17:47:00 +02:00
N. Engelhardt eccc48c39f wild guessing at the problem because it builds fine on my machines 2020-10-16 18:46:59 +02:00
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 `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
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
Eddie Hung 28133432be Ignore all 1'bx in (* init *) 2019-08-27 09:24:59 -07:00
Eddie Hung 51ffb093b5 In sat: 'x' in init attr should not override constant 2019-08-22 16:43:08 -07:00
Eddie Hung 4cfefae21e More use of IdString::in() 2019-08-15 09:23:57 -07:00
Eddie Hung 6d77236f38 substr() -> compare() 2019-08-07 12:20:08 -07:00
Eddie Hung 0c78c62d6c Remove std:: namespace 2019-08-07 11:11:14 -07:00
Eddie Hung 48d0f99406 stoi -> atoi 2019-08-07 11:09:17 -07:00
Eddie Hung c11ad24fd7 Use std::stoi instead of atoi(<str>.c_str()) 2019-08-06 16:45:48 -07:00
Eddie Hung 046e1a5214 Use State::S{0,1} 2019-08-06 16:22:47 -07:00
Clifford Wolf 9546ccdbd3 Fix tests/various/async FFL test
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-07-09 22:44:39 +02:00
Ben Widawsky 8767ec3fbd Add a few more filename rewrites
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>
2019-06-20 10:27:59 -07:00
acw1251 0d888ee7ed Fixed the help summary line for a few commands 2019-06-19 15:27:04 -04:00
Eddie Hung dd134914cc Error out if no top module given before 'sim' 2019-06-05 14:16:24 -07:00
Clifford Wolf 4190d7c094 Fix typo in fmcombine log message, fixes #1063
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-05 09:26:44 +02:00
Clifford Wolf b66b657b6b Add "fmcombine -initeq -anyeq"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-05-11 09:28:55 +02:00
Clifford Wolf f02e22a35a Fix bug in "expose -input"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-05-06 13:30:55 +02:00
Clifford Wolf 521663f09e Add missing enable_undef to "sat -tempinduct-def", fixes #883
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-05-02 00:03:31 +02:00
Clifford Wolf f3ad8d680a Add "techmap -wb", use in formal flows
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-04-20 11:23:24 +02:00
Clifford Wolf 75ca06526a Added missing argument checking to "mutate" command
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-04-04 18:10:10 +02:00
Clifford Wolf 38b3fbd3f0 Add "cutpoint -undef"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-26 16:01:14 +01:00
Clifford Wolf ddc1a4488e Add "cutpoint" pass
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-25 19:49:00 +01:00
Clifford Wolf ccfa2fe01c Add "mutate -none -mode", "mutate -mode none"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-23 20:20:32 +01:00
Clifford Wolf 59c44bb61a Add "mutate -s <filename>"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-23 17:53:09 +01:00
Clifford Wolf aa65d3fe65 Improve mix of src/wire/wirebit coverage in "mutate -list"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-16 00:55:46 +01:00
Clifford Wolf dacaebae35 Add "fmcombine -fwd -bwd -nop"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-15 21:45:37 +01:00
Clifford Wolf 370db33a4c Add fmcombine pass
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-15 20:46:17 +01:00
Clifford Wolf d1985f6a22 Improvements in "mutate" list-reduce algorithm
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-15 00:18:31 +01:00
Clifford Wolf 27a5d9c91e Add "mutate -cfg", improve pick_cover behavior
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-14 23:20:41 +01:00
Clifford Wolf 4d304e3da7 Add a strictly coverage-driven mutation selection strategy
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-14 23:01:55 +01:00
Clifford Wolf 2a4263a75d Improve "mutate" wire coverage metric
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-14 23:01:01 +01:00
Clifford Wolf 1b4fdbb0d8 Add more mutation types, improve mutation src cover
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-14 22:04:42 +01:00
Clifford Wolf 6ad5d036c5 Add "mutate" command DB reduce functionality
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-14 22:04:42 +01:00
Clifford Wolf 8e6b69d7bb Add "mutate -mode inv", various other mutate improvements
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-14 22:04:42 +01:00
Clifford Wolf ea8ee24140 Add basic "mutate -list N" framework
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-14 22:04:42 +01:00
Clifford Wolf 399ab16315 Add $dffsr support to async2sync
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-09 11:52:00 -08:00
Clifford Wolf 63be3f3bab Improvements in "supercover" pass
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-27 11:45:13 -08:00
Clifford Wolf a58dbcf2ba Add "supercover" skeleton
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-27 11:37:08 -08:00
acw1251 5fe16c25b8 Fixed minor typo in "sim" help message 2018-09-12 18:34:27 -04:00
Henner Zeller 3aa4484a3c Consistent use of 'override' for virtual methods in derived classes.
o Not all derived methods were marked 'override', but it is a great
  feature of C++11 that we should make use of.
o While at it: touched header files got a -*- c++ -*- for emacs to
  provide support for that language.
o use YS_OVERRIDE for all override keywords (though we should probably
  use the plain keyword going forward now that C++11 is established)
2018-07-20 23:51:06 -07:00
Clifford Wolf 87aef8f0cc Add async2sync pass
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-07-19 15:31:12 +02:00
Clifford Wolf 665eec3d53 Removed $timescale from "sat" command VCD writer
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-29 12:38:41 +02:00
Clifford Wolf 08225f49a4 Add "expose -input"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-12 13:52:52 +01:00
Clifford Wolf d31584c649 Add $dlatchsr support to clk2fflogic 2018-02-26 12:20:28 +01:00
Clifford Wolf 6132e6e72a Fix a bug in clk2fflogic memory handling 2017-12-14 03:05:55 +01:00
Clifford Wolf 590e6961cb Add clk2fflogic memory support 2017-12-14 02:07:31 +01:00
Clifford Wolf 88182e46d7 Check for memories in clk2fflogic 2017-12-13 19:14:34 +01:00
Clifford Wolf ca53fba44a Rename "singleton" pass to "uniquify" 2017-08-20 12:31:50 +02:00
Clifford Wolf bbdf7d9c66 Add "sim -zinit -rstlen" 2017-08-18 12:54:17 +02:00
Clifford Wolf d30cc60ba9 Add "sim" support for memories 2017-08-18 11:44:50 +02:00
Clifford Wolf 0be738eaac Add support for assert/assume/cover to "sim" command 2017-08-18 10:24:14 +02:00
Clifford Wolf 92e4b5aa77 Add writeback mode to "sim" command 2017-08-17 15:54:51 +02:00
Clifford Wolf 7b4f3f86c3 Improve "sim" command 2017-08-17 12:27:08 +02:00
Clifford Wolf 75046aa531 Add "sim" command skeleton 2017-08-16 13:05:21 +02:00
Clifford Wolf 05df3dbee4 Add "setundef -anyseq" 2017-05-28 11:59:05 +02:00
Clifford Wolf 15fb56697a Bugfix in "miter -assert" handling of assumptions 2016-10-17 14:56:58 +02:00
Clifford Wolf 6425d34e73 Added clk2fflogic support for $dffsr and $dlatch 2016-10-17 13:28:55 +02:00
Clifford Wolf 3a09d6bb65 Improvements and bugfixes in clk2fflogic 2016-10-16 23:03:29 +02:00
Clifford Wolf fa535c0b00 Some minor build fixes for Visual C 2016-10-14 18:36:02 +02:00
Clifford Wolf 2733994aeb Added clk2fflogic 2016-10-14 14:55:07 +02:00
Clifford Wolf 8ebba8a35f Added $ff and $_FF_ cell types 2016-10-12 01:18:39 +02:00
Clifford Wolf cb7dbf4070 Improvements in assertpmux 2016-09-07 12:42:16 +02:00
Clifford Wolf ab18e9df7c Added assertpmux 2016-09-07 00:28:01 +02:00
Clifford Wolf fc5281b3f7 Run log_flush() before solving in sat command 2016-09-06 17:35:25 +02:00
Clifford Wolf 54966679df Moved SatHelper::setup_init() code to SatHelper::setup() 2016-07-24 12:18:39 +02:00
Clifford Wolf 34e833103b Added $initstate support to "sat" command 2016-07-23 17:01:03 +02:00
Clifford Wolf 0bc95f1e04 Added "yosys -D" feature 2016-04-21 23:28:37 +02:00
Clifford Wolf eaac5bfbc7 Improved formatting of "sat" output tables 2016-04-05 08:26:10 +02:00
Clifford Wolf 1d0f0d668a Renamed opt_const to opt_expr 2016-03-31 08:46:56 +02:00
Clifford Wolf 207736b4ee Import more std:: stuff into Yosys namespace 2015-10-25 19:30:49 +01:00
Clifford Wolf 7f110e7018 renamed SigSpec::to_single_sigbit() to SigSpec::as_bit(), added is_bit() 2015-10-24 22:56:40 +02:00
Clifford Wolf f40d1b78b6 Added sat -show-regs, -show-public, -show-all 2015-08-18 17:14:30 +02:00
Clifford Wolf 0350074819 Re-created command-reference-manual.tex, copied some doc fixes to online help 2015-08-14 11:27:19 +02:00
Clifford Wolf 84bf862f7c Spell check (by Larry Doolittle) 2015-08-14 10:56:05 +02:00
Clifford Wolf badc5f7eb9 Added "miter -assert" 2015-07-25 12:09:57 +02:00
Clifford Wolf 6c84341f22 Fixed trailing whitespaces 2015-07-02 11:14:30 +02:00
Clifford Wolf ee9188a5b4 Added logic-loop error handling to freduce 2015-06-30 17:11:46 +02:00
Clifford Wolf faa95dd845 don't consider blackbox modules in "sat" command 2015-04-18 09:29:03 +02:00
Clifford Wolf 1f1deda888 Added non-std verilog assume() statement 2015-02-26 18:47:39 +01:00
Clifford Wolf 39d25b212c Fixed "sat -initsteps" off-by-one bug 2015-02-22 12:42:05 +01:00
Clifford Wolf fae0e75ace Added "sat -stepsize" and "sat -tempinduct-step" 2015-02-21 22:52:49 +01:00
Clifford Wolf b19c926af8 sat docu change 2015-02-21 22:03:54 +01:00
Clifford Wolf 9237fb924e When "sat -tempinduct-baseonly -maxsteps N" reaches maxsteps it is a good thing. 2015-02-21 20:05:16 +01:00
Clifford Wolf 1688b9b464 Added "sat -tempinduct-baseonly -tempinduct-inductonly" 2015-02-21 17:53:22 +01:00
Clifford Wolf dcbd00c101 Fixed basecase init for "sat -tempinduct" 2015-02-21 17:43:49 +01:00
Clifford Wolf 4e6ca7760f Replaced ezDefaultSAT with ezSatPtr 2015-02-21 12:15:41 +01:00
Clifford Wolf 08c0fe164f format fixes in "sat -dump_json" 2015-02-19 13:19:04 +01:00
Clifford Wolf 1ecee6c49c Added "sat -dump_json" (WaveJSON format) 2015-02-19 10:53:40 +01:00
Clifford Wolf 9ebf803cbe Improved an error message 2015-01-28 00:46:00 +01:00
Clifford Wolf 23e54bda81 Added "sat -show-ports" 2015-01-27 23:04:28 +00:00
Clifford Wolf 0a225f8b27 Moved equiv stuff to passes/equiv/ 2015-01-22 12:03:15 +01:00
Clifford Wolf abf8398216 Progress in equiv_simple 2015-01-21 23:59:58 +00:00
Clifford Wolf 5febbe3620 Added equiv_simple 2015-01-19 15:08:44 +01:00
Clifford Wolf 615c2e136e Added equiv_status 2015-01-19 14:20:04 +01:00
Clifford Wolf 76c5d863c5 Added equiv_make command 2015-01-19 13:59:08 +01:00
Clifford Wolf edb3c9d0c4 Renamed extend() to extend_xx(), changed most users to extend_u0() 2014-12-24 09:51:17 +01:00
Clifford Wolf fe829bdbdc Added log_warning() API 2014-11-09 10:44:23 +01:00
Clifford Wolf 7cb0d3aa1a Renamed TRUE/FALSE to CONST_TRUE/CONST_FALSE because of name collision on Win32 2014-10-10 17:07:24 +02:00
Clifford Wolf 4569a747f8 Renamed SIZE() to GetSize() because of name collision on Win32 2014-10-10 17:07:24 +02:00
Clifford Wolf f9a307a50b namespace Yosys 2014-09-27 16:17:53 +02:00