SymbiYosys.git
2 years agoAdded CI
Miodrag Milanovic [Wed, 12 Jan 2022 13:18:17 +0000 (14:18 +0100)]
Added CI

2 years agoMerge pull request #136 from nakengelhardt/fix_pono
Miodrag Milanović [Wed, 12 Jan 2022 12:46:25 +0000 (13:46 +0100)]
Merge pull request #136 from nakengelhardt/fix_pono

use --witness option when calling pono

2 years agocreate only a single bad when using pono solver; workaround for #137
N. Engelhardt [Wed, 12 Jan 2022 12:18:54 +0000 (13:18 +0100)]
create only a single bad when using pono solver; workaround for #137

2 years agoadd testcase exposing #137
N. Engelhardt [Wed, 12 Jan 2022 10:06:05 +0000 (11:06 +0100)]
add testcase exposing #137

2 years agouse --witness option when calling pono
N. Engelhardt [Wed, 12 Jan 2022 09:48:32 +0000 (10:48 +0100)]
use --witness option when calling pono

2 years agoMerge pull request #135 from nakengelhardt/rename_task
N. Engelhardt [Wed, 12 Jan 2022 09:52:42 +0000 (10:52 +0100)]
Merge pull request #135 from nakengelhardt/rename_task

Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion

2 years agoMerge pull request #134 from nakengelhardt/advertise_suite_in_readme
N. Engelhardt [Tue, 11 Jan 2022 16:34:35 +0000 (17:34 +0100)]
Merge pull request #134 from nakengelhardt/advertise_suite_in_readme

mention tabby+oss cad suite in readme

2 years agoRename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion. Config file...
N. Engelhardt [Tue, 11 Jan 2022 15:12:23 +0000 (16:12 +0100)]
Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion. Config file tasks now correspond to SbyTasks.

2 years agomention tabby+oss cad suite in readme
N. Engelhardt [Tue, 4 Jan 2022 15:32:59 +0000 (16:32 +0100)]
mention tabby+oss cad suite in readme

2 years agoImprovements and cleanups in tasks handling
Claire Xenia Wolf [Sat, 18 Dec 2021 10:36:34 +0000 (11:36 +0100)]
Improvements and cleanups in tasks handling

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2 years agoFixed [tasks] section parsing
Claire Xenia Wolf [Fri, 17 Dec 2021 19:57:19 +0000 (20:57 +0100)]
Fixed [tasks] section parsing

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2 years agoUpdate README.md
Claire Xen [Fri, 17 Dec 2021 14:50:57 +0000 (15:50 +0100)]
Update README.md

2 years agoUpdate README.md
Claire Xen [Fri, 17 Dec 2021 14:48:01 +0000 (15:48 +0100)]
Update README.md

2 years agoAdd inductive invariants example
Claire Xenia Wolf [Fri, 17 Dec 2021 14:42:04 +0000 (15:42 +0100)]
Add inductive invariants example

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2 years agoAdd ":"-syntax for [tasks] section
Claire Xenia Wolf [Fri, 17 Dec 2021 14:36:35 +0000 (15:36 +0100)]
Add ":"-syntax for [tasks] section

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2 years agoUpdate docs theme
Claire Xenia Wolf [Tue, 30 Nov 2021 09:47:43 +0000 (10:47 +0100)]
Update docs theme

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2 years agoUpdate docs theme
Claire Xenia Wolf [Mon, 29 Nov 2021 15:51:54 +0000 (16:51 +0100)]
Update docs theme

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2 years agoupdate docs theme
Claire Xenia Wolf [Fri, 26 Nov 2021 19:34:55 +0000 (20:34 +0100)]
update docs theme

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
3 years agoAdd support for directories in [files] section
Claire Xenia Wolf [Sun, 31 Oct 2021 13:43:02 +0000 (14:43 +0100)]
Add support for directories in [files] section

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
3 years agoFixed names and links
Claire Xenia Wolf [Sun, 31 Oct 2021 13:42:39 +0000 (14:42 +0100)]
Fixed names and links

3 years agoMerge pull request #127 from christian-krieg/feat/update-docs_super-prove
Miodrag Milanović [Mon, 13 Sep 2021 14:21:18 +0000 (16:21 +0200)]
Merge pull request #127 from christian-krieg/feat/update-docs_super-prove

Updated install instructions for super_prove

3 years agoFix regression
Miodrag Milanovic [Wed, 25 Aug 2021 10:10:18 +0000 (12:10 +0200)]
Fix regression

3 years agoInitialize variable
Miodrag Milanovic [Wed, 25 Aug 2021 09:38:24 +0000 (11:38 +0200)]
Initialize variable

3 years agoMerge pull request #126 from piegamesde/master
Claire Xen [Mon, 23 Aug 2021 14:03:03 +0000 (16:03 +0200)]
Merge pull request #126 from piegamesde/master

Various improvements and fixes

3 years agoUpdated install instructions for super_prove
Christian Krieg [Tue, 20 Jul 2021 20:33:03 +0000 (22:33 +0200)]
Updated install instructions for super_prove

* Links were dead
* No binaries to download
* Updated with install information from super_prove github repository
* Augmented with additional commands to ease installation

3 years agofixup! Allow to set a working directory even when having multiple tasks
piegames [Thu, 8 Jul 2021 18:48:23 +0000 (20:48 +0200)]
fixup! Allow to set a working directory even when having multiple tasks

3 years agoBetter error message when tasks failed
piegames [Thu, 24 Jun 2021 22:03:05 +0000 (00:03 +0200)]
Better error message when tasks failed

3 years agoTurn .format() strings into f-strings
piegames [Thu, 24 Jun 2021 22:02:22 +0000 (00:02 +0200)]
Turn .format() strings into f-strings

3 years agoAllow to set a working directory even when having multiple tasks
piegames [Mon, 21 Jun 2021 20:32:29 +0000 (22:32 +0200)]
Allow to set a working directory even when having multiple tasks

Fixes #125.

3 years agoPrint paths as absolute
piegames [Mon, 21 Jun 2021 20:31:51 +0000 (22:31 +0200)]
Print paths as absolute

This generally makes debugging path issues easier.

3 years agoUpdate docs conf.py
Claire Xenia Wolf [Fri, 21 May 2021 01:36:11 +0000 (03:36 +0200)]
Update docs conf.py

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
3 years agoNew docs conf.py
Claire Xenia Wolf [Fri, 21 May 2021 01:31:50 +0000 (03:31 +0200)]
New docs conf.py

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
3 years agoMake readme of abstraction example more tutorial-like
N. Engelhardt [Fri, 16 Apr 2021 13:54:51 +0000 (15:54 +0200)]
Make readme of abstraction example more tutorial-like

3 years agoMerge pull request #121 from YosysHQ/windows_fix
Miodrag Milanović [Mon, 22 Mar 2021 15:51:11 +0000 (16:51 +0100)]
Merge pull request #121 from YosysHQ/windows_fix

Windows specific fixes

3 years agoWindows specific fixes
Miodrag Milanovic [Mon, 22 Mar 2021 15:48:33 +0000 (16:48 +0100)]
Windows specific fixes

3 years agoUpdate conf.py
Claire Xen [Thu, 4 Mar 2021 15:49:31 +0000 (16:49 +0100)]
Update conf.py

3 years agoDelete symbiotic_logo.png
Claire Xen [Wed, 24 Feb 2021 16:52:54 +0000 (17:52 +0100)]
Delete symbiotic_logo.png

3 years agoUpdate conf.py
Claire Xen [Wed, 24 Feb 2021 16:48:13 +0000 (17:48 +0100)]
Update conf.py

3 years agoFix syntax errors
Miodrag Milanovic [Tue, 26 Jan 2021 08:09:43 +0000 (09:09 +0100)]
Fix syntax errors

4 years agoExtract installation procedure to separate file
Miodrag Milanovic [Fri, 23 Oct 2020 12:03:55 +0000 (14:03 +0200)]
Extract installation procedure to separate file

4 years agocopyright
Matt Venn [Thu, 15 Oct 2020 16:02:03 +0000 (18:02 +0200)]
copyright

4 years agologo and links
Matt Venn [Thu, 15 Oct 2020 15:02:52 +0000 (17:02 +0200)]
logo and links

4 years agoMerge pull request #116 from nakengelhardt/sed_mac
N. Engelhardt [Mon, 12 Oct 2020 11:01:15 +0000 (13:01 +0200)]
Merge pull request #116 from nakengelhardt/sed_mac

make install: mac OS compatible sed usage

4 years agosed -i option is not posix, and argument syntax is incompatible between mac and linux...
N. Engelhardt [Fri, 9 Oct 2020 09:41:18 +0000 (11:41 +0200)]
sed -i option is not posix, and argument syntax is incompatible between mac and linux. use redirects instead

4 years agoMerge pull request #115 from nakengelhardt/rename_test
Miodrag Milanović [Fri, 11 Sep 2020 14:28:32 +0000 (16:28 +0200)]
Merge pull request #115 from nakengelhardt/rename_test

rename make test to make ci

4 years agorename make test to make ci
N. Engelhardt [Fri, 11 Sep 2020 11:22:07 +0000 (13:22 +0200)]
rename make test to make ci

4 years agoMerge pull request #101 from YosysHQ/program-prefix
whitequark [Sat, 22 Aug 2020 14:49:25 +0000 (14:49 +0000)]
Merge pull request #101 from YosysHQ/program-prefix

Add a PROGRAM_PREFIX= Makefile option for packages with prefixed Yosys

4 years agoAdd a PROGRAM_PREFIX= Makefile option for packages with prefixed Yosys.
whitequark [Sat, 11 Jul 2020 05:28:19 +0000 (05:28 +0000)]
Add a PROGRAM_PREFIX= Makefile option for packages with prefixed Yosys.

4 years agoRun dffunmap before writing the design with aiger/btor/smt2 backends.
Marcelina Kościelnicka [Fri, 31 Jul 2020 11:10:13 +0000 (13:10 +0200)]
Run dffunmap before writing the design with aiger/btor/smt2 backends.

4 years agofix test rule
N. Engelhardt [Fri, 24 Jul 2020 14:06:44 +0000 (16:06 +0200)]
fix test rule

4 years agoRemove redundant copy of picorv32
Claire Wolf [Fri, 24 Jul 2020 13:13:45 +0000 (15:13 +0200)]
Remove redundant copy of picorv32

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoImprovements in "make test"
Claire Wolf [Fri, 24 Jul 2020 12:58:23 +0000 (14:58 +0200)]
Improvements in "make test"

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoMerge pull request #104 from nakengelhardt/more_tests
clairexen [Fri, 24 Jul 2020 12:48:36 +0000 (14:48 +0200)]
Merge pull request #104 from nakengelhardt/more_tests

add tests directory with additional tests

4 years agoadd tests directory with additional tests
N. Engelhardt [Fri, 24 Jul 2020 11:50:02 +0000 (13:50 +0200)]
add tests directory with additional tests

4 years agofix error message formatting
N. Engelhardt [Tue, 21 Jul 2020 12:48:38 +0000 (14:48 +0200)]
fix error message formatting

4 years agoInclude verilog source files for demo1.sby
Claire Wolf [Tue, 21 Jul 2020 11:01:36 +0000 (13:01 +0200)]
Include verilog source files for demo1.sby

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoMerge pull request #102 from YosysHQ/claire/maketest
clairexen [Mon, 20 Jul 2020 21:08:31 +0000 (23:08 +0200)]
Merge pull request #102 from YosysHQ/claire/maketest

Add "make test"

4 years agoAdd "Unexpected response" handling to smtbmc engine
Claire Wolf [Mon, 20 Jul 2020 17:42:10 +0000 (19:42 +0200)]
Add "Unexpected response" handling to smtbmc engine

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoAdd "make test"
Claire Wolf [Mon, 20 Jul 2020 15:17:49 +0000 (17:17 +0200)]
Add "make test"

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoMerge pull request #99 from whitequark/patch-1
clairexen [Thu, 9 Jul 2020 16:18:09 +0000 (18:18 +0200)]
Merge pull request #99 from whitequark/patch-1

Inject executable dependencies from the environment

4 years agoMerge pull request #100 from edbordin/master
clairexen [Thu, 9 Jul 2020 16:12:13 +0000 (18:12 +0200)]
Merge pull request #100 from edbordin/master

Use latest windows python launcher from yosys

4 years agouse latest win python launcher from yosys
Ed Bordin [Wed, 8 Jul 2020 03:02:53 +0000 (13:02 +1000)]
use latest win python launcher from yosys

4 years agoInject executable dependencies from the environment
whitequark [Sun, 5 Jul 2020 10:20:35 +0000 (10:20 +0000)]
Inject executable dependencies from the environment

4 years agoMerge pull request #98 from YosysHQ/cosa2_to_pono
clairexen [Fri, 3 Jul 2020 15:42:51 +0000 (17:42 +0200)]
Merge pull request #98 from YosysHQ/cosa2_to_pono

cosa2 -> pono rename

4 years agocosa2 -> pono rename
Miodrag Milanovic [Fri, 3 Jul 2020 09:25:55 +0000 (11:25 +0200)]
cosa2 -> pono rename

4 years agoMerge pull request #97 from nakengelhardt/seed_arg
clairexen [Wed, 1 Jul 2020 17:20:06 +0000 (19:20 +0200)]
Merge pull request #97 from nakengelhardt/seed_arg

add --seed option to smtbmc and btor engines

4 years agoMerge pull request #94 from nakengelhardt/fix_93
clairexen [Wed, 1 Jul 2020 17:19:08 +0000 (19:19 +0200)]
Merge pull request #94 from nakengelhardt/fix_93

ignore race condition in killing already-terminated process

4 years agoadd --seed option to smtbmc and btor engines
N. Engelhardt [Wed, 1 Jul 2020 16:05:20 +0000 (18:05 +0200)]
add --seed option to smtbmc and btor engines

4 years agoMerge pull request #96 from YosysHQ/claire/btorscript
clairexen [Wed, 1 Jul 2020 14:21:55 +0000 (16:21 +0200)]
Merge pull request #96 from YosysHQ/claire/btorscript

Be more conservative in btor ys script

4 years agoMerge pull request #95 from adumont/patch-1
N. Engelhardt [Tue, 30 Jun 2020 09:54:04 +0000 (11:54 +0200)]
Merge pull request #95 from adumont/patch-1

Typo: missing * in Global Clock example

4 years agoTipo missing * in Global Clock example
Alexandre Dumont aka Adlx [Sun, 28 Jun 2020 22:42:06 +0000 (00:42 +0200)]
Tipo missing * in Global Clock example

4 years agoBe more conservative in btor ys script
Claire Wolf [Tue, 23 Jun 2020 12:32:59 +0000 (14:32 +0200)]
Be more conservative in btor ys script

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoignore race condition in killing already-terminated process
N. Engelhardt [Tue, 16 Jun 2020 10:41:26 +0000 (12:41 +0200)]
ignore race condition in killing already-terminated process

4 years agoMerge pull request #88 from YosysHQ/claire/cosa2
clairexen [Mon, 18 May 2020 15:01:19 +0000 (17:01 +0200)]
Merge pull request #88 from YosysHQ/claire/cosa2

Add support for cosa2 BTOR solver

4 years agoAdd support for cosa2 BTOR solver
Claire Wolf [Mon, 18 May 2020 13:13:56 +0000 (15:13 +0200)]
Add support for cosa2 BTOR solver

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agobtor engine: handle models with 0 properties
N. Engelhardt [Mon, 18 May 2020 11:11:25 +0000 (13:11 +0200)]
btor engine: handle models with 0 properties

4 years agoMerge pull request #87 from nakengelhardt/cover_trace_summary
N. Engelhardt [Wed, 13 May 2020 16:45:39 +0000 (18:45 +0200)]
Merge pull request #87 from nakengelhardt/cover_trace_summary

Trace generation improvements

4 years agofix trace summary printing
N. Engelhardt [Wed, 13 May 2020 16:15:33 +0000 (18:15 +0200)]
fix trace summary printing

4 years agocall job.terminate at end of btor engine run to kill other engines in case of whoever...
N. Engelhardt [Wed, 13 May 2020 10:42:30 +0000 (12:42 +0200)]
call job.terminate at end of btor engine run to kill other engines in case of whoever-gets-there-first runs

4 years agostart btorsim as soon as a witness is ready, print summary when multiple traces are...
N. Engelhardt [Tue, 12 May 2020 14:48:58 +0000 (16:48 +0200)]
start btorsim as soon as a witness is ready, print summary when multiple traces are produced

4 years agoAdd silent mode to SbyTask
Claire Wolf [Fri, 8 May 2020 16:49:08 +0000 (18:49 +0200)]
Add silent mode to SbyTask

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agofix return code check in btor engine
N. Engelhardt [Wed, 29 Apr 2020 14:09:18 +0000 (16:09 +0200)]
fix return code check in btor engine

4 years agoMerge pull request #85 from nakengelhardt/new_btorsim
N. Engelhardt [Wed, 29 Apr 2020 09:47:20 +0000 (11:47 +0200)]
Merge pull request #85 from nakengelhardt/new_btorsim

Note that the btor engine now requires changes not upstreamed to btor2tools yet, see btor2tools/pull/4

4 years agoUpdate wolf_goat_cabbage.sv
Claire Wolf [Wed, 22 Apr 2020 17:21:15 +0000 (19:21 +0200)]
Update wolf_goat_cabbage.sv

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoMerge pull request #86 from mattvenn/master
Claire Wolf [Wed, 22 Apr 2020 17:19:18 +0000 (19:19 +0200)]
Merge pull request #86 from mattvenn/master

make wolf goat cabbage puzzle gender neutral

4 years agoconsistent naming and put person moving line at the top
matt venn [Wed, 22 Apr 2020 17:11:23 +0000 (19:11 +0200)]
consistent naming and put person moving line at the top

4 years agoMerge branch 'master' of https://github.com/YosysHQ/SymbiYosys
matt venn [Wed, 22 Apr 2020 15:54:53 +0000 (17:54 +0200)]
Merge branch 'master' of https://github.com/YosysHQ/SymbiYosys

4 years agochange order of statements and make gender neutral
matt venn [Wed, 22 Apr 2020 15:54:39 +0000 (17:54 +0200)]
change order of statements and make gender neutral

4 years agoAdd task pattern matching, closes #76
Claire Wolf [Tue, 14 Apr 2020 17:55:14 +0000 (19:55 +0200)]
Add task pattern matching, closes #76

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoAdd a status message when one or more tasks returned a non-zero return code, closes #78
Claire Wolf [Tue, 14 Apr 2020 17:54:24 +0000 (19:54 +0200)]
Add a status message when one or more tasks returned a non-zero return code, closes #78

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoAdd djb2hash example
Claire Wolf [Thu, 9 Apr 2020 17:46:19 +0000 (19:46 +0200)]
Add djb2hash example

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agomerge master
N. Engelhardt [Wed, 8 Apr 2020 15:21:44 +0000 (17:21 +0200)]
merge master

4 years agouse info file for btorsim
N. Engelhardt [Wed, 8 Apr 2020 13:25:00 +0000 (15:25 +0200)]
use info file for btorsim

4 years agoGet rid of verific warning in abstraction example
Claire Wolf [Fri, 3 Apr 2020 13:28:23 +0000 (15:28 +0200)]
Get rid of verific warning in abstraction example

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoFix typo
Claire Wolf [Fri, 3 Apr 2020 13:18:52 +0000 (15:18 +0200)]
Fix typo

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoMerge pull request #74 from mattvenn/master
Claire Wolf [Thu, 2 Apr 2020 16:27:50 +0000 (18:27 +0200)]
Merge pull request #74 from mattvenn/master

add --init-config option

4 years agoand another
N. Engelhardt [Thu, 2 Apr 2020 15:36:54 +0000 (17:36 +0200)]
and another

4 years agofix formatting error
N. Engelhardt [Thu, 2 Apr 2020 15:21:48 +0000 (17:21 +0200)]
fix formatting error

4 years agoMerge pull request #73 from nakengelhardt/str_format
Claire Wolf [Thu, 2 Apr 2020 13:41:30 +0000 (15:41 +0200)]
Merge pull request #73 from nakengelhardt/str_format

Use .format() instead of %

4 years agofix callback functions
N. Engelhardt [Mon, 30 Mar 2020 19:15:04 +0000 (21:15 +0200)]
fix callback functions