Clifford Wolf [Mon, 12 Mar 2018 12:52:35 +0000 (13:52 +0100)]
Add "setundef -undef"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Larry Doolittle [Sat, 10 Mar 2018 17:59:06 +0000 (09:59 -0800)]
Squelch trailing whitespace, including meta-whitespace
Larry Doolittle [Tue, 6 Mar 2018 17:43:42 +0000 (09:43 -0800)]
Harmonize uses of _WIN32 macro
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
Clifford Wolf [Wed, 7 Mar 2018 16:31:07 +0000 (17:31 +0100)]
Add Xilinx RAM64X1D and RAM128X1D simulation models
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
Clifford Wolf [Sun, 4 Mar 2018 20:31:10 +0000 (21:31 +0100)]
Update copyright header
Signed-off-by: Clifford Wolf <clifford@clifford.at>
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>
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>
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>
Clifford Wolf [Sun, 4 Mar 2018 16:13:45 +0000 (17:13 +0100)]
Add "synth -noshare"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
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>
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>
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>
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>
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>
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>
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>
Clifford Wolf [Fri, 2 Mar 2018 17:17:10 +0000 (18:17 +0100)]
Fix handling of SVA "until seq.triggered" properties
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Clifford Wolf [Fri, 2 Mar 2018 15:05:56 +0000 (16:05 +0100)]
Update SVA cheat sheet in verificsva.cc
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Clifford Wolf [Thu, 1 Mar 2018 18:37:36 +0000 (19:37 +0100)]
Fix in Verific SVA importer handling of until_with
Signed-off-by: Clifford Wolf <clifford@clifford.at>
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>
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>
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>
Clifford Wolf [Wed, 28 Feb 2018 14:32:53 +0000 (15:32 +0100)]
Merge branch 'verificsva-ng'
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>
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>
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>
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>
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>
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>
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>
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>
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>
Clifford Wolf [Mon, 26 Feb 2018 11:20:28 +0000 (12:20 +0100)]
Add $dlatchsr support to clk2fflogic
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>
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>
Clifford Wolf [Fri, 23 Feb 2018 18:37:00 +0000 (19:37 +0100)]
Merge branch 'forall'
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>
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>
Clifford Wolf [Thu, 22 Feb 2018 11:37:30 +0000 (12:37 +0100)]
Add Verific SVA support for ranges in repetition operator
Clifford Wolf [Wed, 21 Feb 2018 12:09:47 +0000 (13:09 +0100)]
Add support for SVA throughout via Verific
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>
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.
William D. Jones [Mon, 19 Feb 2018 17:43:44 +0000 (12:43 -0500)]
Improve msys2 flags for building abc.
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>
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>
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>
Clifford Wolf [Sun, 18 Feb 2018 12:28:08 +0000 (13:28 +0100)]
Merge Verific SVA preprocessor and SVA importer
Clifford Wolf [Fri, 16 Feb 2018 13:22:11 +0000 (14:22 +0100)]
Merge branch 'master' of github.com:cliffordwolf/yosys
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>
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
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>
Clifford Wolf [Tue, 13 Feb 2018 13:55:24 +0000 (14:55 +0100)]
Recognize stand-alone obj pattern even when it contains a slash
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>
Clifford Wolf [Sat, 3 Feb 2018 14:05:08 +0000 (15:05 +0100)]
Merge branch 'master' of github.com:cliffordwolf/yosys
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>
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
Clifford Wolf [Sat, 3 Feb 2018 13:31:47 +0000 (14:31 +0100)]
Fixed gcc 7.2 "statement will never be executed" warning
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>
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>
Clifford Wolf [Mon, 29 Jan 2018 11:34:28 +0000 (12:34 +0100)]
Fix smtio.py for large SMT2 S-expressions
Clifford Wolf [Sun, 28 Jan 2018 17:52:01 +0000 (18:52 +0100)]
Fix permissions on verific vdb files
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>
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>
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>
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
Robert Ou [Sun, 19 Nov 2017 09:15:54 +0000 (01:15 -0800)]
coolrunner2: Move LOC attributes onto the IO cells
Clifford Wolf [Wed, 17 Jan 2018 13:14:10 +0000 (14:14 +0100)]
Strip debug symbols from binaries on install
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>
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>
Clifford Wolf [Sun, 7 Jan 2018 15:35:22 +0000 (16:35 +0100)]
Bugfix in hierarchy blackbox module port width handling
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>
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.
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>
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.
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>
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.
Staf Verhaegen [Wed, 3 Jan 2018 20:29:55 +0000 (20:29 +0000)]
Some standard cell libraries include a latch with only set/reset.
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
Clifford Wolf [Sun, 24 Dec 2017 16:21:37 +0000 (17:21 +0100)]
Bugfix in verilog_defaults argument parser