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

Add aigsmt option

Add smtbmc stbv support

Add aiger engine

Update documentation

Use smtbmc args for solver options

Fix readline() handling for partial lines

Fix "smtbmc --syn" and "smtbmc --nomem"

Add options to set tool paths

Add support for "[file <filename>]" .sby sections

Add docs for "wait" option, more config checking

Fix bug in job.terminate()

Add support for "wait" option

Update docs

Add "timeout" option

Add "expect" config option

Add "cover" mode