Add PRIM_HDL_ASSERTION support to Verific importer

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

Fix handling of $global_clocking in Verific

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

Add documentation for anyconst/anyseq/allconst/allseq attribute

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

Add read_verilog anyseq/anyconst/allseq/allconst attribute support

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

Add Verific anyseq/anyconst/allseq/allconst attribute support

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

Add "verific -autocover"

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

Merge pull request #530 from makaimann/set-ram-flags

Set RAM runtime flags for Verific frontend

Set RAM runtime flags for Verific frontend

Added missing dont_use handling for SR FFs to dfflibmap

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

Create issue_template.md

Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants

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

Fixed -stbv handling in SMT2 back-end

Merge pull request #522 from c60k28/master

Fixed broken Quartus backend on dffeas init value, and other updates.

Fixed broken Quartus backend on dffeas init value (Error (12170): Illegal value  for the POWER_UP parameter. Fixed and tested Cyclone V device

Remove left-over log_ping debug commands.. oops.

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

Merge pull request #521 from azonenberg/for_clifford

coolrunner2: Improve optimization for TFF/counters

coolrunner2: Add an ANDTERM/XOR between chained FFs

In some cases (e.g. the low bits of counters) the design might end up
with a flip-flop whose input is directly driven by another flip-flop.
This isn't possible in the Coolrunner-II architecture, so add a single
AND term and XOR in this case.

coolrunner2: Split multi-bit nets

The PAR tool doesn't expect any "dangling" nets with no drivers nor
sinks. By splitting the nets, clean removes them.

coolrunner2: Add extraction for TFFs

Add smtio status msgs when --progress is inactive

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

Bugfix in smtio.py VCD file generator

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

Removed $timescale from "sat" command VCD writer

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

Set stack size to at least 128 MB (large stack needed for parsing huge expressions)

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

Fix tests/simple/specify.v

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

First draft of Verilog parser support for specify blocks and parameters.
The only functionality of this code at the moment is to accept correct specify syntax and ignore it.
No part of the specify block is added to the AST

Merge pull request #515 from edcote/patch-1

Rename rename to renames

Chenged "extensions_map" to "extensions_list" in hierarchy.cc

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

Merge pull request #518 from xerpi/master

passes/hierarchy: Reduce code duplication in expand_module

passes/hierarchy: Reduce code duplication in expand_module

This also makes it easier to add new file extensions support.

Signed-off-by: Sergi Granell <xerpi.g.12@gmail.com>

Add $mem support to SMT2 clock tagging

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

Fix build for new ABC location on github, also update ABC to a2d59be

Add .sv support to "hierarchy -libdir"

Fix handling of unclocked immediate assertions in Verific front-end

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

Rename rename to renames

Create TCL alias for rename command.  Using renames.  Following the same convention as proc -> procs.

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>