Jannis Harder
8709c8a8ee
Add --version option based on git describe
2024-07-08 18:39:23 +02:00
Jannis Harder
c9e3b8224a
Merge pull request #275 from YosysHQ/micko/pr_template
...
Add PR template
2024-06-14 18:18:25 +02:00
Krystine Sherwin
0fab912005
Docs: Use sby role shortcut
2024-06-10 18:46:31 +12:00
Krystine Sherwin
a3844d4a30
Docs: Use sby lexer
2024-06-10 18:41:15 +12:00
Krystine Sherwin
5426bee107
Use furo-ys
2024-05-14 12:54:30 +12:00
Krystine Sherwin
7f1853bd78
Add note on docs to clarify verific support
...
Having a verific license does not provide access to the verific frontend. This helps to make that clearer.
2024-05-14 12:25:29 +12:00
Miodrag Milanović
641d5d55fa
Merge pull request #277 from YosysHQ/krys/fix-ci
...
Fix failing `build_verific`
2024-05-09 07:27:12 +02:00
Krystine Sherwin
0a6a484760
ci: Checkout Yosys with submodules
2024-05-09 13:12:36 +12:00
Miodrag Milanovic
d8904f47ea
Add PR template
2024-05-08 11:13:56 +02:00
Jannis Harder
7dd287f287
Merge pull request #274 from jix/abc-prep
...
abc: Support arbitrary prep abc commands
2024-04-24 09:43:00 +02:00
Jannis Harder
e0dda21555
abc: Support arbitrary prep abc commands
2024-04-19 16:40:30 +02:00
Miodrag Milanović
415f404513
Merge pull request #273 from YosysHQ/ci
...
Update CI scripts
2024-04-10 18:39:05 +02:00
Miodrag Milanovic
dfd4c8c734
Update CI scripts
2024-04-10 13:36:05 +02:00
N. Engelhardt
b84cd93ea0
Merge pull request #271 from YosysHQ/aiju/issue-269
...
Fixes issue #269 by removing an erroneous "if sbyfile" check.
2024-04-05 13:02:13 +02:00
Miodrag Milanović
ebfb2ee7e0
Merge pull request #270 from YosysHQ/aiju/fix-timeout-test
...
Replace the 'primes' test in junit_timeout_error.sby with a new test …
2024-04-04 09:00:13 +02:00
Emily Schmidt
da46e1984b
Fixes issue #269 by removing an erroneous "if sbyfile" check.
...
This commit removes an erroneous "if sbyfile" that would turn '-f' into a no-op
for stdin input files. Presumably this check was originally intended to handle
the case of stdin input file and no specified workdir (which uses a temporary
workdir). In the current version the check is redundant for this particular
case. The check is erroneous in the case of stdin input file and a specified
workdir, so we simply remove the check.
2024-04-02 13:32:24 +01:00
Emily Schmidt
725038d315
Replace the 'primes' test in junit_timeout_error.sby with a new test that solves a**3 + b**3 == c**3.
...
The old test tried to find two primes that are 7 apart. It is supposed to time
out after 1 second but on newer hardware the test completes too quickly. This
commit replaces it with a new test that tries to find a non-trivial solution to
the diophantine equation a**3 + b**3 == c**3, which is a lot more difficult.
2024-04-02 11:28:54 +01:00
Jannis Harder
e30a0fe611
Merge pull request #268 from YosysHQ/KrystalDelusion-patch-1
...
Update sby_engine_abc.py
2024-03-12 00:37:49 +01:00
KrystalDelusion
6c8b838eb3
Update sby_engine_abc.py
...
ABC will sometimes return negative frame numbers when proving by convergence, e.g.
```
engine_0: Proved output 1 in frame -698905656 (converged).
engine_0: Proved output 4 in frame -698905656 (converged).
```
This change fixes these properties being missed and causing the engine status to return UNKNOWN due to `proved_count != len(proved)`.
2024-03-12 10:48:26 +13:00
Jannis Harder
c73cd3eeea
Merge pull request #267 from jix/sby-status-errormsg
...
Improved CLI behavior when not specifying a config or existing workdir
2024-03-11 17:03:59 +01:00
Jannis Harder
cba77083c3
Print a message when SBY is waiting for a config on stdin
2024-03-11 16:35:03 +01:00
Jannis Harder
fd381ade05
Print an error message when using "--status" with no project specified
2024-03-11 15:37:39 +01:00
Jannis Harder
0c84510cef
Merge pull request #263 from jix/pdr-X
...
Support for "abc --keep-going pdr" via new "pdr -X" mode
2024-03-06 17:07:04 +01:00
Jannis Harder
b6e41a388b
Support for the new anytime schedule in yosys-abc's pdr
2024-03-06 12:26:01 +01:00
Krystine Sherwin
549c5f33f5
Add formal_bind example
...
Demonstrate binding SVA properties to a VHDL design.
Mention example code (with snippets) in section on Verific.
2024-03-05 15:29:08 +13:00
Jannis Harder
d3a6f2d758
Emit status db update from aigsmt
2024-02-20 14:06:43 +01:00
Jannis Harder
6ba762db4c
Support for "abc --keep-going pdr" via new "pdr -X" mode
2024-02-20 14:06:43 +01:00
Jannis Harder
52184e5bf0
Initial support for a multi-task property status database
...
This adds initial support for an sqlite database that is shared across
multiple tasks of a single SBY file and that can track the status of
individual properties.
The amount of information tracked in the database is currently quite
minimal and depends on the engine and options used. This can be
incrementally extended in the future.
The ways in which the information in the database can be queries is even
more limited for this initial version, consisting of a single '--status'
option which lists all properties and their status.
2024-02-20 13:34:58 +01:00
Jannis Harder
5c649c8e75
Merge pull request #260 from jix/prepare-check
...
sby_design: Also track fairness assumptions
2024-02-01 15:34:52 +01:00
Jannis Harder
cde9e57507
Merge pull request #258 from jix/sby_cmd
...
tests: Support testing an installed SBY using the SBY_CMD make variable
2024-01-29 15:16:03 +01:00
Miodrag Milanović
056ced9afd
Merge pull request #261 from YosysHQ/workflows
...
Update workflows
2024-01-29 09:37:25 +01:00
Miodrag Milanovic
44ccad3882
Update workflows
2024-01-29 08:48:29 +01:00
Jannis Harder
40bf8fcb87
sby_design: Also track fairness assumptions
2024-01-24 16:08:31 +01:00
Jannis Harder
bd9e218c4a
Merge pull request #259 from jix/prepare-check
...
Prepare SBY for upcomming `$check` cell support and prevent backend failure for `$print` cells
2024-01-23 10:05:02 +01:00
Jannis Harder
881082c990
sby_design: Discover properties represented using $check cells
2024-01-22 18:11:16 +01:00
Jannis Harder
1eeb6f3f0b
Delete $print cells in the backend flows
...
They are only useful and supported for the simulation that is run with
the output of the prep flow, not the output of the backend flows.
2024-01-22 18:10:00 +01:00
Jannis Harder
6f0f2645c2
tests: Support testing an installed SBY using the SBY_CMD make variable
2024-01-19 14:51:16 +01:00
N. Engelhardt
130aa37ed1
Merge pull request #254 from daxzio/prefix_fix
...
Fix PREFIX in makefile to accept environment variable, if set
2024-01-15 16:11:34 +01:00
Dave Keeshan
6e97cea07f
Fix PREFIX in makefile to accept environment variable, if set
2023-12-02 00:05:05 +00:00
Jannis Harder
f0f140c83c
Merge pull request #252 from jix/cexenum
...
Add aigcxemin and cexenum.py tools
2023-11-20 17:04:02 +01:00
Jannis Harder
040b8deef2
Add aigcxemin and cexenum.py tools
2023-11-16 13:46:25 +01:00
Jannis Harder
9e35ec9948
Merge pull request #250 from jix/dft-data-diode
2023-10-02 16:59:16 +02:00
Jannis Harder
5b1f26c1e1
Merge pull request #249 from jix/inductive-cex-sim
2023-10-02 16:58:52 +02:00
Jannis Harder
8581bd3171
Add dft/data_diode example
...
This requires YosysHQ/yosys#3961 and YosysHQ/sby#249 to work
2023-09-28 18:59:27 +02:00
Jannis Harder
36f84b8b9f
smtbmc: Use new -noinitstate option when simulating inductive cex
...
This requires YosysHQ/yosys#3962
2023-09-28 17:38:15 +02:00
Miodrag Milanović
7415abfcfa
Create codeql.yml
2023-09-08 14:09:29 +02:00
Miodrag Milanović
85dd50b92a
Merge pull request #248 from jix/ivy_wip
...
assume_early option to implement cross assumes in IVY
2023-08-25 15:56:54 +02:00
Jannis Harder
884ef862cb
assume_early option to implement cross assumes in IVY
...
Checking IVY's cross assumes requires delaying a subset of assumptions,
which we don't want SBY to undo.
2023-08-11 15:58:55 +02:00
Claire Xen
cf0a761a3a
Merge pull request #246 from YosysHQ/krys/scy_dev
...
Adding prep mode and skip_prep option
2023-07-18 16:46:40 +02:00
Claire Xen
4cddd7a749
Merge branch 'master' into krys/scy_dev
2023-07-18 16:46:09 +02:00
