Clifford Wolf
e97f10b142
Fix smtio.py for large SMT2 S-expressions
2018-01-29 12:34:28 +01:00
Clifford Wolf
675f53abbb
Fix permissions on verific vdb files
2018-01-28 18:52:01 +01:00
Clifford Wolf
1d8161b432
Fixed handling of synchronous and asynchronous assertion/assumption/cover in verific bindings
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-01-23 17:42:40 +01:00
Clifford Wolf
318be8651c
Use "strip -S" instead of "strip -d" for Mac OS X compatibility
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-01-19 23:56:23 +01:00
Clifford Wolf
9337e4999d
Improve log messages in equiv_make
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-01-19 16:20:40 +01:00
Clifford Wolf
54aeca0983
Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output
2018-01-18 14:25:22 +01:00
Robert Ou
2abcd98527
coolrunner2: Move LOC attributes onto the IO cells
2018-01-17 16:17:32 -08:00
Clifford Wolf
57e02b6629
Strip debug symbols from binaries on install
2018-01-17 14:14:10 +01:00
Clifford Wolf
9ac560f5d3
Add "dffinit -highlow" and fix synth_intel
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-01-09 18:42:19 +01:00
Clifford Wolf
a96c775a73
Add support for "yosys -E"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-01-07 16:36:13 +01:00
Clifford Wolf
446ccf1f05
Bugfix in hierarchy blackbox module port width handling
2018-01-07 16:35:22 +01:00
Clifford Wolf
b557989576
Update ABC to hg rev 6e3c24b3308a
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-01-07 13:47:59 +01:00
Clifford Wolf
26c4323d48
Merge pull request #479 from Fatsie/latch_without_data
...
Some standard cell libraries include a latch with only set/reset.
2018-01-05 23:00:28 +01:00
Clifford Wolf
c80315cea4
Bugfix in hierarchy handling of blackbox module ports
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-01-05 13:28:45 +01:00
Clifford Wolf
fefb652d56
Merge pull request #480 from Fatsie/liberty_value_expression
...
Value of properties can be expression.
2018-01-04 13:30:00 +01:00
Clifford Wolf
2d140a44eb
Temporarily derive blackbox modules in hierarchy to evaluate port widths
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-01-04 13:23:29 +01:00
Staf Verhaegen
92eb841f0a
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.
2018-01-03 21:37:17 +00:00
Staf Verhaegen
5126c6f22b
Some standard cell libraries include a latch with only set/reset.
2018-01-03 21:36:02 +00:00
Clifford Wolf
9804ebedbf
Add "no driver for signal bit" error msg to btor back-end
2017-12-24 17:30:36 +01:00
Clifford Wolf
34005348b6
Bugfix in verilog_defaults argument parser
2017-12-24 17:21:37 +01:00
Clifford Wolf
b66d50e62d
Fix minor typo in "prep" help message
2017-12-19 21:44:05 +01:00
Clifford Wolf
292984896b
Simple fix BTOR memory encoding
2017-12-17 18:57:54 +01:00
Clifford Wolf
bbdcc1f9d4
Improve BTOR memory encoding
2017-12-17 18:55:17 +01:00
Clifford Wolf
8e22e8118a
Merge branch 'btor-ng'
2017-12-15 02:21:56 +01:00
Clifford Wolf
30f23281ed
Add array support to btor back-end
2017-12-15 02:19:06 +01:00
Clifford Wolf
ad901671c5
Add $anyconst/$anyseq support to btor back-end
2017-12-15 00:40:24 +01:00
Clifford Wolf
162c29bd6b
Merge branch 'master' into btor-ng
2017-12-14 03:13:47 +01:00
Clifford Wolf
9419de3e37
Add yosys-smtbmc VCD writer support for memories with async writes
2017-12-14 03:06:00 +01:00
Clifford Wolf
6132e6e72a
Fix a bug in clk2fflogic memory handling
2017-12-14 03:05:55 +01:00
Clifford Wolf
a48ec49017
Merge branch 'master' into btor-ng
2017-12-14 02:17:01 +01:00
Clifford Wolf
590e6961cb
Add clk2fflogic memory support
2017-12-14 02:07:31 +01:00
Clifford Wolf
2625da6440
Add smt2 back-end support for async write memories
2017-12-14 02:07:10 +01:00
Clifford Wolf
76afff7ef6
Add RTLIL::Const::is_fully_ones()
2017-12-14 02:06:39 +01:00
Clifford Wolf
96ad688849
Add SigSpec::is_fully_ones()
2017-12-14 01:29:09 +01:00
Clifford Wolf
1dad2ff682
Merge pull request #469 from kkiningh/master
...
Use quote includes for yosys.h
2017-12-14 00:03:26 +01:00
Kevin Kiningham
7350f7692a
Use quote includes for yosys.h
2017-12-13 13:27:52 -08:00
Clifford Wolf
88182e46d7
Check for memories in clk2fflogic
2017-12-13 19:14:34 +01:00
Clifford Wolf
07bfe8ba40
Merge pull request #468 from grahamedgecombe/fix-sb-io-od
...
Fix SB_IO_OD module
2017-12-13 16:55:39 +01:00
Clifford Wolf
546de7fa4f
Add "write_btor -s" mode
2017-12-13 00:15:44 +01:00
Clifford Wolf
0881bbf2e7
Add state initval handling to btor back-end
2017-12-12 23:44:08 +01:00
Clifford Wolf
f697282246
Add btor back-end support for 'x' constants
2017-12-12 21:48:55 +01:00
Clifford Wolf
2b6307547f
Add SigSpec::is_fully_ones()
2017-12-12 21:48:31 +01:00
Clifford Wolf
ca2adc30c9
Add warnings for driver-driver conflicts between FFs (and other cells) and constants
2017-12-12 17:13:27 +01:00
Clifford Wolf
82d1fd77de
Add btor $shift/$shiftx support
2017-12-11 14:24:19 +01:00
Graham Edgecombe
f93e6637aa
Fix port names in SB_IO_OD
2017-12-10 15:33:38 +00:00
Graham Edgecombe
52ace35a73
Remove trailing comma from SB_IO_OD port list
...
This isn't compatible with Icarus Verilog.
2017-12-10 15:33:38 +00:00
Clifford Wolf
cc119b5232
Fix btor back-end shift handling
2017-12-10 08:40:11 +01:00
Clifford Wolf
133a0f4978
Add support for $pmux in btor back-end
2017-12-10 08:11:08 +01:00
Clifford Wolf
83cf736309
Add support for more cell types to btor back-end
2017-12-10 07:16:47 +01:00
Clifford Wolf
8069118e6e
Merge branch 'master' into btor-ng
2017-12-10 01:27:41 +01:00