yosys.git
6 years agoupdate README
Johnny Sorocil [Sun, 6 May 2018 16:22:18 +0000 (18:22 +0200)]
update README

6 years agoautotest.sh: Change from /bin/bash to /usr/bin/env bash
Johnny Sorocil [Sun, 6 May 2018 13:26:23 +0000 (15:26 +0200)]
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).

6 years agoEnable building on FreeBSD
Johnny Sorocil [Sun, 6 May 2018 13:19:44 +0000 (15:19 +0200)]
Enable building on FreeBSD

6 years agoFurther improve handling of zero-length SVA consecutive repetition
Clifford Wolf [Sat, 5 May 2018 12:32:04 +0000 (14:32 +0200)]
Further improve handling of zero-length SVA consecutive repetition

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix handling of zero-length SVA consecutive repetition
Clifford Wolf [Sat, 5 May 2018 11:58:01 +0000 (13:58 +0200)]
Fix handling of zero-length SVA consecutive repetition

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd "#ifdef __FreeBSD__"
Johnny Sorocil [Sat, 5 May 2018 11:02:44 +0000 (13:02 +0200)]
Add "#ifdef __FreeBSD__"

6 years agoAdd ABC FAQ to "help abc"
Clifford Wolf [Fri, 4 May 2018 19:59:31 +0000 (21:59 +0200)]
Add ABC FAQ to "help abc"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd "yosys -e regex" for turning warnings into errors
Clifford Wolf [Fri, 4 May 2018 13:27:28 +0000 (15:27 +0200)]
Add "yosys -e regex" for turning warnings into errors

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMerge pull request #537 from mithro/yosys-vpr
Clifford Wolf [Fri, 4 May 2018 10:32:30 +0000 (12:32 +0200)]
Merge pull request #537 from mithro/yosys-vpr

Improving Yosys when used with VPR

6 years agoReplace -ignore_redef with -[no]overwrite
Clifford Wolf [Thu, 3 May 2018 13:25:59 +0000 (15:25 +0200)]
Replace -ignore_redef with -[no]overwrite

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoSupport more character literals
Dan Gisselquist [Thu, 3 May 2018 10:35:01 +0000 (12:35 +0200)]
Support more character literals

6 years agoUpdate ABC to git rev f23ea8e
Clifford Wolf [Mon, 30 Apr 2018 17:50:34 +0000 (19:50 +0200)]
Update ABC to git rev f23ea8e

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd "synth_intel --noiopads"
Clifford Wolf [Mon, 30 Apr 2018 11:02:56 +0000 (13:02 +0200)]
Add "synth_intel --noiopads"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd $dlatch support to write_verilog
Clifford Wolf [Sun, 22 Apr 2018 14:03:26 +0000 (16:03 +0200)]
Add $dlatch support to write_verilog

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoImproving vpr output support.
Tim 'mithro' Ansell [Wed, 18 Apr 2018 23:48:05 +0000 (16:48 -0700)]
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`.

6 years agosynth_ice40: Rework the vpr blif output slightly.
Tim 'mithro' Ansell [Sun, 15 Apr 2018 23:05:52 +0000 (16:05 -0700)]
synth_ice40: Rework the vpr blif output slightly.

6 years agoAdd "synth_ice40 -nodffe"
Clifford Wolf [Mon, 16 Apr 2018 18:44:26 +0000 (20:44 +0200)]
Add "synth_ice40 -nodffe"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd "write_blif -inames -iattr"
Clifford Wolf [Sun, 15 Apr 2018 12:07:21 +0000 (14:07 +0200)]
Add "write_blif -inames -iattr"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd statement labels for immediate assertions
Clifford Wolf [Fri, 13 Apr 2018 09:52:28 +0000 (11:52 +0200)]
Add statement labels for immediate assertions

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAllow "property" in immediate assertions
Clifford Wolf [Thu, 12 Apr 2018 12:28:28 +0000 (14:28 +0200)]
Allow "property" in immediate assertions

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoImprove Makefile error handling for when abc/ is a hg working copy
Clifford Wolf [Thu, 12 Apr 2018 12:02:57 +0000 (14:02 +0200)]
Improve Makefile error handling for when abc/ is a hg working copy

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd PRIM_HDL_ASSERTION support to Verific importer
Clifford Wolf [Sat, 7 Apr 2018 16:38:42 +0000 (18:38 +0200)]
Add PRIM_HDL_ASSERTION support to Verific importer

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix handling of $global_clocking in Verific
Clifford Wolf [Fri, 6 Apr 2018 19:23:47 +0000 (21:23 +0200)]
Fix handling of $global_clocking in Verific

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd documentation for anyconst/anyseq/allconst/allseq attribute
Clifford Wolf [Fri, 6 Apr 2018 12:37:43 +0000 (14:37 +0200)]
Add documentation for anyconst/anyseq/allconst/allseq attribute

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd read_verilog anyseq/anyconst/allseq/allconst attribute support
Clifford Wolf [Fri, 6 Apr 2018 12:35:11 +0000 (14:35 +0200)]
Add read_verilog anyseq/anyconst/allseq/allconst attribute support

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd Verific anyseq/anyconst/allseq/allconst attribute support
Clifford Wolf [Fri, 6 Apr 2018 12:19:55 +0000 (14:19 +0200)]
Add Verific anyseq/anyconst/allseq/allconst attribute support

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd "verific -autocover"
Clifford Wolf [Fri, 6 Apr 2018 12:10:57 +0000 (14:10 +0200)]
Add "verific -autocover"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMerge pull request #530 from makaimann/set-ram-flags
Clifford Wolf [Fri, 6 Apr 2018 11:50:23 +0000 (13:50 +0200)]
Merge pull request #530 from makaimann/set-ram-flags

Set RAM runtime flags for Verific frontend

6 years agoSet RAM runtime flags for Verific frontend
makaimann [Fri, 6 Apr 2018 00:38:08 +0000 (17:38 -0700)]
Set RAM runtime flags for Verific frontend

6 years agoAdded missing dont_use handling for SR FFs to dfflibmap
Clifford Wolf [Thu, 5 Apr 2018 09:01:32 +0000 (11:01 +0200)]
Added missing dont_use handling for SR FFs to dfflibmap

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoCreate issue_template.md
Clifford Wolf [Wed, 4 Apr 2018 17:27:33 +0000 (19:27 +0200)]
Create issue_template.md

6 years agoAdd smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants
Clifford Wolf [Wed, 4 Apr 2018 16:12:27 +0000 (18:12 +0200)]
Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFixed -stbv handling in SMT2 back-end
Clifford Wolf [Wed, 4 Apr 2018 15:28:07 +0000 (17:28 +0200)]
Fixed -stbv handling in SMT2 back-end

6 years agoMerge pull request #522 from c60k28/master
Clifford Wolf [Sun, 1 Apr 2018 13:32:47 +0000 (15:32 +0200)]
Merge pull request #522 from c60k28/master

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

6 years agoFixed broken Quartus backend on dffeas init value (Error (12170): Illegal value ...
c60k28 [Sun, 1 Apr 2018 04:48:47 +0000 (22:48 -0600)]
Fixed broken Quartus backend on dffeas init value (Error (12170): Illegal value  for the POWER_UP parameter. Fixed and tested Cyclone V device

6 years agoRemove left-over log_ping debug commands.. oops.
Clifford Wolf [Sat, 31 Mar 2018 12:23:57 +0000 (14:23 +0200)]
Remove left-over log_ping debug commands.. oops.

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMerge pull request #521 from azonenberg/for_clifford
Clifford Wolf [Sat, 31 Mar 2018 11:31:01 +0000 (13:31 +0200)]
Merge pull request #521 from azonenberg/for_clifford

coolrunner2: Improve optimization for TFF/counters

6 years agocoolrunner2: Add an ANDTERM/XOR between chained FFs
Robert Ou [Sat, 31 Mar 2018 10:54:48 +0000 (03:54 -0700)]
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.

6 years agocoolrunner2: Split multi-bit nets
Robert Ou [Sat, 31 Mar 2018 09:56:11 +0000 (02:56 -0700)]
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.

6 years agocoolrunner2: Add extraction for TFFs
Robert Ou [Sat, 31 Mar 2018 09:54:26 +0000 (02:54 -0700)]
coolrunner2: Add extraction for TFFs

6 years agoAdd smtio status msgs when --progress is inactive
Clifford Wolf [Thu, 29 Mar 2018 19:59:30 +0000 (21:59 +0200)]
Add smtio status msgs when --progress is inactive

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoBugfix in smtio.py VCD file generator
Clifford Wolf [Thu, 29 Mar 2018 10:45:31 +0000 (12:45 +0200)]
Bugfix in smtio.py VCD file generator

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoRemoved $timescale from "sat" command VCD writer
Clifford Wolf [Thu, 29 Mar 2018 10:38:41 +0000 (12:38 +0200)]
Removed $timescale from "sat" command VCD writer

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoSet stack size to at least 128 MB (large stack needed for parsing huge expressions)
Clifford Wolf [Tue, 27 Mar 2018 13:04:10 +0000 (15:04 +0200)]
Set stack size to at least 128 MB (large stack needed for parsing huge expressions)

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix tests/simple/specify.v
Clifford Wolf [Tue, 27 Mar 2018 12:31:19 +0000 (14:31 +0200)]
Fix tests/simple/specify.v

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFirst draft of Verilog parser support for specify blocks and parameters.
Udi Finkelstein [Sun, 4 Mar 2018 21:35:08 +0000 (23:35 +0200)]
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

6 years agoMerge pull request #515 from edcote/patch-1
Clifford Wolf [Tue, 27 Mar 2018 12:14:51 +0000 (14:14 +0200)]
Merge pull request #515 from edcote/patch-1

Rename rename to renames

6 years agoChenged "extensions_map" to "extensions_list" in hierarchy.cc
Clifford Wolf [Tue, 27 Mar 2018 12:12:57 +0000 (14:12 +0200)]
Chenged "extensions_map" to "extensions_list" in hierarchy.cc

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMerge pull request #518 from xerpi/master
Clifford Wolf [Tue, 27 Mar 2018 12:10:39 +0000 (14:10 +0200)]
Merge pull request #518 from xerpi/master

passes/hierarchy: Reduce code duplication in expand_module

6 years agopasses/hierarchy: Reduce code duplication in expand_module
Sergi Granell [Tue, 27 Mar 2018 07:35:20 +0000 (09:35 +0200)]
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>
6 years agoAdd $mem support to SMT2 clock tagging
Clifford Wolf [Tue, 27 Mar 2018 00:11:20 +0000 (02:11 +0200)]
Add $mem support to SMT2 clock tagging

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix build for new ABC location on github, also update ABC to a2d59be
Clifford Wolf [Mon, 26 Mar 2018 22:39:01 +0000 (00:39 +0200)]
Fix build for new ABC location on github, also update ABC to a2d59be

6 years agoAdd .sv support to "hierarchy -libdir"
Clifford Wolf [Mon, 26 Mar 2018 19:19:00 +0000 (21:19 +0200)]
Add .sv support to "hierarchy -libdir"

6 years agoFix handling of unclocked immediate assertions in Verific front-end
Clifford Wolf [Mon, 26 Mar 2018 11:04:10 +0000 (13:04 +0200)]
Fix handling of unclocked immediate assertions in Verific front-end

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoRename rename to renames
Edmond Cote [Tue, 20 Mar 2018 22:50:50 +0000 (15:50 -0700)]
Rename rename to renames

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

6 years agoImprove yosys-smtbmc log output and error handling
Clifford Wolf [Sat, 17 Mar 2018 17:06:17 +0000 (18:06 +0100)]
Improve yosys-smtbmc log output and error handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoImprove handling of invalid check-sat result in smtio.py
Clifford Wolf [Sat, 17 Mar 2018 11:17:53 +0000 (12:17 +0100)]
Improve handling of invalid check-sat result in smtio.py

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoUpdate todo for more features to verificsva.cc
Clifford Wolf [Fri, 16 Mar 2018 14:48:48 +0000 (15:48 +0100)]
Update todo for more features to verificsva.cc

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoUpdate todo for more features to verificsva.cc
Clifford Wolf [Fri, 16 Mar 2018 11:16:52 +0000 (12:16 +0100)]
Update todo for more features to verificsva.cc

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd todo for more features to verificsva.cc
Clifford Wolf [Fri, 16 Mar 2018 11:15:36 +0000 (12:15 +0100)]
Add todo for more features to verificsva.cc

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoImprove import of memories via Verific
Clifford Wolf [Thu, 15 Mar 2018 17:20:37 +0000 (18:20 +0100)]
Improve import of memories via Verific

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix handling of SV compilation units in Verific front-end
Clifford Wolf [Wed, 14 Mar 2018 19:22:11 +0000 (20:22 +0100)]
Fix handling of SV compilation units in Verific front-end

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd "expose -input"
Clifford Wolf [Mon, 12 Mar 2018 12:52:52 +0000 (13:52 +0100)]
Add "expose -input"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd "setundef -undef"
Clifford Wolf [Mon, 12 Mar 2018 12:52:35 +0000 (13:52 +0100)]
Add "setundef -undef"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoSquelch trailing whitespace, including meta-whitespace
Larry Doolittle [Sat, 10 Mar 2018 17:59:06 +0000 (09:59 -0800)]
Squelch trailing whitespace, including meta-whitespace

6 years agoHarmonize uses of _WIN32 macro
Larry Doolittle [Tue, 6 Mar 2018 17:43:42 +0000 (09:43 -0800)]
Harmonize uses of _WIN32 macro

6 years agoFix SVA handling of NON_CONSECUTIVE_REPEAT and GOTO_REPEAT
Clifford Wolf [Sat, 10 Mar 2018 15:24:01 +0000 (16:24 +0100)]
Fix SVA handling of NON_CONSECUTIVE_REPEAT and GOTO_REPEAT

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix variable name typo in verificsva.cc
Clifford Wolf [Sat, 10 Mar 2018 13:33:42 +0000 (14:33 +0100)]
Fix variable name typo in verificsva.cc

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd support for trivial SVA sequences and properties
Clifford Wolf [Sat, 10 Mar 2018 13:32:01 +0000 (14:32 +0100)]
Add support for trivial SVA sequences and properties

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix handling of src attributes in flatten
Clifford Wolf [Sat, 10 Mar 2018 12:55:30 +0000 (13:55 +0100)]
Fix handling of src attributes in flatten

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoRemove debug prints from yosys-smtbmc VCD writer
Clifford Wolf [Thu, 8 Mar 2018 15:24:35 +0000 (16:24 +0100)]
Remove debug prints from yosys-smtbmc VCD writer

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoUse Verific hier_tree component for elaboration
Clifford Wolf [Thu, 8 Mar 2018 12:26:33 +0000 (13:26 +0100)]
Use Verific hier_tree component for elaboration

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoCheck results of (check-sat) in yosys-smtbmc
Clifford Wolf [Wed, 7 Mar 2018 21:54:19 +0000 (22:54 +0100)]
Check results of (check-sat) in yosys-smtbmc

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix Verific handling of "assert property (..);" in always block
Clifford Wolf [Wed, 7 Mar 2018 19:06:02 +0000 (20:06 +0100)]
Fix Verific handling of "assert property (..);" in always block

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd "verific -import -V"
Clifford Wolf [Wed, 7 Mar 2018 18:40:34 +0000 (19:40 +0100)]
Add "verific -import -V"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoSet Verific db_preserve_user_nets flag
Clifford Wolf [Wed, 7 Mar 2018 17:08:03 +0000 (18:08 +0100)]
Set Verific db_preserve_user_nets flag

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd Xilinx RAM64X1D and RAM128X1D simulation models
Clifford Wolf [Wed, 7 Mar 2018 16:31:07 +0000 (17:31 +0100)]
Add Xilinx RAM64X1D and RAM128X1D simulation models

6 years agoAdd "memory_nordff" pass
Clifford Wolf [Tue, 6 Mar 2018 22:31:51 +0000 (23:31 +0100)]
Add "memory_nordff" pass

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoUpdate comment about supported SVA in verificsva.cc
Clifford Wolf [Tue, 6 Mar 2018 14:47:33 +0000 (15:47 +0100)]
Update comment about supported SVA in verificsva.cc

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd SVA NON_CONSECUTIVE_REPEAT and GOTO_REPEAT support
Clifford Wolf [Tue, 6 Mar 2018 14:39:46 +0000 (15:39 +0100)]
Add SVA NON_CONSECUTIVE_REPEAT and GOTO_REPEAT support

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd SVA first_match() support
Clifford Wolf [Tue, 6 Mar 2018 14:06:35 +0000 (15:06 +0100)]
Add SVA first_match() support

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd SVA within support
Clifford Wolf [Tue, 6 Mar 2018 13:41:27 +0000 (14:41 +0100)]
Add SVA within support

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd support for SVA sequence intersect
Clifford Wolf [Tue, 6 Mar 2018 13:26:57 +0000 (14:26 +0100)]
Add support for SVA sequence intersect

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd get_fsm_accept_reject for parsing SVA properties
Clifford Wolf [Tue, 6 Mar 2018 10:50:38 +0000 (11:50 +0100)]
Add get_fsm_accept_reject for parsing SVA properties

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoSimplified SVA "until" handling
Clifford Wolf [Tue, 6 Mar 2018 00:51:42 +0000 (01:51 +0100)]
Simplified SVA "until" handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoImporove yosys-smtbmc error handling, Improve VCD output
Clifford Wolf [Mon, 5 Mar 2018 11:08:41 +0000 (12:08 +0100)]
Imporove yosys-smtbmc error handling, Improve VCD output

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix connwrappers help message
Clifford Wolf [Sun, 4 Mar 2018 21:54:34 +0000 (22:54 +0100)]
Fix connwrappers help message

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoImprove handling of warning messages
Clifford Wolf [Sun, 4 Mar 2018 21:35:59 +0000 (22:35 +0100)]
Improve handling of warning messages

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoUpdate copyright header
Clifford Wolf [Sun, 4 Mar 2018 20:31:10 +0000 (21:31 +0100)]
Update copyright header

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoImprove SMT2 encoding of $reduce_{and,or,bool}
Clifford Wolf [Sun, 4 Mar 2018 20:22:20 +0000 (21:22 +0100)]
Improve SMT2 encoding of $reduce_{and,or,bool}

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix a hangup in yosys-smtbmc error handling
Clifford Wolf [Sun, 4 Mar 2018 20:13:30 +0000 (21:13 +0100)]
Fix a hangup in yosys-smtbmc error handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd proper SVA seq.triggered support
Clifford Wolf [Sun, 4 Mar 2018 18:29:26 +0000 (19:29 +0100)]
Add proper SVA seq.triggered support

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd "synth -noshare"
Clifford Wolf [Sun, 4 Mar 2018 16:13:45 +0000 (17:13 +0100)]
Add "synth -noshare"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd Verific SVA support for "seq and seq" expressions
Clifford Wolf [Sun, 4 Mar 2018 14:08:21 +0000 (15:08 +0100)]
Add Verific SVA support for "seq and seq" expressions

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoRefactor Verific SVA importer property parser
Clifford Wolf [Sun, 4 Mar 2018 13:29:48 +0000 (14:29 +0100)]
Refactor Verific SVA importer property parser

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd VerificClocking class and refactor Verific DFF handling
Clifford Wolf [Sun, 4 Mar 2018 12:48:53 +0000 (13:48 +0100)]
Add VerificClocking class and refactor Verific DFF handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoImproved error handling in yosys-smtbmc
Clifford Wolf [Sat, 3 Mar 2018 19:00:07 +0000 (20:00 +0100)]
Improved error handling in yosys-smtbmc

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd SVA support for sequence OR
Clifford Wolf [Sat, 3 Mar 2018 15:34:28 +0000 (16:34 +0100)]
Add SVA support for sequence OR

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoTerminate running SMT solver when smtbmc is terminated
Clifford Wolf [Sat, 3 Mar 2018 13:50:40 +0000 (14:50 +0100)]
Terminate running SMT solver when smtbmc is terminated

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix smtbmc smtc/aiw parser for wire names containing []
Clifford Wolf [Sat, 3 Mar 2018 13:15:49 +0000 (14:15 +0100)]
Fix smtbmc smtc/aiw parser for wire names containing []

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