George Rennie
ff98e51c13
Merge pull request #317 from SeddonShen/main
...
feat(sby_engine_aiger): add rIC3 support for BMC mode
2025-03-26 10:17:15 +01:00
SeddonShen
ca93e43cec
feat(sby_engine_aiger): add rIC3 support for BMC mode
2025-03-18 16:06:16 +08:00
George Rennie
20ee439df9
Merge pull request #313 from gipsyh/rIC3
...
Support rIC3 model checker as backend
2025-03-14 15:13:06 +01:00
Yuheng Su
fc0afb04c5
Set minimum rIC3 version to 1.35
2025-03-14 22:00:09 +08:00
N. Engelhardt
9675d158ce
Merge pull request #264 from YosysHQ/krys/vhd_example
...
Add formal_bind example
2025-03-03 15:20:59 +00:00
Miodrag Milanović
b6be8ad0fc
Merge pull request #311 from sporniket/patch-2
...
[docs] Fixes instructions for installing boolector
2025-03-03 16:15:59 +01:00
N. Engelhardt
44c44097f8
Merge pull request #310 from sporniket/patch-1
...
[docs] instruct to clone yosys with '--recurse-submodules'
2025-03-03 15:11:05 +00:00
N. Engelhardt
4d92762d5a
Merge pull request #278 from YosysHQ/krys/docs_verific
...
Add note on docs to clarify verific support
2025-03-03 15:09:36 +00:00
Yuheng Su
8da7174b16
update rIC3 backend
...
Signed-off-by: Yuheng Su <gipsyh.icu@gmail.com>
2024-12-17 04:41:58 +00:00
Yuheng Su
daf4e4cb39
Support rIC3 as backend
...
Signed-off-by: Yuheng Su <gipsyh.icu@gmail.com>
2024-12-16 11:02:45 +00:00
David SPORN
8885582e3c
[docs] Fixes instructions for installing boolector
...
There is a `build` folder where `bin\btorsim` is generated
2024-11-19 07:20:08 +01:00
David SPORN
7fc7ed38ae
[docs] instruct to clone yosys with '--recurse-submodules'
...
Without using '--recurse-submodule', make fails to retrieve them before building.
2024-11-19 06:58:01 +01:00
N. Engelhardt
26b387466d
Merge pull request #308 from YosysHQ/krys/drop_ilang
2024-11-07 17:33:53 +01:00
Krystine Sherwin
176e59c3d8
Replace (read_)ilang with (read_)rtlil
2024-11-05 12:55:09 +13:00
N. Engelhardt
daed0e1544
Merge pull request #302 from YosysHQ/fix_mangle_lookup
2024-10-17 11:15:01 +02:00
Miodrag Milanovic
94d1d0aa2f
enable extensions
2024-10-16 17:14:42 +02:00
N. Engelhardt
e84cc443bd
add non-verific name mangling regression test
2024-10-16 15:05:02 +02:00
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
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
