N. Engelhardt
0f13fc6bc7
fix lookup of mangled path names
2024-10-16 13:56:36 +02:00
Jannis Harder
117fb26c68
Merge pull request #298 from YosysHQ/george/smtbmc_paths
...
smtbmc: match on full property paths instead of just names
2024-10-07 20:36:27 +02:00
Jannis Harder
62d17081bf
Merge pull request #276 from YosysHQ/krys/test-furo-ys
...
Use furo-ys
2024-09-27 14:21:07 +02:00
George Rennie
9583985d06
smtbmc: match on full property paths instead of just names
...
* to address #296
* this also required some changes to the formatting of the output from
smtbmc to allow more unambiguous parsing, so corresponds to a matching
change in yosys
2024-09-24 03:13:07 +01:00
Miodrag Milanović
d9a5845323
Merge pull request #297 from jix/imctk-eqy-engine
...
Add support for the imctk-eqy-engine
2024-09-16 17:39:53 +02:00
Jannis Harder
8bd07192ac
Merge pull request #294 from YosysHQ/george/aigbmc_docs
...
docs: fix reference to aigbmc engine option
2024-09-09 10:20:54 +02:00
Jannis Harder
b8a001eab2
Add support for the imctk-eqy-engine
...
This is not added to the documentation, as this is currently intended
for internal use only.
2024-09-08 16:04:26 +02:00
Miodrag Milanović
67a7821946
CI force fast runner
2024-08-19 11:26:44 +02:00
George Rennie
07b9b7cbb8
docs: fix reference to aigbmc engine option
2024-08-01 17:34:54 +01:00
Miodrag Milanović
61ca4de2da
Merge pull request #284 from jix/remember-installed-version
...
Add --version option based on git describe
2024-07-08 19:05:16 +02:00
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
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
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
