Fix handling of unclocked immediate assertions in Verific front-end

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

Improve yosys-smtbmc log output and error handling

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

Improve handling of invalid check-sat result in smtio.py

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

Update todo for more features to verificsva.cc

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

Update todo for more features to verificsva.cc

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

Add todo for more features to verificsva.cc

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

Improve import of memories via Verific

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

Fix handling of SV compilation units in Verific front-end

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

Add "expose -input"

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

Add "setundef -undef"

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

Squelch trailing whitespace, including meta-whitespace

Harmonize uses of _WIN32 macro

Fix SVA handling of NON_CONSECUTIVE_REPEAT and GOTO_REPEAT

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

Fix variable name typo in verificsva.cc

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

Add support for trivial SVA sequences and properties

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

Fix handling of src attributes in flatten

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

Remove debug prints from yosys-smtbmc VCD writer

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

Use Verific hier_tree component for elaboration

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

Check results of (check-sat) in yosys-smtbmc

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

Fix Verific handling of "assert property (..);" in always block

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

Add "verific -import -V"

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

Set Verific db_preserve_user_nets flag

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

Add Xilinx RAM64X1D and RAM128X1D simulation models

Add "memory_nordff" pass

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

Update comment about supported SVA in verificsva.cc

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

Add SVA NON_CONSECUTIVE_REPEAT and GOTO_REPEAT support

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

Add SVA first_match() support

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

Add SVA within support

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

Add support for SVA sequence intersect

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

Add get_fsm_accept_reject for parsing SVA properties

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

Simplified SVA "until" handling

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

Imporove yosys-smtbmc error handling, Improve VCD output

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

Fix connwrappers help message

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

Improve handling of warning messages

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

Update copyright header

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

Improve SMT2 encoding of $reduce_{and,or,bool}

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

Fix a hangup in yosys-smtbmc error handling

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

Add proper SVA seq.triggered support

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

Add "synth -noshare"

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

Add Verific SVA support for "seq and seq" expressions

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

Refactor Verific SVA importer property parser

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

Add VerificClocking class and refactor Verific DFF handling

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

Improved error handling in yosys-smtbmc

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

Add SVA support for sequence OR

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

Terminate running SMT solver when smtbmc is terminated

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

Fix smtbmc smtc/aiw parser for wire names containing []

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

Fix handling of SVA "until seq.triggered" properties

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

Update SVA cheat sheet in verificsva.cc

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

Fix in Verific SVA importer handling of until_with

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

Mangle names with square brackets in VCD files to work around issues in gtkwave

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

Fixes and improvements in Verific SVA importer

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

Add $rose/$fell support to Verific bindings

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

Merge branch 'verificsva-ng'

Add support for PRIM_SVA_UNTIL to new SVA importer

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

Add DFSM generator to verific SVA importer

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

Continue refactoring of Verific SVA importer code

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

Major redesign of Verific SVA importer

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

Add -lz for verific builds

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

Add handling of verific OPER_REDUCE_NOR

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

Add handling of verific OPER_SELECTOR and OPER_WIDE_SELECTOR

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

Add handling of verific OPER_NTO1MUX and OPER_WIDE_NTO1MUX

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

Add "SVA syntax cheat sheet" comment to verificsva.cc

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

Add $dlatchsr support to clk2fflogic

Small fixes and improvements in $allconst/$allseq handling

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

Fix opt_rmdff handling of $dlatchsr

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

Merge branch 'forall'

Add smtbmc support for exist-forall problems

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

Add $allconst and $allseq cell types

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

Add Verific SVA support for ranges in repetition operator

Add support for SVA throughout via Verific

Add support for mockup clock signals in yosys-smtbmc vcd output

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

Merge pull request #507 from cr1901/msys2

Improve msys2 flags for building abc.

Improve msys2 flags for building abc.

Add support for SVA sequence concatenation ranges via verific

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

Add support for SVA until statements via Verific

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

Move Verific SVA importer to extra C++ source file

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

Merge Verific SVA preprocessor and SVA importer

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

Improve handling of "bus" pins in liberty front-end (some files use bus.pin.direction)

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

Fix verific PRIM_SVA_AT handling in properties with PRIM_SVA_DISABLE_IFF

Fixed yosys-config for binary distributions with Verific

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

Recognize stand-alone obj pattern even when it contains a slash

Fix handling of zero-length cell connections in SMT2 back-end

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

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

Do not create deep backtraces unless in ENABLE_DEBUG mode

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

Merge pull request #488 from azonenberg/for_clifford

coolrunner2: Move LOC attributes onto the IO cells

Fixed gcc 7.2 "statement will never be executed" warning

Fix single-bit $stable handling in verific front-end

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

Add Verific attribute handling for assert/assume/cover/live/fair cells

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

Fix smtio.py for large SMT2 S-expressions

Fix permissions on verific vdb files

Fixed handling of synchronous and asynchronous assertion/assumption/cover in verific bindings

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

Use "strip -S" instead of "strip -d" for Mac OS X compatibility

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

Improve log messages in equiv_make

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

Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output

coolrunner2: Move LOC attributes onto the IO cells

Strip debug symbols from binaries on install

Add "dffinit -highlow" and fix synth_intel

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

Add support for "yosys -E"

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

Bugfix in hierarchy blackbox module port width handling