3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-22 04:46:37 +00:00
Commit graph

584 commits

Author SHA1 Message Date
Jannis Harder
eeee1a1ec5 tools/cexenum: Avoid buffering smtbmc's --progress stderr output
We were discarding that output anyway and before YosysHQ/mau#5 this
could lead to the mau internal `stderr.readline()` failing.
2023-12-14 17:32:36 +01:00
Jannis Harder
aa2a96d7c9 tools/cexenum: Fix type annotations
With this it now passes pyright's strict mode
2023-12-14 17:32:36 +01: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
Claire Xen
8c4e2da264
Merge pull request #243 from jix/krys/argparse_docs
Add sphinx-argparse to generate usage
2023-07-18 16:28:11 +02:00
Claire Xen
ffa53a32c1
Merge branch 'master' into krys/argparse_docs 2023-07-18 16:27:12 +02:00
Claire Xen
5ee5a788fe
Merge pull request #241 from YosysHQ/krys/argparse_docs
Add sphinx-argparse to generate usage
2023-07-18 16:24:57 +02:00
Claire Xen
df18dbfbe1
Merge pull request #242 from jix/fix-autotune-crash
autotune: Fix crash on no-engine error path
2023-07-18 16:20:26 +02:00
N. Engelhardt
79e6ecf10a
Merge pull request #245 from jix/fix-jobserver-deadlock 2023-07-17 16:36:26 +02:00
Jannis Harder
edbc0548af Fix deadlock with parallel SBY procs each with parallel tasks
When multiple SBY processes run in parallel (from a Makefile or other
job-server aware tool) and each SBY process runs tasks in parallel, each
with enough tasks to be limited by the total job count, it is possible
for the processes to race in such a way that every SBY process's helper
process is in a blocking read from the job-server but a job-token would
only become available as soon as any SBY process exits.

In that situation SBY doesn't actually need the job-token anymore and
only previously requested it as there was opportunity for parallelism.
It would immediatly return the token as soon as it is acquired. That's
usually sufficient to deal with no-longer-needed-but-requested tokens,
but when SBY is done, it needs to return the job-token held by the
parent process ASAP which it can only do by actually exiting, so we need
to interrupt the blocking read of SBY's helper process.

This could be done by sending a signal to the helper process, except
that Python made the decision in 3.5 to have automatic EINTR retry loops
around most system calls with no opt-out. That was part of the reason to
go with this specifc helper process design that avoids interrupting a
blocking read in the first place.

Using an exception raised from the signal handler instead might lose a
token when the signal arrives after the read returns, but before the
token is stored in a variable. You cannot recover from a lost token in
the context of the job-server protocol, so that's not an option. (This
can't happen with recent Python versions but that would depend on
undocumented behavior that could plausibly change again.)

Thankfully the only case where we need to interrupt the read is when SBY
is about to exit and will not request any further tokens. This allows us
to use a signal handler that uses dup2 to close and replace the
read-from fd with one that already is at EOF, making the next retry
return immediatly. (If we'd need to interrupt a read and continue
running we could also do this but the fd shuffling would be more
involved.)
2023-07-17 15:29:17 +02:00
Claire Xen
fbbbab235f
Merge pull request #240 from YosysHQ/claire/aigfolds
Add "pdr -d" engine support (and aigfolds config option)
2023-06-28 11:11:36 +02:00
Jannis Harder
4d1ac0115c
Merge pull request #244 from jix/smtbmc-cover-keepgoing 2023-06-26 16:35:56 +02:00
Jannis Harder
28c053bd94 smtbmc: Allow using --keep-going in cover mode
See YosysHQ/yosys#3816 for the smtbmc change that made --keep-going do
something in cover mode
2023-06-23 10:34:03 +02:00
Jannis Harder
c52acf2a1f docs: Make sphinx-argparse work independently of sphinx's cwd 2023-06-19 11:39:37 +02:00
Krystine Sherwin
1a4c2a57ad
Add sbysrc to path during docs build 2023-06-19 21:39:07 +12:00
Jannis Harder
0d6a70e137 autotune: Fix crash on no-engine error path 2023-06-19 11:21:49 +02:00
Krystine Sherwin
27e20fd5c3
Add sphinx-argparse to generate usage
Move parser generation into a seperate file to avoid import issues with bad python modules during docs gen.
With the requirements.txt provided to readthedocs, there shouldn't need to be any other changes?
Also I've never been able to run `make test` so I'm not actually sure if the changes break sby, but they shouldn't.
2023-06-13 11:40:28 +12:00
Claire Xenia Wolf
f692eff845 Add support for "abc pdr -d" engine
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2023-06-07 22:21:06 +02:00
Claire Xenia Wolf
8b3ba68845 Add aigfolds option
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2023-06-07 22:05:17 +02:00
Claire Xen
c027aea3db
Merge pull request #237 from jix/sphinx-theme
Change Sphinx theme to "furo"
2023-06-04 21:33:52 +02:00
Claire Xen
c562d65e75
Merge pull request #239 from YosysHQ/claire/aigvmap
Add aigvmap and aigsyms options
2023-06-04 18:53:16 +02:00
Claire Xenia Wolf
7d60a3ba34 Add aigvmap and aigsyms options
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2023-06-03 22:16:35 +02:00
Claire Xen
81b9de988b
Merge pull request #238 from YosysHQ/claire/nowitrename
Make call to "witness -rename" optional (default=on)
2023-06-02 13:11:41 +02:00
Claire Xenia Wolf
f49c9ebb29 Make call to "witness -rename" optional (default=on)
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2023-06-02 13:04:45 +02:00
Krystine Sherwin
36e7a72586
Adding prep mode and skip_prep option
Allows for generating a design_prep model which can then be used by multiple distinct sby runs.
2023-05-16 17:42:53 +12:00
Jannis Harder
cb968ea2bb Update .readthedocs.yaml 2023-05-08 11:33:14 +02:00
Jannis Harder
513d0d4288 Change Sphinx theme to "furo" 2023-05-03 16:56:09 +02:00
Jannis Harder
74f33880bd
Merge pull request #232 from dlmiles/win-qol-cleanopt
-f clean: QoL improvement on Windows concerning file/dir removal locking
2023-02-20 19:48:36 +01:00
Darryl L. Miles
fa5bc957c1 -f clean: QoL improvement on Windows concerning file/dir removal locking
When using the -f argument be more forgiving with the expectation of a clean
workspace and the expectation of the new sby run being responsible for
directory creation.

This is a usability and quality of life improvement for Windows users where
the OS can implement file and directory locking implicitly.  In the EDA world
it is common to have multiple tools in use at any one time and it can become
tortious to have to close files / exit 3rd party applications to release
locking so sby is happy to rerun.

This change will prevent sby claiming a terminal error has occurred when it
fails to create a directory that already exists.  It also now considers the
environment to be 'clean' (as per -f) if all the non-directory elements of
the file tree have been deleted, leaving potentially an empty a skeleton of
directories.
2023-02-18 09:36:18 +00:00
Miodrag Milanović
2cd0f6f71c
Try fixing GH action 2023-02-13 10:33:46 +01:00
Miodrag Milanović
8eaeca9aa4
Update GH action 2023-02-13 10:24:24 +01:00
N. Engelhardt
81ee5fdd5a
update prerequisites 2023-02-08 17:59:26 +01:00
Jannis Harder
466ab84745
Merge pull request #230 from jix/append_assume_default
append_assume: Make `append_assume on` the default for now
2023-02-08 14:42:20 +01:00
Jannis Harder
c5dce57067 append_assume: Make append_assume on the default for now
Having `append_assume off` needs `vcd_sim on` to not be ignored with a
warning and `vcd_sim off` is still the default.
2023-02-08 14:18:52 +01:00
Jannis Harder
37d1234e38
Merge pull request #228 from jix/docs-updates
Docs updates
2023-02-06 22:10:38 +01:00
Jannis Harder
7a3b88ca67 docs: Document new sim related options 2023-02-06 16:55:19 +01:00
Jannis Harder
6d1ef8b5a0 docs: Yices is still recommended 2023-02-06 16:54:37 +01:00
Jannis Harder
7d3f0d50a5
Merge pull request #227 from jix/sim_traces
Unified trace generation using Yosys's sim command across all engines
2023-01-25 10:53:21 +01:00
Jannis Harder
f14aaa57c4 avy: Fold aiger model using abc to support assumptions 2023-01-11 18:36:06 +01:00
Jannis Harder
6398938e6a Enable yosys sim support for clock signals in hierarchical designs 2023-01-11 18:02:45 +01:00
Jannis Harder
06c36d5bb0 Support "fifo:" make jobserver auth 2023-01-10 18:42:26 +01:00