SymbiYosys.git
2 years agoMerge pull request #193 from jix/abc_pdr_v
Jannis Harder [Wed, 13 Jul 2022 14:07:04 +0000 (16:07 +0200)]
Merge pull request #193 from jix/abc_pdr_v

abc pdr: Enable log output by default

2 years agoUpdate autotune.rst
matt venn [Mon, 11 Jul 2022 09:10:45 +0000 (11:10 +0200)]
Update autotune.rst

2 years agoMerge pull request #194 from jix/autotune_rst_fixes
Jannis Harder [Fri, 8 Jul 2022 12:46:41 +0000 (14:46 +0200)]
Merge pull request #194 from jix/autotune_rst_fixes

docs: Don't use linebreaks within inline code spans.

2 years agodocs: Don't use linebreaks within inline code spans.
Jannis Harder [Fri, 8 Jul 2022 12:31:57 +0000 (14:31 +0200)]
docs: Don't use linebreaks within inline code spans.

2 years agoabc pdr: Enable log output by default
Jannis Harder [Fri, 8 Jul 2022 10:36:44 +0000 (12:36 +0200)]
abc pdr: Enable log output by default

This makes it consistent with the other abc solvers and shows whether
abc pdr is making progress.

2 years agoMerge pull request #191 from jix/early-readconfig
Jannis Harder [Wed, 6 Jul 2022 10:05:13 +0000 (12:05 +0200)]
Merge pull request #191 from jix/early-readconfig

Read config before creating a workdir

2 years agoMerge pull request #192 from jix/win_retcode
Jannis Harder [Wed, 6 Jul 2022 10:05:03 +0000 (12:05 +0200)]
Merge pull request #192 from jix/win_retcode

Make SbyProc hide Windows differences in retcode handling

2 years agoMake SbyProc hide Windows differences in retcode handling
Jannis Harder [Wed, 6 Jul 2022 09:19:51 +0000 (11:19 +0200)]
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.

2 years agoRead config before creating a workdir
Jannis Harder [Tue, 5 Jul 2022 15:20:55 +0000 (17:20 +0200)]
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.

2 years agoMerge pull request #190 from jix/windows_fixes
Jannis Harder [Tue, 5 Jul 2022 14:09:54 +0000 (16:09 +0200)]
Merge pull request #190 from jix/windows_fixes

tests: Windows fixes

2 years agotests: Windows fixes
Jannis Harder [Tue, 5 Jul 2022 13:34:27 +0000 (15:34 +0200)]
tests: Windows fixes

Make tests runnable on Windows, as long as a unix like environment as
e.g. provided by MSYS2 is available.

2 years agoMerge pull request #187 from jix/const_clocks
Jannis Harder [Mon, 4 Jul 2022 15:47:16 +0000 (17:47 +0200)]
Merge pull request #187 from jix/const_clocks

Test uninitialized FFs with constant clocks and fix btor script for this

2 years agotest uninited FFs with const clks and fix btor script for this
Jannis Harder [Wed, 29 Jun 2022 16:00:52 +0000 (18:00 +0200)]
test uninited FFs with const clks and fix btor script for this

2 years agoMerge pull request #186 from jix/ff_xinit_opt
Jannis Harder [Mon, 4 Jul 2022 12:03:06 +0000 (14:03 +0200)]
Merge pull request #186 from jix/ff_xinit_opt

tests: Test for invalid x-value FF init optimizations

2 years agotests: Test for invalid x-value FF init optimizations
Jannis Harder [Wed, 29 Jun 2022 14:43:07 +0000 (16:43 +0200)]
tests: Test for invalid x-value FF init optimizations

2 years agoMerge pull request #170 from programmerjake/add-simcheck-option
Jannis Harder [Sun, 3 Jul 2022 09:47:22 +0000 (11:47 +0200)]
Merge pull request #170 from programmerjake/add-simcheck-option

switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules

2 years agoMerge pull request #189 from jix/autotune_docs
Jannis Harder [Thu, 30 Jun 2022 15:53:22 +0000 (17:53 +0200)]
Merge pull request #189 from jix/autotune_docs

docs: add missing autotune.rst

2 years agodocs: add missing autotune.rst
Jannis Harder [Thu, 30 Jun 2022 15:50:05 +0000 (17:50 +0200)]
docs: add missing autotune.rst

2 years agoMerge pull request #158 from jix/autotune
Jannis Harder [Wed, 29 Jun 2022 14:48:06 +0000 (16:48 +0200)]
Merge pull request #158 from jix/autotune

Autotune: Automatic engine selection

2 years agoautotune: Initial documentation
Jannis Harder [Mon, 27 Jun 2022 13:57:22 +0000 (15:57 +0200)]
autotune: Initial documentation

2 years agoTest autotune
Jannis Harder [Thu, 23 Jun 2022 14:37:56 +0000 (16:37 +0200)]
Test autotune

2 years agoAutomatic engine selection
Jannis Harder [Mon, 25 Apr 2022 10:27:18 +0000 (12:27 +0200)]
Automatic engine selection

2 years agosby_design: Extract total memory size and forall usage
Jannis Harder [Tue, 14 Jun 2022 16:04:24 +0000 (18:04 +0200)]
sby_design: Extract total memory size and forall usage

2 years agoMerge pull request #185 from georgerennie/prefix_empty_taskname
Jannis Harder [Fri, 24 Jun 2022 10:40:09 +0000 (12:40 +0200)]
Merge pull request #185 from georgerennie/prefix_empty_taskname

Use default prefix directory when no task is specified

2 years agoMerge pull request #183 from jix/engine-option-docs
Jannis Harder [Thu, 23 Jun 2022 14:39:32 +0000 (16:39 +0200)]
Merge pull request #183 from jix/engine-option-docs

Reflect recent engine updates in the reference docs

2 years agoMerge pull request #184 from jix/smtbmc-keepgoing-induction-trace-fix
Jannis Harder [Thu, 23 Jun 2022 11:37:38 +0000 (13:37 +0200)]
Merge pull request #184 from jix/smtbmc-keepgoing-induction-trace-fix

smtbmc: Fix induction trace filename with --keep-going for the basecase

2 years agosmtbmc: Fix induction trace filename with --keep-going for the basecase
Jannis Harder [Thu, 23 Jun 2022 11:15:58 +0000 (13:15 +0200)]
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.

2 years agoswitch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module... add-simcheck-option
Jacob Lifshay [Thu, 23 Jun 2022 04:17:29 +0000 (21:17 -0700)]
switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules.

Fixes: #168
Depends on: https://github.com/YosysHQ/yosys/pull/3391

2 years agoReflect recent engine updates in the reference docs
Jannis Harder [Mon, 20 Jun 2022 12:59:00 +0000 (14:59 +0200)]
Reflect recent engine updates in the reference docs

2 years agoUse default prefix directory when no task is specified
George Rennie [Sat, 18 Jun 2022 23:49:12 +0000 (00:49 +0100)]
Use default prefix directory when no task is specified

2 years agoMerge pull request #182 from jix/taskloop
Jannis Harder [Wed, 15 Jun 2022 14:41:39 +0000 (16:41 +0200)]
Merge pull request #182 from jix/taskloop

Decouple taskloop from task

2 years agoDecouple taskloop from task
Jannis Harder [Thu, 21 Apr 2022 14:22:32 +0000 (16:22 +0200)]
Decouple taskloop from task

2 years agoMerge pull request #181 from jix/monotonic
Jannis Harder [Wed, 15 Jun 2022 14:27:23 +0000 (16:27 +0200)]
Merge pull request #181 from jix/monotonic

Use monotonic clock for timeouts

2 years agoUse monotonic clock for timeouts
Jannis Harder [Mon, 25 Apr 2022 13:43:59 +0000 (15:43 +0200)]
Use monotonic clock for timeouts

2 years agoMerge pull request #180 from jix/sby-fewer-asserts
Jannis Harder [Wed, 15 Jun 2022 12:08:15 +0000 (14:08 +0200)]
Merge pull request #180 from jix/sby-fewer-asserts

Don't use python asserts to handle unexpected solver output

2 years agoDon't use python asserts to handle unexpected solver output
Jannis Harder [Tue, 14 Jun 2022 15:59:08 +0000 (17:59 +0200)]
Don't use python asserts to handle unexpected solver output

2 years agoSbyProc: New error_callback instead of exit_callback for failing procs
Jannis Harder [Wed, 15 Jun 2022 10:10:52 +0000 (12:10 +0200)]
SbyProc: New error_callback instead of exit_callback for failing procs

2 years agoMerge pull request #179 from jix/btor-option-handling
Jannis Harder [Wed, 15 Jun 2022 11:24:36 +0000 (13:24 +0200)]
Merge pull request #179 from jix/btor-option-handling

btor pono: improve option handling

2 years agobtor pono: improve option handling
Jannis Harder [Tue, 14 Jun 2022 15:56:54 +0000 (17:56 +0200)]
btor pono: improve option handling

Fail on the unsupported skip option and pass solver args to pono.

2 years agoMerge pull request #178 from jix/aiger-aigbmc-fixes
Jannis Harder [Tue, 14 Jun 2022 15:52:33 +0000 (17:52 +0200)]
Merge pull request #178 from jix/aiger-aigbmc-fixes

aiger: check supported modes and aigbmc fixes

2 years agoaiger: check supported modes and aigbmc fixes
Jannis Harder [Tue, 14 Jun 2022 15:15:32 +0000 (17:15 +0200)]
aiger: check supported modes and aigbmc fixes

2 years agoMerge pull request #177 from mattvenn/tristate-example
Jannis Harder [Tue, 14 Jun 2022 13:54:09 +0000 (15:54 +0200)]
Merge pull request #177 from mattvenn/tristate-example

Tristate example

2 years agoadd makefile for test
Matt Venn [Tue, 14 Jun 2022 13:35:22 +0000 (15:35 +0200)]
add makefile for test

2 years agoremove unused module port
Matt Venn [Mon, 13 Jun 2022 12:00:08 +0000 (14:00 +0200)]
remove unused module port

2 years agoexpect fail
Matt Venn [Mon, 13 Jun 2022 11:59:12 +0000 (13:59 +0200)]
expect fail

2 years agotristate example
Matt Venn [Mon, 13 Jun 2022 11:51:04 +0000 (13:51 +0200)]
tristate example

2 years agoMerge pull request #172 from jix/smtbmc-unroll-noincr-traces-fix
Jannis Harder [Mon, 13 Jun 2022 12:05:37 +0000 (14:05 +0200)]
Merge pull request #172 from jix/smtbmc-unroll-noincr-traces-fix

Regression test for smtbmc --unroll --noincr

2 years agoMerge pull request #175 from jix/more-test-improvements
Jannis Harder [Mon, 13 Jun 2022 11:59:31 +0000 (13:59 +0200)]
Merge pull request #175 from jix/more-test-improvements

Use the test Makefile for all examples

2 years agoUse the test Makefile for all examples
Jannis Harder [Mon, 13 Jun 2022 11:20:33 +0000 (13:20 +0200)]
Use the test Makefile for all examples

* Rename and move sbysrc/demo[123].sby to docs/examples/demos
    * Make them use multiple tasks for multiple engines
* Scan docs/examples for sby files for make test
* `make ci` is now `NOSKIP` by default
* Skip scripts using `verific` w/o yosys verific support
    * This does not fail even with NOSKIP set

2 years agoRegression test for smtbmc --unroll --noincr
Jannis Harder [Wed, 8 Jun 2022 10:08:34 +0000 (12:08 +0200)]
Regression test for smtbmc --unroll --noincr

2 years agoMerge pull request #173 from jix/test-cvc
Jannis Harder [Fri, 10 Jun 2022 13:24:49 +0000 (15:24 +0200)]
Merge pull request #173 from jix/test-cvc

Test that cvc4 and cvc5 can be used

2 years agoMerge pull request #164 from jix/suggest_f_flag
Jannis Harder [Fri, 10 Jun 2022 13:14:01 +0000 (15:14 +0200)]
Merge pull request #164 from jix/suggest_f_flag

Suggest -f when the workdir already exists

2 years agoTest that cvc4 and cvc5 can be used
Jannis Harder [Wed, 8 Jun 2022 11:33:12 +0000 (13:33 +0200)]
Test that cvc4 and cvc5 can be used

2 years agoMerge pull request #171 from jix/make-remove-unused-tool-list
Jannis Harder [Wed, 8 Jun 2022 09:43:43 +0000 (11:43 +0200)]
Merge pull request #171 from jix/make-remove-unused-tool-list

tests: Remove unused tool list in test Makefile

2 years agotests: Remove unused tool list in test Makefile
Jannis Harder [Wed, 8 Jun 2022 09:32:35 +0000 (11:32 +0200)]
tests: Remove unused tool list in test Makefile

The checks for available tools moved to a python script, so need need to
have a copy of the tool list in the Makefile.

2 years agoMerge pull request #169 from jix/yices-forall
Jannis Harder [Wed, 8 Jun 2022 07:43:47 +0000 (09:43 +0200)]
Merge pull request #169 from jix/yices-forall

Test designs using $allconst

2 years agoMerge pull request #163 from jix/make_improvements
Jannis Harder [Tue, 7 Jun 2022 12:50:59 +0000 (14:50 +0200)]
Merge pull request #163 from jix/make_improvements

Test makefile improvements

2 years agotests: Move required tool checks from rule generation to execution
Jannis Harder [Tue, 7 Jun 2022 12:29:25 +0000 (14:29 +0200)]
tests: Move required tool checks from rule generation to execution

This avoids regenerating the test makefile rules when the set of
installed tools changes and is a bit simpler overall.

2 years agoDon't fail tests when xmlschema is missing
Jannis Harder [Fri, 3 Jun 2022 15:16:01 +0000 (17:16 +0200)]
Don't fail tests when xmlschema is missing

2 years agoTest designs using $allconst
Jannis Harder [Fri, 3 Jun 2022 14:48:21 +0000 (16:48 +0200)]
Test designs using $allconst

2 years agotests: Fail on CI when any required tool is missing
Jannis Harder [Thu, 2 Jun 2022 14:25:11 +0000 (16:25 +0200)]
tests: Fail on CI when any required tool is missing

2 years agotests: Check for btorsim --vcd
Jannis Harder [Thu, 2 Jun 2022 14:24:30 +0000 (16:24 +0200)]
tests: Check for btorsim --vcd

2 years agoupdate install instructions for btorsim
N. Engelhardt [Wed, 1 Jun 2022 14:51:28 +0000 (16:51 +0200)]
update install instructions for btorsim

2 years agoSuggest -f when the workdir already exists
Jannis Harder [Mon, 30 May 2022 14:18:37 +0000 (16:18 +0200)]
Suggest -f when the workdir already exists

2 years agoCheck for the tabby/oss cad suite before running make ci checks
Jannis Harder [Mon, 30 May 2022 13:27:14 +0000 (15:27 +0200)]
Check for the tabby/oss cad suite before running make ci checks

2 years agoBetter checking of available solvers
Jannis Harder [Mon, 30 May 2022 12:37:20 +0000 (14:37 +0200)]
Better checking of available solvers

Check for required auxiliary tools and always regenerate the make rules
when the set of available tools changes.

2 years agoMakefile: Rename run_tests to test, update help, use .PHONY
Jannis Harder [Mon, 30 May 2022 11:35:57 +0000 (13:35 +0200)]
Makefile: Rename run_tests to test, update help, use .PHONY

2 years agoMerge pull request #161 from programmerjake/add-div-mod-floor-tests
Jannis Harder [Thu, 26 May 2022 10:00:05 +0000 (12:00 +0200)]
Merge pull request #161 from programmerjake/add-div-mod-floor-tests

add test for yosys's $divfloor and $modfloor cells

2 years agoadd depth 1
Jacob Lifshay [Wed, 25 May 2022 10:35:21 +0000 (03:35 -0700)]
add depth 1

2 years agoadd test for yosys's $divfloor and $modfloor cells
Jacob Lifshay [Wed, 25 May 2022 00:51:48 +0000 (17:51 -0700)]
add test for yosys's $divfloor and $modfloor cells

Depends on: https://github.com/YosysHQ/yosys/pull/3335

2 years agodocs: add instructions for newer btorsim version required
N. Engelhardt [Tue, 24 May 2022 09:39:10 +0000 (11:39 +0200)]
docs: add instructions for newer btorsim version required

2 years agoMerge pull request #159 from jix/fix-dpmem-example
Jannis Harder [Wed, 11 May 2022 09:23:57 +0000 (11:23 +0200)]
Merge pull request #159 from jix/fix-dpmem-example

examples: Fix use of SVA value change expressions

2 years agoexamples: Fix use of SVA value change expressions
Jannis Harder [Wed, 11 May 2022 08:38:54 +0000 (10:38 +0200)]
examples: Fix use of SVA value change expressions

The $stable value change expression cannot be true for a non-x signal in
the initial state. This is now correctly handled by the verific import,
so the dpmem example needs to start assuming `$stable` only after
leaving the initial state.

2 years agoMerge pull request #156 from jix/refactor-tests
Jannis Harder [Mon, 25 Apr 2022 09:21:21 +0000 (11:21 +0200)]
Merge pull request #156 from jix/refactor-tests

Refactor tests

2 years agoRefactor tests
Jannis Harder [Mon, 11 Apr 2022 15:39:05 +0000 (17:39 +0200)]
Refactor tests

Organize tests into subdirectories and use a new makefile that scans
.sby files and allows selecting tests by mode, engine, solver and/or
subdirectory. Automatically skips tests that use engines/solvers that
are not found in the PATH.

See `cd tests; make help` for a description of supported make targets.

2 years agoAdd --dumptaskinfo option to output some .sby metadata as json
Jannis Harder [Mon, 11 Apr 2022 15:37:27 +0000 (17:37 +0200)]
Add --dumptaskinfo option to output some .sby metadata as json

2 years agoAdd envvar to enable automatic .gitignore creation for workdirs
Jannis Harder [Mon, 11 Apr 2022 15:35:11 +0000 (17:35 +0200)]
Add envvar to enable automatic .gitignore creation for workdirs

2 years agoMerge pull request #140 from nakengelhardt/junit_jny
Miodrag Milanović [Fri, 8 Apr 2022 13:26:48 +0000 (15:26 +0200)]
Merge pull request #140 from nakengelhardt/junit_jny

junit: use write_jny instead of write_json

2 years agojunit: use write_jny instead of write_json
N. Engelhardt [Thu, 10 Mar 2022 16:46:08 +0000 (17:46 +0100)]
junit: use write_jny instead of write_json

2 years agoMerge pull request #155 from jix/invalid_ff_dcinit_merge
Miodrag Milanović [Sun, 3 Apr 2022 10:15:58 +0000 (12:15 +0200)]
Merge pull request #155 from jix/invalid_ff_dcinit_merge

Regression test: do not merge FFs with unconstrained initvals

2 years agoRegression test: do not merge FFs with unconstrained initvals
Jannis Harder [Fri, 1 Apr 2022 17:25:09 +0000 (19:25 +0200)]
Regression test: do not merge FFs with unconstrained initvals

Currently done by `opt -keepdc` via `opt_merge` but not valid in a
formal context.

2 years agoMerge pull request #154 from jix/sby_design-fixes
Jannis Harder [Thu, 31 Mar 2022 14:35:40 +0000 (16:35 +0200)]
Merge pull request #154 from jix/sby_design-fixes

sby_design fixes

2 years agoFix design_hierarchy handling of $paramod cells
Jannis Harder [Thu, 31 Mar 2022 13:51:58 +0000 (15:51 +0200)]
Fix design_hierarchy handling of $paramod cells

2 years agoFix variable name in find_property_by_cellname's error path
Jannis Harder [Thu, 31 Mar 2022 11:12:15 +0000 (13:12 +0200)]
Fix variable name in find_property_by_cellname's error path

2 years agoMerge pull request #151 from jix/prefer-first-trace
Jannis Harder [Wed, 30 Mar 2022 12:48:04 +0000 (14:48 +0200)]
Merge pull request #151 from jix/prefer-first-trace

Prefer the first tracefile for each failing assertion

2 years agoPrefer the first tracefile for each failing assertion
Jannis Harder [Wed, 30 Mar 2022 11:35:57 +0000 (13:35 +0200)]
Prefer the first tracefile for each failing assertion

2 years agoMerge pull request #150 from nakengelhardt/fix_junit_type_assignment
N. Engelhardt [Wed, 30 Mar 2022 10:53:48 +0000 (12:53 +0200)]
Merge pull request #150 from nakengelhardt/fix_junit_type_assignment

note unexpected return statuses in junit

2 years agoMerge pull request #147 from jix/smtbmc-keepgoing
Jannis Harder [Wed, 30 Mar 2022 09:42:48 +0000 (11:42 +0200)]
Merge pull request #147 from jix/smtbmc-keepgoing

Support and tests for smtbmc `--keep-going`

2 years agoTests for `--keep-going`
Jannis Harder [Thu, 24 Mar 2022 15:36:59 +0000 (16:36 +0100)]
Tests for `--keep-going`

This also changes the test Makefile to run `.check.py` files after
running the corresponding `.sby` file to allow more precise testing of
the keep going feature.

2 years agonote unexpected return statuses in junit
N. Engelhardt [Tue, 29 Mar 2022 17:10:29 +0000 (19:10 +0200)]
note unexpected return statuses in junit

2 years agoMerge pull request #148 from nakengelhardt/docs_updates
N. Engelhardt [Mon, 28 Mar 2022 14:34:00 +0000 (16:34 +0200)]
Merge pull request #148 from nakengelhardt/docs_updates

documentation updates

2 years agoMerge pull request #145 from nakengelhardt/fix_junit_tracefile
N. Engelhardt [Mon, 28 Mar 2022 14:32:54 +0000 (16:32 +0200)]
Merge pull request #145 from nakengelhardt/fix_junit_tracefile

junit: handle multiple asserts failing with the same trace

2 years agoMerge pull request #142 from nakengelhardt/fix_backslash_smt2
N. Engelhardt [Mon, 28 Mar 2022 14:32:10 +0000 (16:32 +0200)]
Merge pull request #142 from nakengelhardt/fix_backslash_smt2

translate backslashes in cell names the same way as smt2 backend does

2 years agoMerge pull request #146 from jix/aim_vs_smt2_nonzero_start_offset
Miodrag Milanović [Sat, 26 Mar 2022 07:20:57 +0000 (08:20 +0100)]
Merge pull request #146 from jix/aim_vs_smt2_nonzero_start_offset

Test and fix signals with nonzero start offsets in aim files with smtbmc

2 years agodocument btor engine, add overview of mode/engine/solver combinations, remove unimple...
N. Engelhardt [Fri, 25 Mar 2022 17:01:09 +0000 (18:01 +0100)]
document btor engine, add overview of mode/engine/solver combinations, remove unimplemented modes

2 years agoTest signals with nonzero start offsets in aim files with smtbmc
Jannis Harder [Thu, 24 Mar 2022 12:12:25 +0000 (13:12 +0100)]
Test signals with nonzero start offsets in aim files with smtbmc

2 years agoUse `-no-startoffset`, avoiding index mismatch between aiger and smt2
Jannis Harder [Fri, 25 Mar 2022 10:38:22 +0000 (11:38 +0100)]
Use `-no-startoffset`, avoiding index mismatch between aiger and smt2

2 years agoInitial support for the new smtbmc --keep-going option
Jannis Harder [Mon, 21 Mar 2022 17:36:09 +0000 (18:36 +0100)]
Initial support for the new smtbmc --keep-going option

So far this only passes on the option and adjusts the trace_prefix to
support multiple numbered traces. Further changes are needed to
correctly associate individual traces with the assertions failing in
that trace.

2 years agojunit: handle multiple asserts failing with the same trace
N. Engelhardt [Tue, 22 Mar 2022 15:16:02 +0000 (16:16 +0100)]
junit: handle multiple asserts failing with the same trace

2 years agotranslate backslashes in cell names the same way as smt2 backend does
N. Engelhardt [Fri, 18 Mar 2022 15:36:41 +0000 (16:36 +0100)]
translate backslashes in cell names the same way as smt2 backend does