aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Bump versiongithub-actions[bot]2022-11-011-1/+1
|
* Merge pull request #3533 from YosysHQ/micko/libertyMiodrag Milanović2022-10-312-1/+84
|\ | | | | Liberty file support using verific library
| * Add additional help infoMiodrag Milanovic2022-10-311-0/+2
| |
| * Enable importing blackbox modules onlyMiodrag Milanovic2022-10-311-1/+33
| |
| * Support for reading liberty files using verificMiodrag Milanovic2022-10-312-1/+50
| |
* | Merge pull request #3534 from mmicko/win32_pluginsMiodrag Milanović2022-10-313-6/+942
|\ \ | |/ |/| Plugin support for mingw windows builds
| * Windows plugin build supportMiodrag Milanovic2022-10-311-6/+28
| |
| * Add dlfcn library for win32Miodrag Milanovic2022-10-282-0/+914
| |
* | Bump versiongithub-actions[bot]2022-10-311-1/+1
| |
* | Add missing log_dump_val_worker forward declarationsClaire Xenia Wolf2022-10-301-0/+5
| | | | | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* | Bump versiongithub-actions[bot]2022-10-301-1/+1
| |
* | Merge pull request #3530 from jix/simlib-mux-fixJannis Harder2022-10-291-4/+2
|\ \ | |/ |/| simlib: Simplify recently changed $mux model
| * simlib: Simplify recently changed $mux modelJannis Harder2022-10-281-4/+2
|/ | | | | | The use of a procedural continuous assignment introduced in #3526 was unintended and is completely unnecessary for the actual change of that PR.
* Bump versiongithub-actions[bot]2022-10-251-1/+1
|
* Merge pull request #3528 from YosysHQ/claire/crossbitsClaire Xen2022-10-251-4/+32
|\ | | | | Add miter -cross option
| * Add miter -cross optionClaire Xenia Wolf2022-10-241-4/+32
|/
* Merge pull request #3526 from jix/mux-simlib-evalJannis Harder2022-10-245-15/+38
|\ | | | | Consistent $mux undef handling
| * Consistent $mux undef handlingJannis Harder2022-10-245-15/+38
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Change simlib's $mux cell to use the ternary operator as $_MUX_ already does * Stop opt_expr -keepdc from changing S=x to S=0 * Change const eval of $mux and $pmux to match the updated simlib (fixes sim) * The sat behavior of $mux already matches the updated simlib The verilog frontend uses $mux for the ternary operators and this changes all interpreations of the $mux cell (that I found) to match the verilog simulation behavior for the ternary operator. For 'if' and 'case' expressions the frontend may also use $mux but uses $eqx if the verilog simulation behavior is requested with the '-ifx' option. For $pmux there is a remaining mismatch between the sat behavior and the simlib behavior. Resolving this requires more discussion, as the $pmux cell does not directly correspond to a specific verilog construct.
* | Merge pull request #3518 from jix/smtmapJannis Harder2022-10-242-0/+29
|\ \ | | | | | | Add smtmap.v describing the smt2 backend's behavior for undef bits
| * | Add smtmap.v describing the smt2 backend's behavior for undef bitsJannis Harder2022-10-202-0/+29
| | | | | | | | | | | | | | | | | | | | | | | | | | | Some builtin cells have an undefined (x) output even when all inputs are defined. This is not natively supported by the formal backends which will produce a fully defined value instead. This can lead to issues when combining different backends in a formal flow. To work around these, this adds a file containing verilog implementation of cells matching the fully defined behavior implemented by the smt2 backend.
* | | Merge pull request #3517 from jix/smtbmc-witness-no-assume-skippedJannis Harder2022-10-241-3/+0
|\ \ \ | | | | | | | | smtbmc: Do not assume skipped assertions when loading a witness trace
| * | | smtbmc: Do not assume skipped assertions when loading a witness traceJannis Harder2022-10-201-3/+0
| | | | | | | | | | | | | | | | | | | | | | | | This is not valid when the prefix of a trace already violates assertions. This can happen when the trace generating solver doesn't look for a minimal length counterexample.
* | | | Merge pull request #3523 from lparkes/basenameMiodrag Milanović2022-10-241-1/+1
|\ \ \ \ | | | | | | | | | | Replace GNU specific invocation of basename(1) with the equivalent POSIX one
| * | | | Replace GNU specific invocation of basename(1) with the equivalentLloyd Parkes2022-10-231-1/+1
| | | | | | | | | | | | | | | | | | | | POSIX one. The tests now complete on BSD as well as GNU/Linux.
* | | | | Merge pull request #3512 from lparkes/fstapiMiodrag Milanović2022-10-241-0/+2
|\ \ \ \ \ | | | | | | | | | | | | Failure to read FST files on *BSD systems
| * | | | | And another place we need to lseek() after dup().Lloyd Parkes2022-10-161-0/+1
| | | | | |
| * | | | | Forcibly set the current seek location of gz files that we are accessingLloyd Parkes2022-10-161-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | via dup(fileno());gzdopen() because stdio might have buffered data from the underlying file meaning that the underlying seek position isn't what we think it is.
* | | | | | Update CodeQL actionMiodrag Milanovic2022-10-241-1/+1
| | | | | |
* | | | | | Bump versiongithub-actions[bot]2022-10-221-1/+1
| |/ / / / |/| | | |
* | | | | Merge pull request #3521 from YosysHQ/ci_upgradeMiodrag Milanović2022-10-215-14/+14
|\ \ \ \ \ | |_|_|_|/ |/| | | | Update versions of CI actions used
| * | | | Update versions of CI actions usedMiodrag Milanovic2022-10-215-14/+14
|/ / / /
* | | / Bump versiongithub-actions[bot]2022-10-211-1/+1
| |_|/ |/| |
* | | Add missing log_dump handler for std::vector<>Claire Xenia Wolf2022-10-201-0/+12
| |/ |/| | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* | Bump versiongithub-actions[bot]2022-10-201-1/+1
| |
* | Temporal induction counterexample loop detection (#3504)Emil J2022-10-191-1/+36
| | | | | | I have added an optional flag to smtbmc that causes failed temporal induction counterexample traces to be checked for duplicate states and reported to the user, since loops in the counterexample mean that increasing the induction depth won't help prove a design's safety properties.
* | Merge pull request #3514 from jix/smtbmc-kind-witness-fixJannis Harder2022-10-191-1/+1
|\ \ | | | | | | smtbmc: Fix witness handling for k-induction failures
| * | smtbmc: Fix witness handling for k-induction failuresJannis Harder2022-10-181-1/+1
| | | | | | | | | | | | | | | The "uninitialized" value is a _list_ of chunks that are part of the initial state for the witness trace.
* | | Bump versiongithub-actions[bot]2022-10-151-1/+1
| | |
* | | Merge pull request #3511 from YosysHQ/improve_edifMiodrag Milanović2022-10-141-1/+31
|\ \ \ | |/ / |/| | verific: enable import all cells
| * | Skip verific primitives and operators import by defaultMiodrag Milanovic2022-10-141-0/+1
| | |
| * | Add option to import all cells from all librariesMiodrag Milanovic2022-10-141-1/+30
|/ /
* | Bump versiongithub-actions[bot]2022-10-131-1/+1
| |
* | Merge pull request #3510 from jix/ff_witness_fixesJannis Harder2022-10-124-12/+29
|\ \ | | | | | | smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
| * | smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFsJannis Harder2022-10-124-12/+29
|/ / | | | | | | | | | | | | The witness metadata was missing fine grained FFs completely and for coarse grained FFs where the output connection has multiple chunks it lacked the offset of the chunk within the SMT expression. This fixes both, the later by adding an "smtoffset" field to the metadata.
* / github: issues: added an OS dropdown to the issue templateAki Van Ness2022-10-121-1/+13
|/
* Merge pull request #3502 from jix/equiv_opt_fixesJannis Harder2022-10-1128-267/+207
|\ | | | | equiv_opt and clk2fflogic fixes
| * Reenable existing equiv_opt testsJannis Harder2022-10-0713-54/+52
| |
| * Fix tests for check in equiv_optJannis Harder2022-10-0713-15/+31
| |
| * Add "check -assert" to equiv_optClaire Xenia Wolf2022-10-071-1/+13
| | | | | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
| * Re-enable opt_dff_sr equiv_opt checksClaire Xenia Wolf2022-10-071-13/+12
| | | | | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
generated by cgit v1.2.3 (git 2.25.1) at 2025-09-10 13:36:16 +0000