N. Engelhardt
1cf206fc1c
add cvc5 executable to required tool mapping
2022-07-25 17:01:17 +02:00
N. Engelhardt
3ff2c9affc
avoid erroring out when coarse-grain logic loops can be resolved by mapping to fine grain operators
2022-07-25 16:22:32 +02:00
Jannis Harder
b4dd638311
Merge pull request #197 from YosysHQ/Autotune-grammar-check
...
Autotune grammar/spelling check
2022-07-25 09:53:39 +02:00
Jannis Harder
07d19b202b
Merge pull request #195 from jix/sbyproc-truncated-output
...
Fix a race-condition SbyProc that could truncate output
2022-07-13 17:30:36 +02:00
Jannis Harder
b8a1bdd40a
Merge pull request #193 from jix/abc_pdr_v
...
abc pdr: Enable log output by default
2022-07-13 16:07:04 +02:00
Jannis Harder
5d3f784beb
Fix a race-condition SbyProc that could truncate output
...
Present for a long time, but was not easy to hit. Some of my work in
progress changes made this much more likely and running the complete
test suite in parallel had a good chance of reproducing this for at
least one of the tests.
2022-07-13 16:01:49 +02:00
KrystalDelusion
ca3429e328
Autotune grammar/spelling check
2022-07-11 21:21:31 +12:00
matt venn
4ab610ce87
Update autotune.rst
2022-07-11 11:10:45 +02:00
Jannis Harder
cea760bd52
Merge pull request #194 from jix/autotune_rst_fixes
...
docs: Don't use linebreaks within inline code spans.
2022-07-08 14:46:41 +02:00
Jannis Harder
bc2bb5c863
docs: Don't use linebreaks within inline code spans.
2022-07-08 14:31:57 +02:00
Jannis Harder
92e7eb2e32
abc pdr: Enable log output by default
...
This makes it consistent with the other abc solvers and shows whether
abc pdr is making progress.
2022-07-08 12:36:44 +02:00
Jannis Harder
de43a4c936
Merge pull request #191 from jix/early-readconfig
...
Read config before creating a workdir
2022-07-06 12:05:13 +02:00
Jannis Harder
f42ed5eb10
Merge pull request #192 from jix/win_retcode
...
Make SbyProc hide Windows differences in retcode handling
2022-07-06 12:05:03 +02:00
Jannis Harder
b3b315a473
Make SbyProc hide Windows differences in retcode handling
...
Without this, we don't properly detect missing solver binaries and do
not properly handle the return status of the pono solver.
2022-07-06 11:22:59 +02:00
Jannis Harder
566edad13c
Read config before creating a workdir
...
When using a task name not defined in the config, this now produces an
error before creating an unnecessary workdir for that non-existing task.
2022-07-05 17:20:55 +02:00
Jannis Harder
ff1f87e169
Merge pull request #190 from jix/windows_fixes
...
tests: Windows fixes
2022-07-05 16:09:54 +02:00
Jannis Harder
ea7fc7dc2c
tests: Windows fixes
...
Make tests runnable on Windows, as long as a unix like environment as
e.g. provided by MSYS2 is available.
2022-07-05 15:34:27 +02:00
Jannis Harder
ab98938faa
Merge pull request #187 from jix/const_clocks
...
Test uninitialized FFs with constant clocks and fix btor script for this
2022-07-04 17:47:16 +02:00
Jannis Harder
ff802086b4
test uninited FFs with const clks and fix btor script for this
2022-07-04 14:03:56 +02:00
Jannis Harder
9016031f32
Merge pull request #186 from jix/ff_xinit_opt
...
tests: Test for invalid x-value FF init optimizations
2022-07-04 14:03:06 +02:00
Jannis Harder
e01ac8b848
tests: Test for invalid x-value FF init optimizations
2022-07-04 13:33:39 +02:00
KrystalDelusion
cc27d27c05
More literalincludes
...
Tidying up of newstart.rst and fifo.sv to include as much code as possible by reference.
Should reduce repetition and make it easier if changes occur in source.
2022-07-04 11:53:40 +12:00
KrystalDelusion
c9fbfa3684
Adding makefile for fifo
2022-07-04 10:32:55 +12:00
Jannis Harder
e3123283ea
Merge pull request #170 from programmerjake/add-simcheck-option
...
switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules
2022-07-03 11:47:22 +02:00
KrystalDelusion
a5f67ed904
Merge branch 'master' into fifo_example
2022-07-01 11:46:02 +12:00
KrystalDelusion
de5b9b7821
Changed phrasing to avoid confusion on witnesses
2022-07-01 11:29:33 +12:00
KrystalDelusion
aab2c3c2e0
New exercise section
...
Worked exercise using the MAX_DATA parameter, highlighting its
incompleteness. Includes completed examples in /golden subdirectory.
Also some formatting changes for spacing and extra links.
2022-07-01 11:19:01 +12:00
KrystalDelusion
7ba67ef260
Removing unnecessary underflow assertions
2022-07-01 11:15:47 +12:00
Jannis Harder
4d858a1b9c
Merge pull request #189 from jix/autotune_docs
...
docs: add missing autotune.rst
2022-06-30 17:53:22 +02:00
Jannis Harder
685457915a
docs: add missing autotune.rst
2022-06-30 17:50:05 +02:00
KrystalDelusion
907db48ac9
Updating from feedback
...
Primarily addressing Nak's comments on the PR first.
Of note is the change from separate files to a single file.
Changed to boolector engine and bmc by default.
Updated install instructions to move z3 to optional and boolector to
recommended.
Literal code includes use :lines: option.
2022-06-30 12:06:12 +12:00
Jannis Harder
abe0086ec1
Merge pull request #158 from jix/autotune
...
Autotune: Automatic engine selection
2022-06-29 16:48:06 +02:00
Jannis Harder
d038a7d35c
autotune: Initial documentation
2022-06-27 15:58:42 +02:00
Jannis Harder
48a02f9cc4
Test autotune
2022-06-27 15:58:42 +02:00
Jannis Harder
b4458d43d7
Automatic engine selection
2022-06-27 15:58:42 +02:00
Jannis Harder
5014d74023
sby_design: Extract total memory size and forall usage
2022-06-24 13:50:26 +02:00
Jannis Harder
157bb156c0
Merge pull request #185 from georgerennie/prefix_empty_taskname
...
Use default prefix directory when no task is specified
2022-06-24 12:40:09 +02:00
Jannis Harder
0d90e29ef3
Merge pull request #183 from jix/engine-option-docs
...
Reflect recent engine updates in the reference docs
2022-06-23 16:39:32 +02:00
Jannis Harder
f66436ce48
Merge pull request #184 from jix/smtbmc-keepgoing-induction-trace-fix
...
smtbmc: Fix induction trace filename with --keep-going for the basecase
2022-06-23 13:37:38 +02:00
Jannis Harder
3dcf7766ea
smtbmc: Fix induction trace filename with --keep-going for the basecase
...
--keep-going only applies to the basecase and induction runs without that
option, so the trace filename for induction should have no placeholder.
2022-06-23 13:15:58 +02:00
db740839b7
switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules.
...
Fixes : #168
Depends on: https://github.com/YosysHQ/yosys/pull/3391
2022-06-22 21:17:29 -07:00
Jannis Harder
d8ebd1eb9d
Reflect recent engine updates in the reference docs
2022-06-20 15:23:59 +02:00
George Rennie
0308142fa4
Use default prefix directory when no task is specified
2022-06-19 00:49:12 +01:00
Jannis Harder
fb5705b5bd
Merge pull request #182 from jix/taskloop
...
Decouple taskloop from task
2022-06-15 16:41:39 +02:00
Jannis Harder
0fe8c223cf
Decouple taskloop from task
2022-06-15 16:28:09 +02:00
Jannis Harder
c944a9c99c
Merge pull request #181 from jix/monotonic
...
Use monotonic clock for timeouts
2022-06-15 16:27:23 +02:00
Jannis Harder
d1c04f79d6
Use monotonic clock for timeouts
2022-06-15 14:11:25 +02:00
Jannis Harder
0df73ea666
Merge pull request #180 from jix/sby-fewer-asserts
...
Don't use python asserts to handle unexpected solver output
2022-06-15 14:08:15 +02:00
Jannis Harder
d0c59a3155
Don't use python asserts to handle unexpected solver output
2022-06-15 13:25:21 +02:00
Jannis Harder
e99884e319
SbyProc: New error_callback instead of exit_callback for failing procs
2022-06-15 13:25:21 +02:00
