riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
11,923 Commits 81 Branches 48 Tags 64 MiB
Commit Graph

11923 Commits

Author SHA1 Message Date
github-actions[bot] 4f4cff0080 Bump version 2022-10-21 00:23:12 +00:00
Jannis Harder 0f96ae5990 Add smtmap.v describing the smt2 backend's behavior for undef bits 
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.
 2022-10-20 15:48:18 +02:00
Claire Xenia Wolf be1a12595a Add missing log_dump handler for std::vector<> 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2022-10-20 13:50:25 +02:00
Jannis Harder 96029400cb smtbmc: Do not assume skipped assertions when loading a witness trace 
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.
 2022-10-20 13:49:47 +02:00
github-actions[bot] 6781746872 Bump version 2022-10-20 00:25:10 +00:00
Emil J 8859d801c8
Temporal induction counterexample loop detection (#3504) 
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.
 2022-10-19 12:20:12 +02:00
Jannis Harder f4ede15d68
Merge pull request #3514 from jix/smtbmc-kind-witness-fix 
smtbmc: Fix witness handling for k-induction failures
 2022-10-19 11:28:12 +02:00
Jannis Harder 8838b1eaa4 smtbmc: Fix witness handling for k-induction failures 
The "uninitialized" value is a _list_ of chunks that are part of the
initial state for the witness trace.
 2022-10-18 19:51:36 +02:00
Lloyd Parkes 7dcc9c664e And another place we need to lseek() after dup(). 2022-10-16 12:50:49 +13:00
Lloyd Parkes 635aa2a3fc Forcibly set the current seek location of gz files that we are accessing 
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.
 2022-10-16 12:36:00 +13:00
github-actions[bot] d02ae8f2fc Bump version 2022-10-15 00:24:26 +00:00
Miodrag Milanović fc53a0a5c2
Merge pull request #3511 from YosysHQ/improve_edif 
verific: enable import all cells
 2022-10-14 17:53:56 +02:00
Miodrag Milanovic 48628fbf5a Skip verific primitives and operators import by default 2022-10-14 17:41:24 +02:00
Miodrag Milanovic 922f8b614a Add option to import all cells from all libraries 2022-10-14 16:54:57 +02:00
github-actions[bot] 2e837956dc Bump version 2022-10-13 00:25:23 +00:00
Jannis Harder 33a2773de0
Merge pull request #3510 from jix/ff_witness_fixes 
smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
 2022-10-12 20:50:00 +02:00
Jannis Harder 4d334fd3e3 smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs 
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.
 2022-10-12 19:48:36 +02:00
Aki Van Ness f35c062354 github: issues: added an OS dropdown to the issue template 2022-10-12 09:31:32 -04:00
Jannis Harder fcf742837e
Merge pull request #3502 from jix/equiv_opt_fixes 
equiv_opt and clk2fflogic fixes
 2022-10-11 12:02:16 +02:00
github-actions[bot] 5c7a1eda92 Bump version 2022-10-11 00:24:29 +00:00
Miodrag Milanović 00bef0b534
Merge pull request #3508 from YosysHQ/aki/rm_protobuf 
backends: protobuf: removed protobuf backend
 2022-10-10 18:08:51 +02:00
Aki Van Ness 7a73133c9f
backends: protobuf: removed protobuf backend 2022-10-10 10:41:11 -04:00
Miodrag Milanovic 03df1ac72b fix whitespace 2022-10-10 16:31:29 +02:00
Miodrag Milanović e8ce9442a6
Merge pull request #3452 from ALGCDG/master 
Add BLIF names command input plane size check
 2022-10-10 16:29:27 +02:00
Miodrag Milanović d68013811f
Merge pull request #3507 from YosysHQ/claire/verificlibopt 
Fix handling of verific -L options, add implicit "-L work"
 2022-10-10 07:50:57 +02:00
Claire Xenia Wolf 090228a6a1 Fix handling of verific -L options, add implicit "-L work" 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2022-10-10 00:47:42 +02:00
github-actions[bot] 0e13d7e4c7 Bump version 2022-10-08 00:22:25 +00:00
Jannis Harder ae1a24d0c4
Merge pull request #3503 from jix/abort_on_log_error 
Add YOSYS_ABORT_ON_LOG_ERROR environment variable for debugging.
 2022-10-07 21:30:26 +02:00
Jannis Harder 0113f44faa Reenable existing equiv_opt tests 2022-10-07 16:04:51 +02:00
Jannis Harder 81906aa627 Fix tests for check in equiv_opt 2022-10-07 16:04:51 +02:00
Claire Xenia Wolf 0516307637 Add "check -assert" to equiv_opt 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2022-10-07 16:04:51 +02:00
Claire Xenia Wolf f0478c520d Re-enable opt_dff_sr equiv_opt checks 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2022-10-07 16:04:51 +02:00
Claire Xenia Wolf afa5e6bb53 Exclude primary inputs from quiv_make rewiring 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2022-10-07 16:04:51 +02:00
Claire Xenia Wolf 381ce66f58 Revert "Merge pull request #641 from tklam/master" 
This reverts commit 08be796cb8, reversing
changes made to 38dbb44fa0.

This fixes #2728. PR #641 did not actually "fix" #639.

The actual issue in #639 is not equiv_make, but assumptions in equiv_simple
that are not true for the test case provided in #639.
 2022-10-07 16:04:51 +02:00
Jannis Harder 925f92918a clk2fflogic: Always correctly handle simultaneously changing signals 
This is a complete rewrite of the FF replacing code.

The previous implementation tried to implement the negative hold time by
wrapping async control signals individually with pulse stretching. This
did not correctly model the interaction between different simultaneously
changing inputs (e.g. a falling ALOAD together with a changing AD would
load the changed AD instead of the value AD had when ALOAD was high; a
falling CLR could mask a raising SET for one cycle; etc.).

The new approach first has the logic for all updates using only sampled
values followed by the logic for all updates using only current values.
That way, e.g., a falling ALOAD will load the sampled AD value but a
still active ALOAD will load the current AD value.

The new code also has deterministic behavior for the initial state: no
operation is active when that operation would depend on a specific
previous signal value. This also means clk2fflogic will no longer
generate any additional uninitialized FFs.

I also documented the negative hold time behavior in the help message,
copying the relevant part from async2sync's help messages.
 2022-10-07 16:04:51 +02:00
Jannis Harder ac906d15ce Add YOSYS_ABORT_ON_LOG_ERROR environment variable for debugging. 2022-10-07 15:02:33 +02:00
github-actions[bot] c4a52b1b02 Bump version 2022-10-06 00:24:43 +00:00
Miodrag Milanovic a5172df9e9 Next dev cycle 2022-10-05 11:32:11 +02:00
Miodrag Milanovic f109fa3d4c Release version 0.22 2022-10-05 11:30:38 +02:00
Miodrag Milanovic 7db26a8e59 Update CHANGELOG 2022-10-05 11:28:48 +02:00
Miodrag Milanović 11203815a8
Merge pull request #3500 from nakengelhardt/mutate_warn_not_enough 
mutate: warn if less mutations possible than number requested
 2022-10-05 11:28:20 +02:00
N. Engelhardt 47e73826e0 mutate: warn if less mutations possible than number requested 2022-10-05 10:59:38 +02:00
Miodrag Milanović b5d3920bf5
Merge pull request #3499 from YosysHQ/micko/verific_edif 
Add support for EDIF file reading using Verific
 2022-10-05 08:20:03 +02:00
github-actions[bot] 620af8b663 Bump version 2022-10-05 00:26:07 +00:00
Miodrag Milanovic 1a6f10e8ba Add support for EDIF file reading using Verific 2022-10-04 09:18:44 +02:00
Miodrag Milanović f5e2c0a498
Merge pull request #3494 from YosysHQ/micko/verific_attributes 
Handle attributes imported from verific
 2022-10-04 08:23:52 +02:00
Archie d29606532a Changing error reason string to be based on lut input plane limit constant. 2022-10-02 22:05:51 +02:00
Miodrag Milanovic 43267dec99 support file content redirection for verific frontened 2022-09-28 15:56:46 +02:00
Miodrag Milanovic b45517f7b7 Add comment for future self 2022-09-28 14:45:39 +02:00
Miodrag Milanovic f54ac8a6d6 Handle attributes imported from verific 2022-09-28 08:51:26 +02:00