SymbiYosys.git
3 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

3 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

3 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.

3 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.

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

3 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>
3 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>
3 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

3 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

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

3 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>
3 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"

3 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>
3 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>
3 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

3 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

3 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

3 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

3 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

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

3 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

3 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

3 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

3 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

3 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

3 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

3 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>
3 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

4 years agoadd btor cover mode; use btorsim for vcd generation
N. Engelhardt [Wed, 25 Mar 2020 14:53:55 +0000 (15:53 +0100)]
add btor cover mode; use btorsim for vcd generation

Signed-off-by: N. Engelhardt <nak@symbioticeda.com>
4 years agoremove stray braces
N. Engelhardt [Mon, 30 Mar 2020 19:23:11 +0000 (21:23 +0200)]
remove stray braces

4 years agouse argument for name of .sby and .sv files
matt venn [Thu, 26 Mar 2020 17:24:56 +0000 (18:24 +0100)]
use argument for name of .sby and .sv files

4 years agoadd --init-config option
matt venn [Wed, 25 Mar 2020 17:00:48 +0000 (18:00 +0100)]
add --init-config option

4 years agoUse .format() instead of %
N. Engelhardt [Mon, 23 Mar 2020 17:09:27 +0000 (18:09 +0100)]
Use .format() instead of %

Signed-off-by: N. Engelhardt <nak@symbioticeda.com>
4 years agoFix primegen example
Claire Wolf [Tue, 24 Mar 2020 16:12:12 +0000 (17:12 +0100)]
Fix primegen example

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoImprove BTOR and AIG yosys scripts
Claire Wolf [Tue, 11 Feb 2020 16:33:46 +0000 (17:33 +0100)]
Improve BTOR and AIG yosys scripts

Signed-off-by: Claire Wolf <clifford@clifford.at>
4 years agoMerge pull request #70 from dh73/master
Claire Wolf [Sat, 1 Feb 2020 16:11:38 +0000 (17:11 +0100)]
Merge pull request #70 from dh73/master

Fix typo in log message

4 years agoFix typo in log message
Diego H [Thu, 30 Jan 2020 19:55:34 +0000 (13:55 -0600)]
Fix typo in log message

4 years agoAdd special handling for command not found errors
Claire Wolf [Mon, 27 Jan 2020 16:59:33 +0000 (17:59 +0100)]
Add special handling for command not found errors

Signed-off-by: Claire Wolf <clifford@clifford.at>
4 years agoMerge pull request #67 from mmicko/mmicko/windows_fix
Claire Wolf [Tue, 21 Jan 2020 16:15:27 +0000 (17:15 +0100)]
Merge pull request #67 from mmicko/mmicko/windows_fix

Fix sby execution on Windows

4 years agoAdded sleep for non-posix, allow supported signals
Miodrag Milanovic [Wed, 15 Jan 2020 07:09:11 +0000 (08:09 +0100)]
Added sleep for non-posix, allow supported signals

4 years agoFix sby execution on Windows
Miodrag Milanovic [Sun, 17 Nov 2019 15:58:35 +0000 (16:58 +0100)]
Fix sby execution on Windows

4 years agoUse lowercase for non-final smtbmc status, treat PREUNSAT as ERROR
Clifford Wolf [Thu, 3 Oct 2019 13:00:11 +0000 (15:00 +0200)]
Use lowercase for non-final smtbmc status, treat PREUNSAT as ERROR

Signed-off-by: Clifford Wolf <clifford@clifford.at>
4 years agoFix YosysHQ links
Clifford Wolf [Tue, 13 Aug 2019 15:25:10 +0000 (17:25 +0200)]
Fix YosysHQ links

Signed-off-by: Clifford Wolf <clifford@clifford.at>
4 years agoMerge pull request #55 from YosysHQ/q3k/fix-bash
Clifford Wolf [Thu, 1 Aug 2019 11:02:01 +0000 (13:02 +0200)]
Merge pull request #55 from YosysHQ/q3k/fix-bash

sby_core: fix hardcoded /bin/bash path

4 years agosby_core: fix hardcoded /bin/bash path
Serge Bazanski [Wed, 24 Jul 2019 11:31:37 +0000 (13:31 +0200)]
sby_core: fix hardcoded /bin/bash path

Not all systems (eg. BSDs, NixOS) have a /bin/bash. The de-facto standard for maximum compatibility
these days is using /usr/bin/env bash.

4 years agoDocumentation update: Boolector is using the MIT license now
Clifford Wolf [Tue, 23 Jul 2019 13:24:04 +0000 (15:24 +0200)]
Documentation update: Boolector is using the MIT license now

Signed-off-by: Clifford Wolf <clifford@clifford.at>
4 years agoCleanup some command line option oddities
Clifford Wolf [Thu, 27 Jun 2019 12:06:47 +0000 (14:06 +0200)]
Cleanup some command line option oddities

Signed-off-by: Clifford Wolf <clifford@clifford.at>
4 years agoMerge branch 'feature_file_paths' of https://github.com/gs-jgj/SymbiYosys into staging
Clifford Wolf [Thu, 27 Jun 2019 11:55:25 +0000 (13:55 +0200)]
Merge branch 'feature_file_paths' of https://github.com/gs-jgj/SymbiYosys into staging

4 years agoFix default argument for tasknames
Hans Anderson [Tue, 25 Jun 2019 00:35:52 +0000 (18:35 -0600)]
Fix default argument for tasknames

4 years agoSwitch from getopt to argparse
Hans Anderson [Sat, 22 Jun 2019 01:12:26 +0000 (19:12 -0600)]
Switch from getopt to argparse

4 years agoAdd docs/examples/abstract/.gitignore
Clifford Wolf [Tue, 18 Jun 2019 08:31:55 +0000 (10:31 +0200)]
Add docs/examples/abstract/.gitignore

Signed-off-by: Clifford Wolf <clifford@clifford.at>
4 years agoFix quickstart demo to work with verific
Clifford Wolf [Tue, 18 Jun 2019 08:30:04 +0000 (10:30 +0200)]
Fix quickstart demo to work with verific

Signed-off-by: Clifford Wolf <clifford@clifford.at>
5 years agoMerge pull request #49 from ZipCPU/verilog-doc
Clifford Wolf [Wed, 22 May 2019 09:42:34 +0000 (11:42 +0200)]
Merge pull request #49 from ZipCPU/verilog-doc

Updated Verilog documentation

5 years agoUpdated Verilog documentation
ZipCPU [Wed, 22 May 2019 00:55:46 +0000 (20:55 -0400)]
Updated Verilog documentation

5 years agoAdd dumpfiles command line argument.
Jeppe Johansen [Wed, 8 May 2019 15:08:31 +0000 (17:08 +0200)]
Add dumpfiles command line argument.

Signed-off-by: Jeppe Johansen <jgj@gomspace.com>
5 years agoAdd support for expanding environment variables.
Jeppe Johansen [Wed, 8 May 2019 14:56:33 +0000 (16:56 +0200)]
Add support for expanding environment variables.

Signed-off-by: Jeppe Johansen <jgj@gomspace.com>
5 years agoCheck if config contains any engines, fixes #38
Clifford Wolf [Wed, 1 May 2019 16:47:41 +0000 (18:47 +0200)]
Check if config contains any engines, fixes #38

Signed-off-by: Clifford Wolf <clifford@clifford.at>
5 years agoFix re-run in same directory feature
Clifford Wolf [Tue, 30 Apr 2019 18:03:24 +0000 (20:03 +0200)]
Fix re-run in same directory feature

Signed-off-by: Clifford Wolf <clifford@clifford.at>
5 years agoMerge pull request #42 from mithro/master
Clifford Wolf [Thu, 18 Apr 2019 09:13:10 +0000 (11:13 +0200)]
Merge pull request #42 from mithro/master

Adding some extra licensing information.

5 years agoAdding license info to the top level README file too.
Tim 'mithro' Ansell [Thu, 11 Apr 2019 22:36:19 +0000 (15:36 -0700)]
Adding license info to the top level README file too.

5 years agoAdding top level COPYING file.
Tim 'mithro' Ansell [Thu, 11 Apr 2019 22:32:32 +0000 (15:32 -0700)]
Adding top level COPYING file.

 * Enables github license detection.

5 years agoImprove readability of boolector build instructions
Clifford Wolf [Thu, 28 Mar 2019 07:48:49 +0000 (08:48 +0100)]
Improve readability of boolector build instructions

Signed-off-by: Clifford Wolf <clifford@clifford.at>
5 years agoMinor improvements in docs/examples/abstract/abstr.sv
Clifford Wolf [Wed, 27 Mar 2019 13:49:35 +0000 (14:49 +0100)]
Minor improvements in docs/examples/abstract/abstr.sv

Signed-off-by: Clifford Wolf <clifford@clifford.at>
5 years agoAdd docs/examples/abstract
Clifford Wolf [Wed, 27 Mar 2019 13:45:30 +0000 (14:45 +0100)]
Add docs/examples/abstract

Signed-off-by: Clifford Wolf <clifford@clifford.at>
5 years agoAdd extra "setundef -anyseq" to aiger script
Clifford Wolf [Fri, 22 Mar 2019 12:40:50 +0000 (13:40 +0100)]
Add extra "setundef -anyseq" to aiger script

Signed-off-by: Clifford Wolf <clifford@clifford.at>
5 years agoBackward compatibility with Python 3.4 API
Clifford Wolf [Thu, 21 Mar 2019 19:09:44 +0000 (20:09 +0100)]
Backward compatibility with Python 3.4 API

Signed-off-by: Clifford Wolf <clifford@clifford.at>
5 years agoSignificantly improve management of child processes
Clifford Wolf [Thu, 21 Mar 2019 14:06:49 +0000 (15:06 +0100)]
Significantly improve management of child processes

Signed-off-by: Clifford Wolf <clifford@clifford.at>
5 years agoImprove logfile/output flushing
Clifford Wolf [Wed, 20 Mar 2019 18:08:46 +0000 (19:08 +0100)]
Improve logfile/output flushing

Signed-off-by: Clifford Wolf <clifford@clifford.at>
5 years agoDo not overwrite config.sby in reusedir mode
Clifford Wolf [Fri, 15 Mar 2019 18:36:13 +0000 (19:36 +0100)]
Do not overwrite config.sby in reusedir mode

Signed-off-by: Clifford Wolf <clifford@clifford.at>
5 years agoMerge pull request #33 from cr1901/no-resource
Clifford Wolf [Tue, 19 Mar 2019 13:20:28 +0000 (14:20 +0100)]
Merge pull request #33 from cr1901/no-resource

Meaningful Windows Support

5 years agoAnnotate cmdline comment, summary string, and output XML with
William D. Jones [Mon, 18 Mar 2019 04:46:06 +0000 (00:46 -0400)]
Annotate cmdline comment, summary string, and output XML with
OS-specific information.

5 years agoChoose command separator for tasks based on OS.
William D. Jones [Sat, 16 Mar 2019 03:14:12 +0000 (23:14 -0400)]
Choose command separator for tasks based on OS.

Signed-off-by: William D. Jones <thor0505@comcast.net>
5 years agoMerge pull request #35 from FelixVi/master
Clifford Wolf [Sun, 17 Mar 2019 11:27:44 +0000 (12:27 +0100)]
Merge pull request #35 from FelixVi/master

Update Boolector build instructions