Fix verific handling of anyconst/anyseq attributes

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

Merge pull request #454 from rqou/emscripten-and-abc

Add option to statically link abc; emscripten fixes

Force abc to align memory to 8 bytes

Apparently abc has a memory pool implementation that by default returns
memory that is unaligned. There is a workaround in the abc makefile that
uses uname to look for "arm" specifically and then sets the alignment.
However, ARM is not the only platform that requires proper alignment
(e.g. emscripten does too). For now, pessimistically force the alignment
for 8 bytes all the time (somehow 4 wasn't enough for fixing emscripten
despite being approximately a 32-bit platform).

Modify emscripten main to mount nodefs and to run arg as a script

Force abc to be linked statically and without threads in emscripten

Fix infinite loop in abc command under emscripten

Fix reading techlibs under emscripten

Add options to disable abc's usage of pthreads and readline

Add an option to statically link abc into yosys

This is currently incomplete because the output filter no longer works.

Makefile: Make abc always use stdint.h

Merge pull request #550 from jimparis/yosys-upstream

Support SystemVerilog `` extension for macros

Merge pull request #551 from olofk/ice40_cells_sim_ports

Avoid mixing module port declaration styles in ice40 cells_sim.v

Avoid mixing module port declaration styles in ice40 cells_sim.v

The current code requires workarounds for several simulators
For modelsim, the file must be compiled with -mixedansiports and
xsim needs --relax.

Support SystemVerilog `` extension for macros

Skip spaces around macro arguments

Fix handling of anyconst/anyseq attrs in VHDL code via Verific

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

Remove mercurial from build instructions

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

Fix iopadmap for loops between tristate IO buffers

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

Fix iopadmap for cases where IO pins already have buffers on them

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

Some cleanups in setundef.cc

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

Use $(OS) in makefile to check for Darwin

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

Merge pull request #505 from thefallenidealist/FreeBSD_build

FreeBSD build

Add "#ifdef __FreeBSD__"

(Re-commit e3575a8 with corrected author field)

Revert "Add "#ifdef __FreeBSD__""

This reverts commit e3575a86c525f2511902e7022893c3923ba8093e.

Also interpret '&' in liberty functions

Add optimization of tristate buffer with constant control input

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

Add "hierarchy -simcheck"

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

update README

autotest.sh: Change from /bin/bash to /usr/bin/env bash

This enables running tests on Unix systems which are not shipped with
bash installed in /bin/bash (eg *BSDs and Solaris).

Enable building on FreeBSD

Further improve handling of zero-length SVA consecutive repetition

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

Fix handling of zero-length SVA consecutive repetition

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

Add "#ifdef __FreeBSD__"

Add ABC FAQ to "help abc"

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

Add "yosys -e regex" for turning warnings into errors

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

Merge pull request #537 from mithro/yosys-vpr

Improving Yosys when used with VPR

Replace -ignore_redef with -[no]overwrite

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

Support more character literals

Update ABC to git rev f23ea8e

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

Add "synth_intel --noiopads"

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

Add $dlatch support to write_verilog

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

Improving vpr output support.

 * Support output BLIF for Xilinx architectures.
 * Support using .names in BLIF for Xilinx architectures.
 * Use the same `NO_LUT` define in both `synth_ice40` and
  `synth_xilinx`.

synth_ice40: Rework the vpr blif output slightly.

Add "synth_ice40 -nodffe"

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

Add "write_blif -inames -iattr"

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

Add statement labels for immediate assertions

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

Allow "property" in immediate assertions

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

Improve Makefile error handling for when abc/ is a hg working copy

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

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>