luke/yosys
1
0
Fork 0
mirror of https://github.com/YosysHQ/yosys.git synced 2026-08-22 06:07:26 +02:00
Code Issues Packages Projects Releases Wiki Activity
17,465 Commits 140 Branches 70 Tags
emil/dlatchlibmap
Commit Graph
61 Commits
Author SHA1 Message Date
Codexplorer e41b969da2 Refactored uses of log_id() 2026-05-08 20:59:24 -07:00
Robert O'Callahan a7c46f7b4a Remove .c_str() calls from parameters to log_warning()/log_warning_noprefix() 2025-09-16 23:02:16 +00:00
Robert O'Callahan 5ac6858f26 Remove .c_str() from log_cmd_error() and log_file_error() parameters 2025-09-16 22:59:08 +00:00
Robert O'Callahan e0ae7b7af4 Remove .c_str() calls from log()/log_error() 
There are some leftovers, but this is an easy regex-based approach that removes most of them.
 2025-09-11 20:59:37 +00:00
Robert O'Callahan c7df6954b9 Remove .c_str() from stringf parameters 2025-09-01 23:34:42 +00:00
Krystine Sherwin 3959d19291 Reapply "Add groups to command reference" 
This reverts commit 81f87ce6ed.
 2025-08-06 13:52:12 +12:00
N. Engelhardt 81f87ce6ed Revert "Add groups to command reference" 2025-07-23 14:41:49 +00:00
Krystine Sherwin 92ab125113 cmdref: Assigning cmds to formal group 
Give formal index a proper title.
Use `Pass::formatted_help()` to assign the group, but still return `false` because the help text still comes from `Pass::help()`.
Tidy up some of the affected files' includes to make use of the shared `yosys.h` includes.
 2025-07-21 10:35:56 +12:00
Miodrag Milanovic 5801152779 Deprecate gcc-4.8 2023-01-11 09:54:19 +01:00
Miodrag Milanovic e3c0fd8b10 qbfsat support for cvc5, fixes #3608 2023-01-09 16:14:01 +01:00
KrystalDelusion 9465b2af95 Fitting help messages to 80 character width 
Uses the regex below to search (using vscode):
	^\t\tlog\("(.{10,}(?<!\\n)|.{81,}\\n)"\);

Finds any log messages double indented (which help messages are)
and checks if *either* there are is no newline character at the end,
*or* the number of characters before the newline is more than 80.
 2022-08-24 10:40:57 +12:00
Miodrag Milanovic f4a1906721 support file locations containing spaces 2022-08-08 20:30:50 +02:00
Mohamed A. Bamakhrama 1822be8792 Observe $TMPDIR variable when creating tmp files 
POSIX defines $TMPDIR as containing the pathname of the directory where
programs can create temporary files. On most systems, this variable points to
"/tmp". However, on some systems it can point to a different location.
Without respecting this variable, yosys fails to run on such systems.

Signed-off-by: Mohamed A. Bamakhrama <[email protected]>
 2022-05-27 15:06:53 +02:00
Alberto Gonzalez 2f786fcfac qbfsat: Add -solver-option option. 2020-07-20 21:54:56 +00: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
Alberto GonzalezandMarcelina Kościelnicka 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 <[email protected]>
 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
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 GonzalezandClaire Wolf e1fedf054e qbfsat: Avoid instantiating AttrObjects directly. 
Co-Authored-By: Claire Wolf <[email protected]>
 2020-06-21 02:16:11 +00:00
Alberto GonzalezandClaire Wolf 08cede4669 qbfsat: Simplify solution format and replace SigBit::str() with log_signal(). 
Co-Authored-By: Claire Wolf <[email protected]>
 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 7191dd16f9 Use C++11 final/override keywords. 2020-06-18 23:34:52 +00: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
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 586739ecf3 qbfsat: Fix illegal use of 'stdout' identifier 
Signed-off-by: David Shah <[email protected]>
 2020-04-17 08:42:39 +01: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 GonzalezandN. Engelhardt 6af8b767b4 Use log_push() and log_pop() and show the satisfiable model when -specialize is not specified. 
Co-Authored-By: N. Engelhardt <[email protected]>
 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 GonzalezandClaire Wolf 125a583c57 Use the -duplicate option rather than -save and -load with an explicit name. 
Co-Authored-By: Claire Wolf <[email protected]>
 2020-04-04 22:13:26 +00:00
Alberto GonzalezandClaire Wolf 86fc49a9d6 Use internal run_command() API instead of popen(). 
Co-Authored-By: Claire Wolf <[email protected]>
 2020-04-04 22:13:26 +00:00