Fix primegen example

Signed-off-by: Claire Wolf <claire@symbioticeda.com>

Improve BTOR and AIG yosys scripts

Signed-off-by: Claire Wolf <clifford@clifford.at>

Merge pull request #70 from dh73/master

Fix typo in log message

Fix typo in log message

Add special handling for command not found errors

Signed-off-by: Claire Wolf <clifford@clifford.at>

Merge pull request #67 from mmicko/mmicko/windows_fix

Fix sby execution on Windows

Added sleep for non-posix, allow supported signals

Fix sby execution on Windows

Use lowercase for non-final smtbmc status, treat PREUNSAT as ERROR

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Fix YosysHQ links

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Merge pull request #55 from YosysHQ/q3k/fix-bash

sby_core: fix hardcoded /bin/bash path

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.

Documentation update: Boolector is using the MIT license now

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Cleanup some command line option oddities

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Merge branch 'feature_file_paths' of https://github.com/gs-jgj/SymbiYosys into staging

Fix default argument for tasknames

Switch from getopt to argparse

Add docs/examples/abstract/.gitignore

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Fix quickstart demo to work with verific

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Merge pull request #49 from ZipCPU/verilog-doc

Updated Verilog documentation

Updated Verilog documentation

Add dumpfiles command line argument.

Signed-off-by: Jeppe Johansen <jgj@gomspace.com>

Add support for expanding environment variables.

Signed-off-by: Jeppe Johansen <jgj@gomspace.com>

Check if config contains any engines, fixes #38

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Fix re-run in same directory feature

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Merge pull request #42 from mithro/master

Adding some extra licensing information.

Adding license info to the top level README file too.

Adding top level COPYING file.

 * Enables github license detection.

Improve readability of boolector build instructions

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Minor improvements in docs/examples/abstract/abstr.sv

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add docs/examples/abstract

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add extra "setundef -anyseq" to aiger script

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Backward compatibility with Python 3.4 API

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Significantly improve management of child processes

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Improve logfile/output flushing

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Do not overwrite config.sby in reusedir mode

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Merge pull request #33 from cr1901/no-resource

Meaningful Windows Support

Annotate cmdline comment, summary string, and output XML with
OS-specific information.

Choose command separator for tasks based on OS.

Signed-off-by: William D. Jones <thor0505@comcast.net>

Merge pull request #35 from FelixVi/master

Update Boolector build instructions

Update Boolector build instructions

Rename ".stamp" file to "status"

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Merge branch 'master' into no-resource

Merge pull request #32 from cr1901/win-shell

Install launcher executable when running on Windows. Fixes #30.

Install launcher executable when running on Windows.

Signed-off-by: William D. Jones <thor0505@comcast.net>

Gate Unix-specific functionality from resources and fcntl.

Signed-off-by: William D. Jones <thor0505@comcast.net>

Improve rerun-in-existing-dir functionality

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add support for (re-)running in existing workdir

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add --dumptasks to documentation

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Improve sby file pycode/tasks handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add --dumpcfg and --dumptasks

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Further improve BTOR cex handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Improve BTOR cex handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Also add install docs for btorsim

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Update boolector build instructions

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Fixes and improvements in BTOR engine

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Merge pull request #22 from YosysHQ/btor

Btor BMC engine

Working BTOR BMC engine

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add btor engine

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add "smtbmc ... -- ..." feature (for "raw" smtbmc options)

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Generate AIGERs with -I -B

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Improve bogus task tags detection

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Detect bogus task tags

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add "skip" options (smtbmc only)

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Update docs

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Update README.md

Add "pour_853_4" puzzle to examples

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Fixed "counterexample trace:" log message for things like warmup failed

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Fixed bug in examples/quickstart/demo.sv

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Use async2sync for "multiclock off" mode

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Update examples

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Update remaining quickstart examples

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Update quickstart demo

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Improve documentation of scripts and Verific bindings

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Use "multiclock on" option in dpmem.sby example

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Use "hierarchy -simcheck" in default script

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Fix fix for chained tasks

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Fix bug in handling of chained tasks

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add comment support in [tasks] section

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add [script] documentation, add some paragraphs on "verific" command

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Typo fix

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add check for malformed dst filename in [files] section

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add documentation on [files] and [file ..] sections

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add JUnit XML output file and .stamp files

Signed-off-by: Clifford Wolf <clifford@clifford.at>

More improvements in sby error handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Drastically improve sby error handling

Improve handling of nomem models

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add localtime also to early log messages

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add localtime to log file

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Extend primegen example

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add "smtbmc --basecase/--induction"

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add smtbmc --progress option

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Add "mkdir -p" to "make install"

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Update verific.rst

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Merge branch 'master' of github.com:cliffordwolf/SymbiYosys

Use memory_nordff in postprocess script

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Improvements in [tasks] handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Update verific.rst

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Update verific.rst

Signed-off-by: Clifford Wolf <clifford@clifford.at>

Minor format fix in documentation

Signed-off-by: Clifford Wolf <clifford@clifford.at>