yosys.git
6 years agoMangle names with square brackets in VCD files to work around issues in gtkwave
Clifford Wolf [Thu, 1 Mar 2018 13:15:27 +0000 (14:15 +0100)]
Mangle names with square brackets in VCD files to work around issues in gtkwave

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFixes and improvements in Verific SVA importer
Clifford Wolf [Thu, 1 Mar 2018 10:40:43 +0000 (11:40 +0100)]
Fixes and improvements in Verific SVA importer

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd $rose/$fell support to Verific bindings
Clifford Wolf [Thu, 1 Mar 2018 09:12:15 +0000 (10:12 +0100)]
Add $rose/$fell support to Verific bindings

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMerge branch 'verificsva-ng'
Clifford Wolf [Wed, 28 Feb 2018 14:32:53 +0000 (15:32 +0100)]
Merge branch 'verificsva-ng'

6 years agoAdd support for PRIM_SVA_UNTIL to new SVA importer
Clifford Wolf [Wed, 28 Feb 2018 14:32:17 +0000 (15:32 +0100)]
Add support for PRIM_SVA_UNTIL to new SVA importer

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd DFSM generator to verific SVA importer
Clifford Wolf [Wed, 28 Feb 2018 14:05:33 +0000 (15:05 +0100)]
Add DFSM generator to verific SVA importer

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoContinue refactoring of Verific SVA importer code
Clifford Wolf [Wed, 28 Feb 2018 10:45:04 +0000 (11:45 +0100)]
Continue refactoring of Verific SVA importer code

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMajor redesign of Verific SVA importer
Clifford Wolf [Tue, 27 Feb 2018 19:33:15 +0000 (20:33 +0100)]
Major redesign of Verific SVA importer

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd -lz for verific builds
Clifford Wolf [Tue, 27 Feb 2018 11:15:42 +0000 (12:15 +0100)]
Add -lz for verific builds

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd handling of verific OPER_REDUCE_NOR
Clifford Wolf [Mon, 26 Feb 2018 14:26:01 +0000 (15:26 +0100)]
Add handling of verific OPER_REDUCE_NOR

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd handling of verific OPER_SELECTOR and OPER_WIDE_SELECTOR
Clifford Wolf [Mon, 26 Feb 2018 14:20:27 +0000 (15:20 +0100)]
Add handling of verific OPER_SELECTOR and OPER_WIDE_SELECTOR

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd handling of verific OPER_NTO1MUX and OPER_WIDE_NTO1MUX
Clifford Wolf [Mon, 26 Feb 2018 14:02:03 +0000 (15:02 +0100)]
Add handling of verific OPER_NTO1MUX and OPER_WIDE_NTO1MUX

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd "SVA syntax cheat sheet" comment to verificsva.cc
Clifford Wolf [Mon, 26 Feb 2018 13:31:58 +0000 (14:31 +0100)]
Add "SVA syntax cheat sheet" comment to verificsva.cc

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd $dlatchsr support to clk2fflogic
Clifford Wolf [Mon, 26 Feb 2018 11:20:28 +0000 (12:20 +0100)]
Add $dlatchsr support to clk2fflogic

6 years agoSmall fixes and improvements in $allconst/$allseq handling
Clifford Wolf [Mon, 26 Feb 2018 10:58:44 +0000 (11:58 +0100)]
Small fixes and improvements in $allconst/$allseq handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix opt_rmdff handling of $dlatchsr
Clifford Wolf [Mon, 26 Feb 2018 10:46:05 +0000 (11:46 +0100)]
Fix opt_rmdff handling of $dlatchsr

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMerge branch 'forall'
Clifford Wolf [Fri, 23 Feb 2018 18:37:00 +0000 (19:37 +0100)]
Merge branch 'forall'

6 years agoAdd smtbmc support for exist-forall problems
Clifford Wolf [Fri, 23 Feb 2018 18:33:30 +0000 (19:33 +0100)]
Add smtbmc support for exist-forall problems

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd $allconst and $allseq cell types
Clifford Wolf [Fri, 23 Feb 2018 12:14:47 +0000 (13:14 +0100)]
Add $allconst and $allseq cell types

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd Verific SVA support for ranges in repetition operator
Clifford Wolf [Thu, 22 Feb 2018 11:37:30 +0000 (12:37 +0100)]
Add Verific SVA support for ranges in repetition operator

6 years agoAdd support for SVA throughout via Verific
Clifford Wolf [Wed, 21 Feb 2018 12:09:47 +0000 (13:09 +0100)]
Add support for SVA throughout via Verific

6 years agoAdd support for mockup clock signals in yosys-smtbmc vcd output
Clifford Wolf [Tue, 20 Feb 2018 16:45:22 +0000 (17:45 +0100)]
Add support for mockup clock signals in yosys-smtbmc vcd output

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMerge pull request #507 from cr1901/msys2
Clifford Wolf [Mon, 19 Feb 2018 18:32:11 +0000 (19:32 +0100)]
Merge pull request #507 from cr1901/msys2

Improve msys2 flags for building abc.

6 years agoImprove msys2 flags for building abc.
William D. Jones [Mon, 19 Feb 2018 17:43:44 +0000 (12:43 -0500)]
Improve msys2 flags for building abc.

6 years agoAdd support for SVA sequence concatenation ranges via verific
Clifford Wolf [Sun, 18 Feb 2018 15:35:06 +0000 (16:35 +0100)]
Add support for SVA sequence concatenation ranges via verific

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd support for SVA until statements via Verific
Clifford Wolf [Sun, 18 Feb 2018 13:57:52 +0000 (14:57 +0100)]
Add support for SVA until statements via Verific

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMove Verific SVA importer to extra C++ source file
Clifford Wolf [Sun, 18 Feb 2018 12:52:49 +0000 (13:52 +0100)]
Move Verific SVA importer to extra C++ source file

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMerge Verific SVA preprocessor and SVA importer
Clifford Wolf [Sun, 18 Feb 2018 12:28:08 +0000 (13:28 +0100)]
Merge Verific SVA preprocessor and SVA importer

6 years agoMerge branch 'master' of github.com:cliffordwolf/yosys
Clifford Wolf [Fri, 16 Feb 2018 13:22:11 +0000 (14:22 +0100)]
Merge branch 'master' of github.com:cliffordwolf/yosys

6 years agoImprove handling of "bus" pins in liberty front-end (some files use bus.pin.direction)
Clifford Wolf [Thu, 15 Feb 2018 16:36:08 +0000 (17:36 +0100)]
Improve handling of "bus" pins in liberty front-end (some files use bus.pin.direction)

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix verific PRIM_SVA_AT handling in properties with PRIM_SVA_DISABLE_IFF
Clifford Wolf [Thu, 15 Feb 2018 14:26:37 +0000 (15:26 +0100)]
Fix verific PRIM_SVA_AT handling in properties with PRIM_SVA_DISABLE_IFF

6 years agoFixed yosys-config for binary distributions with Verific
Clifford Wolf [Tue, 13 Feb 2018 14:22:50 +0000 (15:22 +0100)]
Fixed yosys-config for binary distributions with Verific

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoRecognize stand-alone obj pattern even when it contains a slash
Clifford Wolf [Tue, 13 Feb 2018 13:55:24 +0000 (14:55 +0100)]
Recognize stand-alone obj pattern even when it contains a slash

6 years agoFix handling of zero-length cell connections in SMT2 back-end
Clifford Wolf [Thu, 8 Feb 2018 18:12:12 +0000 (19:12 +0100)]
Fix handling of zero-length cell connections in SMT2 back-end

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMerge branch 'master' of github.com:cliffordwolf/yosys
Clifford Wolf [Sat, 3 Feb 2018 14:05:08 +0000 (15:05 +0100)]
Merge branch 'master' of github.com:cliffordwolf/yosys

6 years agoDo not create deep backtraces unless in ENABLE_DEBUG mode
Clifford Wolf [Sat, 3 Feb 2018 14:04:39 +0000 (15:04 +0100)]
Do not create deep backtraces unless in ENABLE_DEBUG mode

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMerge pull request #488 from azonenberg/for_clifford
Clifford Wolf [Sat, 3 Feb 2018 13:45:23 +0000 (14:45 +0100)]
Merge pull request #488 from azonenberg/for_clifford

coolrunner2: Move LOC attributes onto the IO cells

6 years agoFixed gcc 7.2 "statement will never be executed" warning
Clifford Wolf [Sat, 3 Feb 2018 13:31:47 +0000 (14:31 +0100)]
Fixed gcc 7.2 "statement will never be executed" warning

6 years agoFix single-bit $stable handling in verific front-end
Clifford Wolf [Thu, 1 Feb 2018 11:51:49 +0000 (12:51 +0100)]
Fix single-bit $stable handling in verific front-end

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd Verific attribute handling for assert/assume/cover/live/fair cells
Clifford Wolf [Wed, 31 Jan 2018 18:06:51 +0000 (19:06 +0100)]
Add Verific attribute handling for assert/assume/cover/live/fair cells

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoFix smtio.py for large SMT2 S-expressions
Clifford Wolf [Mon, 29 Jan 2018 11:34:28 +0000 (12:34 +0100)]
Fix smtio.py for large SMT2 S-expressions

6 years agoFix permissions on verific vdb files
Clifford Wolf [Sun, 28 Jan 2018 17:52:01 +0000 (18:52 +0100)]
Fix permissions on verific vdb files

6 years agoFixed handling of synchronous and asynchronous assertion/assumption/cover in verific...
Clifford Wolf [Tue, 23 Jan 2018 16:42:40 +0000 (17:42 +0100)]
Fixed handling of synchronous and asynchronous assertion/assumption/cover in verific bindings

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoUse "strip -S" instead of "strip -d" for Mac OS X compatibility
Clifford Wolf [Fri, 19 Jan 2018 22:56:23 +0000 (23:56 +0100)]
Use "strip -S" instead of "strip -d" for Mac OS X compatibility

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoImprove log messages in equiv_make
Clifford Wolf [Fri, 19 Jan 2018 15:20:40 +0000 (16:20 +0100)]
Improve log messages in equiv_make

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMove user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output
Clifford Wolf [Thu, 18 Jan 2018 13:25:22 +0000 (14:25 +0100)]
Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output

6 years agocoolrunner2: Move LOC attributes onto the IO cells
Robert Ou [Sun, 19 Nov 2017 09:15:54 +0000 (01:15 -0800)]
coolrunner2: Move LOC attributes onto the IO cells

6 years agoStrip debug symbols from binaries on install
Clifford Wolf [Wed, 17 Jan 2018 13:14:10 +0000 (14:14 +0100)]
Strip debug symbols from binaries on install

6 years agoAdd "dffinit -highlow" and fix synth_intel
Clifford Wolf [Tue, 9 Jan 2018 17:42:19 +0000 (18:42 +0100)]
Add "dffinit -highlow" and fix synth_intel

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoAdd support for "yosys -E"
Clifford Wolf [Sun, 7 Jan 2018 15:36:13 +0000 (16:36 +0100)]
Add support for "yosys -E"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoBugfix in hierarchy blackbox module port width handling
Clifford Wolf [Sun, 7 Jan 2018 15:35:22 +0000 (16:35 +0100)]
Bugfix in hierarchy blackbox module port width handling

6 years agoUpdate ABC to hg rev 6e3c24b3308a
Clifford Wolf [Sun, 7 Jan 2018 12:47:59 +0000 (13:47 +0100)]
Update ABC to hg rev 6e3c24b3308a

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMerge pull request #479 from Fatsie/latch_without_data
Clifford Wolf [Fri, 5 Jan 2018 22:00:28 +0000 (23:00 +0100)]
Merge pull request #479 from Fatsie/latch_without_data

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

6 years agoBugfix in hierarchy handling of blackbox module ports
Clifford Wolf [Fri, 5 Jan 2018 12:28:45 +0000 (13:28 +0100)]
Bugfix in hierarchy handling of blackbox module ports

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoMerge pull request #480 from Fatsie/liberty_value_expression
Clifford Wolf [Thu, 4 Jan 2018 12:30:00 +0000 (13:30 +0100)]
Merge pull request #480 from Fatsie/liberty_value_expression

Value of properties can be expression.

6 years agoTemporarily derive blackbox modules in hierarchy to evaluate port widths
Clifford Wolf [Thu, 4 Jan 2018 12:23:29 +0000 (13:23 +0100)]
Temporarily derive blackbox modules in hierarchy to evaluate port widths

Signed-off-by: Clifford Wolf <clifford@clifford.at>
6 years agoValue of properties can be expression.
Staf Verhaegen [Wed, 3 Jan 2018 20:36:22 +0000 (20:36 +0000)]
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.

6 years agoSome standard cell libraries include a latch with only set/reset.
Staf Verhaegen [Wed, 3 Jan 2018 20:29:55 +0000 (20:29 +0000)]
Some standard cell libraries include a latch with only set/reset.

6 years agoAdd "no driver for signal bit" error msg to btor back-end
Clifford Wolf [Sun, 24 Dec 2017 16:29:54 +0000 (17:29 +0100)]
Add "no driver for signal bit" error msg to btor back-end

6 years agoBugfix in verilog_defaults argument parser
Clifford Wolf [Sun, 24 Dec 2017 16:21:37 +0000 (17:21 +0100)]
Bugfix in verilog_defaults argument parser

6 years agoFix minor typo in "prep" help message
Clifford Wolf [Tue, 19 Dec 2017 20:44:05 +0000 (21:44 +0100)]
Fix minor typo in "prep" help message

6 years agoSimple fix BTOR memory encoding
Clifford Wolf [Sun, 17 Dec 2017 17:57:54 +0000 (18:57 +0100)]
Simple fix BTOR memory encoding

6 years agoImprove BTOR memory encoding
Clifford Wolf [Sun, 17 Dec 2017 17:55:17 +0000 (18:55 +0100)]
Improve BTOR memory encoding

6 years agoMerge branch 'btor-ng'
Clifford Wolf [Fri, 15 Dec 2017 01:21:56 +0000 (02:21 +0100)]
Merge branch 'btor-ng'

6 years agoAdd array support to btor back-end
Clifford Wolf [Fri, 15 Dec 2017 01:19:06 +0000 (02:19 +0100)]
Add array support to btor back-end

6 years agoAdd $anyconst/$anyseq support to btor back-end
Clifford Wolf [Thu, 14 Dec 2017 23:40:24 +0000 (00:40 +0100)]
Add $anyconst/$anyseq support to btor back-end

6 years agoMerge branch 'master' into btor-ng
Clifford Wolf [Thu, 14 Dec 2017 02:13:47 +0000 (03:13 +0100)]
Merge branch 'master' into btor-ng

6 years agoAdd yosys-smtbmc VCD writer support for memories with async writes
Clifford Wolf [Thu, 14 Dec 2017 02:05:20 +0000 (03:05 +0100)]
Add yosys-smtbmc VCD writer support for memories with async writes

6 years agoFix a bug in clk2fflogic memory handling
Clifford Wolf [Thu, 14 Dec 2017 01:29:19 +0000 (02:29 +0100)]
Fix a bug in clk2fflogic memory handling

6 years agoMerge branch 'master' into btor-ng
Clifford Wolf [Thu, 14 Dec 2017 01:17:01 +0000 (02:17 +0100)]
Merge branch 'master' into btor-ng

6 years agoAdd clk2fflogic memory support
Clifford Wolf [Thu, 14 Dec 2017 01:07:31 +0000 (02:07 +0100)]
Add clk2fflogic memory support

6 years agoAdd smt2 back-end support for async write memories
Clifford Wolf [Thu, 14 Dec 2017 01:07:10 +0000 (02:07 +0100)]
Add smt2 back-end support for async write memories

6 years agoAdd RTLIL::Const::is_fully_ones()
Clifford Wolf [Thu, 14 Dec 2017 01:06:39 +0000 (02:06 +0100)]
Add RTLIL::Const::is_fully_ones()

6 years agoAdd SigSpec::is_fully_ones()
Clifford Wolf [Tue, 12 Dec 2017 20:48:31 +0000 (21:48 +0100)]
Add SigSpec::is_fully_ones()

6 years agoMerge pull request #469 from kkiningh/master
Clifford Wolf [Wed, 13 Dec 2017 23:03:26 +0000 (00:03 +0100)]
Merge pull request #469 from kkiningh/master

Use quote includes for yosys.h

6 years agoUse quote includes for yosys.h
Kevin Kiningham [Wed, 13 Dec 2017 21:27:52 +0000 (13:27 -0800)]
Use quote includes for yosys.h

6 years agoCheck for memories in clk2fflogic
Clifford Wolf [Wed, 13 Dec 2017 18:14:34 +0000 (19:14 +0100)]
Check for memories in clk2fflogic

6 years agoMerge pull request #468 from grahamedgecombe/fix-sb-io-od
Clifford Wolf [Wed, 13 Dec 2017 15:55:39 +0000 (16:55 +0100)]
Merge pull request #468 from grahamedgecombe/fix-sb-io-od

Fix SB_IO_OD module

6 years agoAdd "write_btor -s" mode
Clifford Wolf [Tue, 12 Dec 2017 23:15:44 +0000 (00:15 +0100)]
Add "write_btor -s" mode

6 years agoAdd state initval handling to btor back-end
Clifford Wolf [Tue, 12 Dec 2017 22:43:55 +0000 (23:43 +0100)]
Add state initval handling to btor back-end

6 years agoAdd btor back-end support for 'x' constants
Clifford Wolf [Tue, 12 Dec 2017 20:48:55 +0000 (21:48 +0100)]
Add btor back-end support for 'x' constants

6 years agoAdd SigSpec::is_fully_ones()
Clifford Wolf [Tue, 12 Dec 2017 20:48:31 +0000 (21:48 +0100)]
Add SigSpec::is_fully_ones()

6 years agoAdd warnings for driver-driver conflicts between FFs (and other cells) and constants
Clifford Wolf [Tue, 12 Dec 2017 16:13:27 +0000 (17:13 +0100)]
Add warnings for driver-driver conflicts between FFs (and other cells) and constants

6 years agoAdd btor $shift/$shiftx support
Clifford Wolf [Mon, 11 Dec 2017 13:24:19 +0000 (14:24 +0100)]
Add btor $shift/$shiftx support

6 years agoFix port names in SB_IO_OD
Graham Edgecombe [Sat, 9 Dec 2017 21:49:07 +0000 (21:49 +0000)]
Fix port names in SB_IO_OD

6 years agoRemove trailing comma from SB_IO_OD port list
Graham Edgecombe [Sat, 9 Dec 2017 21:39:20 +0000 (21:39 +0000)]
Remove trailing comma from SB_IO_OD port list

This isn't compatible with Icarus Verilog.

6 years agoFix btor back-end shift handling
Clifford Wolf [Sun, 10 Dec 2017 07:40:11 +0000 (08:40 +0100)]
Fix btor back-end shift handling

6 years agoAdd support for $pmux in btor back-end
Clifford Wolf [Sun, 10 Dec 2017 07:11:08 +0000 (08:11 +0100)]
Add support for $pmux in btor back-end

6 years agoAdd support for more cell types to btor back-end
Clifford Wolf [Sun, 10 Dec 2017 06:16:47 +0000 (07:16 +0100)]
Add support for more cell types to btor back-end

6 years agoMerge branch 'master' into btor-ng
Clifford Wolf [Sun, 10 Dec 2017 00:27:41 +0000 (01:27 +0100)]
Merge branch 'master' into btor-ng

6 years agoAdd support for Verific PRIM_SVA_NOT properties
Clifford Wolf [Sun, 10 Dec 2017 00:10:03 +0000 (01:10 +0100)]
Add support for Verific PRIM_SVA_NOT properties

6 years agoAdd Verific OPER_SVA_STABLE support
Clifford Wolf [Sat, 9 Dec 2017 23:59:44 +0000 (00:59 +0100)]
Add Verific OPER_SVA_STABLE support

6 years agoRefactoring Verific SVA rewriter
Clifford Wolf [Sat, 9 Dec 2017 23:26:26 +0000 (00:26 +0100)]
Refactoring Verific SVA rewriter

6 years agoFix btor concat
Clifford Wolf [Sat, 9 Dec 2017 04:58:14 +0000 (05:58 +0100)]
Fix btor concat

6 years agoMerge branch 'master' into btor-ng
Clifford Wolf [Sat, 9 Dec 2017 04:26:02 +0000 (05:26 +0100)]
Merge branch 'master' into btor-ng

6 years agoMerge pull request #467 from mithro/patch-1
Clifford Wolf [Sat, 9 Dec 2017 02:46:32 +0000 (03:46 +0100)]
Merge pull request #467 from mithro/patch-1

Fix spelling in -vpr help for synth_ice40

6 years agoFix spelling in -vpr help for synth_ice40
Tim Ansell [Sat, 9 Dec 2017 02:44:45 +0000 (18:44 -0800)]
Fix spelling in -vpr help for synth_ice40

6 years agoUse "hg ... --insecure" for cloning/pulling ABC
Clifford Wolf [Sun, 3 Dec 2017 05:11:11 +0000 (06:11 +0100)]
Use "hg ... --insecure" for cloning/pulling ABC

6 years agoUpdate ABC to hg rev 31fc97b0aeed
Clifford Wolf [Sat, 2 Dec 2017 20:24:12 +0000 (21:24 +0100)]
Update ABC to hg rev 31fc97b0aeed

6 years agoFix error handling for nested always/initial
Clifford Wolf [Sat, 2 Dec 2017 17:52:05 +0000 (18:52 +0100)]
Fix error handling for nested always/initial