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

Improve "abc sim3" handling

Add support for "abc sim3" engine

Fix bug in /examples/quickstart/prove.v

Add some docs for "prove" mode

Add smtbmc prove support

Added prove mode support via "abc pdr"

Fix typo

Improve docs

Improve quickstart memory example

Fix bug in task management

Refactor engine/mode interfaces

Improve bmc task management

Use new "yosys-smtbmc --aig <aim>:<aiw>" feature

Fix "abc bmc3" engine for small state spaces

Improve documentation

Improve documentation

Fix handling of counter examples with "abc bmc3" engine

Fix error handling in model creation

Rename "abc_bmc3" engine to "abc bmc3"

Add AIGER cex support

Improve docs

Fix handling of empty src dir

Add .gitignore