Aki Van Ness
a0d366e58a
some cleanup, added some rough parser tests, and started altering the engines section
2022-08-18 05:36:09 -04:00
Aki Van Ness
0ab158eea1
sby: core: minor update to the stage parsing
2022-08-18 05:36:09 -04:00
Aki Van Ness
ed82c78acc
sby: core: Added preliminary support for [stage] sections
2022-08-18 05:36:08 -04:00
Aki Van Ness
4cccbf77fa
sby: core: Added preliminary support for the [setup] section
2022-08-18 05:36:08 -04:00
Jannis Harder
9a14f4d238
Merge pull request #210 from jix/witness_flow
...
Updated formal flow with new witness format
2022-08-17 16:57:11 +02:00
Jannis Harder
0aebf0b4d0
aig model: Call memory_map late to avoid performance issues
...
This requires running simplemap on the output as memory_map produces
coarse-grained cells even though we already have a fine-grained design.
2022-08-17 16:41:32 +02:00
Jannis Harder
3412ea859b
New "none" engine to be used with the "make_model" option
2022-08-05 16:31:15 +02:00
Jannis Harder
231f0b80aa
Add make_model option to generate models not required by the task
...
Useful to do custom things (like counter example minimization) but still
use sby's flow to prepare models.
2022-08-05 16:31:15 +02:00
Jannis Harder
22585b33dc
Use 'rename -witness' instead of multiple 'rename -enumerate'
2022-08-05 16:31:15 +02:00
Jannis Harder
d3520037b9
Write native yosys witness traces
2022-08-05 16:31:15 +02:00
Jannis Harder
acaf6ef0c2
Use new memory_map -formal for aiger/_nomem
2022-08-05 16:31:15 +02:00
Jannis Harder
5265a52b65
Refactor flow to use a common prep model
...
The goal of this is to make sure that all backend flows are compatible
and we can map between them, so that e.g. the aiger model can be used to
minimize a counterexample trace produced by smtbmc. Reducing the parts
that differ per backend (including parts that receive different input
depending on the used backend) also makes testing more effective as the
common parts are easier to cover.
2022-08-05 16:31:15 +02:00
Jannis Harder
edb068bff4
Fix print_junit_results failure during some error conditions
...
There is a small window between setting self.precise_prop_status and
initializing self.design. I've only managed to produce an error within
that windows during development, but getting unrelated stacktraces from
print_junit_result failing distracts from debugging the issue at hand.
2022-08-05 16:31:15 +02:00
Aki Van Ness
46ca20f8ec
sby: core: ensured to strip the line of any uneeded whitespace
2022-08-04 06:13:28 -04:00
Aki Van Ness
9368f3f987
sby: core: explicitly split the the entries for the [options] section params to be at most one,
2022-08-04 06:13:28 -04:00
Aki Van Ness
10234fef00
sby: core: changed how the split for the section header and arguments are done, with a prior strip to remove and extra whitespace
2022-08-04 06:13:28 -04:00
Aki Van Ness
8133aaa8f8
sby: core: changed how the sections and their arguments are handled and cleared up the strangly worded error messages related to that
2022-08-04 06:13:28 -04:00
Jannis Harder
8d2fa9b304
Merge pull request #207 from jix/fix_smt_shift
...
Regression test for YosysHQ/yosys#3433
2022-08-03 17:04:10 +02:00
Jannis Harder
523b7a252e
Regression test for YosysHQ/yosys#3433
2022-08-03 16:08:19 +02:00
Aki Van Ness
59dc27ed73
sby: core: config: cleaned up the error messages to make them less opaque
2022-08-01 10:16:05 -04:00
Jannis Harder
c200690160
Merge pull request #201 from jix/autotune_example_in_docs
...
Autotune example in docs
2022-08-01 12:13:38 +02:00
Jannis Harder
4ec278e6ec
Autotune example in docs
2022-07-26 16:35:57 +02:00
Jannis Harder
0395b8a439
Merge pull request #200 from jix/autotune_example
...
example for autotune
2022-07-26 16:21:16 +02:00
Jannis Harder
9293e66092
example for autotune
2022-07-26 16:06:02 +02:00
Jannis Harder
a498e1e9a1
Merge pull request #199 from nakengelhardt/add_cvc5_tool_rule
...
add cvc5 executable to required tool mapping
2022-07-25 17:27:43 +02:00
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
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
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
Jannis Harder
abe0086ec1
Merge pull request #158 from jix/autotune
...
Autotune: Automatic engine selection
2022-06-29 16:48:06 +02:00
