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

Update ABC to hg rev 6e3c24b3308a

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

Merge pull request #479 from Fatsie/latch_without_data

Some standard cell libraries include a latch with only set/reset.

Bugfix in hierarchy handling of blackbox module ports

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

Merge pull request #480 from Fatsie/liberty_value_expression

Value of properties can be expression.

Temporarily derive blackbox modules in hierarchy to evaluate port widths

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

Value of properties can be expression.

Example found in the 2007.03 Liberty Reference Manual that was also found
in the wild:

    input_voltage(CMOS) {
        vil : 0.3 * VDD ;
        vih : 0.7 * VDD ;
        vimin : -0.5 ;
        vimax : VDD + 0.5 ;
    }

Current implementation just parses the expression but no interpretation is done.

Some standard cell libraries include a latch with only set/reset.

Add "no driver for signal bit" error msg to btor back-end

Bugfix in verilog_defaults argument parser

Fix minor typo in "prep" help message

Simple fix BTOR memory encoding

Improve BTOR memory encoding

Merge branch 'btor-ng'

Add array support to btor back-end

Add $anyconst/$anyseq support to btor back-end

Merge branch 'master' into btor-ng

Add yosys-smtbmc VCD writer support for memories with async writes

Fix a bug in clk2fflogic memory handling

Merge branch 'master' into btor-ng

Add clk2fflogic memory support

Add smt2 back-end support for async write memories

Add RTLIL::Const::is_fully_ones()

Add SigSpec::is_fully_ones()

Merge pull request #469 from kkiningh/master

Use quote includes for yosys.h

Use quote includes for yosys.h

Check for memories in clk2fflogic

Merge pull request #468 from grahamedgecombe/fix-sb-io-od

Fix SB_IO_OD module

Add "write_btor -s" mode

Add state initval handling to btor back-end

Add btor back-end support for 'x' constants

Add SigSpec::is_fully_ones()

Add warnings for driver-driver conflicts between FFs (and other cells) and constants

Add btor $shift/$shiftx support

Fix port names in SB_IO_OD

Remove trailing comma from SB_IO_OD port list

This isn't compatible with Icarus Verilog.

Fix btor back-end shift handling

Add support for $pmux in btor back-end

Add support for more cell types to btor back-end

Merge branch 'master' into btor-ng

Add support for Verific PRIM_SVA_NOT properties

Add Verific OPER_SVA_STABLE support