Install launcher executable when running on Windows.

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

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>

Add more documentation

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

Add fib example using tasks

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

Slightly change tasks syntax

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

Add documentation for [tasks] section

Add tasks in .sby files

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

Add multiclock option

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

Add smtbmc --stdt option

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

Fix --dump-smt2 trace name in cover mode

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

Add primegen example

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

Add wolf_goat_cabbage.sby

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

Add engines documentation

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

Merge pull request #4 from daveshah1/fix_filetop

Ignore whitespace at top of file

Ignore whitespace at top of file

Signed-off-by: David Shah <davey1576@gmail.com>

Improve handling of comments in .sby files

Add DESTDIR and PREFIX to Makefile

Disable unrolling per default for z3

Add dpmem multiclk example

Make --presat and --unroll the default for smtbmc

Add "sby -t", improve handling of stdin

Merge pull request #2 from awygle/scriptability

Support parsing sby file from stdin

Minimum-modification change for stdin support

Add missing prerequisites to quickstart guide

Add "smtbmc --dumpsmt2"

Add "smtbmc --unroll"

Add wolf_goat_cabbage.v puzzle solver

Remove AIGER from install section

Add gperf to prerequisites

Update quickstart.rst

Add "smtbmc --presat"

Add tbtop config option

Add "setundef -anyseq" to default yosys script

Add support for "aigsmt none" option

Yices 2 is the new default solver for yosys-smtbmc

Add "Reactive Synthesis" as TBD to documentation

Add support for --pycode-begin/end-- sections

Add avy install instructions

Fix CEX handle in liveness checking mode

Update docs

Add "mode live" support

Add support for AIGER solvers that do not return a CEX

Add smtc option

Add rc to DONE msg

Improve option handling

Fix typo in aiger engine

Improve super_prove integration

Add "append" option

Add aigbmc support