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

Refactoring Verific SVA rewriter

Fix btor concat

Merge branch 'master' into btor-ng

Merge pull request #467 from mithro/patch-1

Fix spelling in -vpr help for synth_ice40

Fix spelling in -vpr help for synth_ice40

Use "hg ... --insecure" for cloning/pulling ABC

Update ABC to hg rev 31fc97b0aeed

Fix error handling for nested always/initial

Merge branch 'master' into btor-ng

Merge pull request #462 from daveshah1/up5k

Add remaining UltraPlus cells to ice40 techlib

Add remaining UltraPlus cells to ice40 techlib

Merge branch 'master' into btor-ng

Fixed "yosys-smtbmc -g" handling of no solution

Fixed "yosys-smtbmc -g" handling of no solution

Merge pull request #460 from mithro/g3-fixes

Bunch of small fixes

Merge pull request #461 from mithro/travis-rework

travis: Print branches before fetching, try both locations.

travis: Print branches before fetching, try both locations.

minisat: Make update script executable.

minisat: Only define __STDC_XXX_MACROS if not already defined.

Replace;
 #define __STDC_LIMIT_MACROS
 #define __STDC_FORMAT_MACROS

With
 #ifndef __STDC_LIMIT_MACROS
 #define __STDC_LIMIT_MACROS
 #endif
 #ifndef __STDC_FORMAT_MACROS
 #define __STDC_FORMAT_MACROS
 #endif

This fixes a compile warning if you are defining these macros in your
CXXFLAGS (as some distros do).

minisat: Remove template with gzFile specialization.

All the other gzFile functions have been removed but this template was
still left around.

subcircuit: Class with virtual methods should have virtual destructor.

Fixes a compile warning.

* https://stackoverflow.com/questions/1123044/when-should-your-destructor-be-virtual

Merge branch 'master' into btor-ng

Bugfixes in new BTOR back-end