aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Add support for SVA sequence concatenation ranges via verificClifford Wolf2018-02-183-16/+144
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for SVA until statements via VerificClifford Wolf2018-02-183-34/+138
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Move Verific SVA importer to extra C++ source fileClifford Wolf2018-02-184-1279/+1370
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Merge Verific SVA preprocessor and SVA importerClifford Wolf2018-02-181-79/+44
|
* Merge branch 'master' of github.com:cliffordwolf/yosysClifford Wolf2018-02-161-0/+6
|\
| * Improve handling of "bus" pins in liberty front-end (some files use ↵Clifford Wolf2018-02-151-0/+6
| | | | | | | | | | | | bus.pin.direction) Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Fix verific PRIM_SVA_AT handling in properties with PRIM_SVA_DISABLE_IFFClifford Wolf2018-02-152-1/+35
|/
* Fixed yosys-config for binary distributions with VerificClifford Wolf2018-02-131-3/+11
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Recognize stand-alone obj pattern even when it contains a slashClifford Wolf2018-02-131-0/+3
|
* Fix handling of zero-length cell connections in SMT2 back-endClifford Wolf2018-02-081-0/+8
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Merge branch 'master' of github.com:cliffordwolf/yosysClifford Wolf2018-02-031-0/+2
|\
| * Merge pull request #488 from azonenberg/for_cliffordClifford Wolf2018-02-031-0/+2
| |\ | | | | | | coolrunner2: Move LOC attributes onto the IO cells
| | * coolrunner2: Move LOC attributes onto the IO cellsRobert Ou2018-01-171-0/+2
| | |
* | | Do not create deep backtraces unless in ENABLE_DEBUG modeClifford Wolf2018-02-032-2/+6
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | | Fixed gcc 7.2 "statement will never be executed" warningClifford Wolf2018-02-031-1/+1
|/ /
* | Fix single-bit $stable handling in verific front-endClifford Wolf2018-02-011-0/+22
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Add Verific attribute handling for assert/assume/cover/live/fair cellsClifford Wolf2018-01-311-10/+16
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Fix smtio.py for large SMT2 S-expressionsClifford Wolf2018-01-291-1/+12
| |
* | Fix permissions on verific vdb filesClifford Wolf2018-01-281-0/+1
| |
* | Fixed handling of synchronous and asynchronous assertion/assumption/cover in ↵Clifford Wolf2018-01-231-27/+29
| | | | | | | | | | | | verific bindings Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Use "strip -S" instead of "strip -d" for Mac OS X compatibilityClifford Wolf2018-01-191-2/+2
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Improve log messages in equiv_makeClifford Wolf2018-01-191-2/+2
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 outputClifford Wolf2018-01-181-3/+3
|/
* Strip debug symbols from binaries on installClifford Wolf2018-01-171-1/+12
|
* Add "dffinit -highlow" and fix synth_intelClifford Wolf2018-01-092-1/+21
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for "yosys -E"Clifford Wolf2018-01-0713-4/+53
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Bugfix in hierarchy blackbox module port width handlingClifford Wolf2018-01-071-1/+2
|
* Update ABC to hg rev 6e3c24b3308aClifford Wolf2018-01-071-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Merge pull request #479 from Fatsie/latch_without_dataClifford Wolf2018-01-051-4/+23
|\ | | | | Some standard cell libraries include a latch with only set/reset.
| * Some standard cell libraries include a latch with only set/reset.Staf Verhaegen2018-01-031-4/+23
| |
* | Bugfix in hierarchy handling of blackbox module portsClifford Wolf2018-01-055-9/+10
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Merge pull request #480 from Fatsie/liberty_value_expressionClifford Wolf2018-01-041-2/+22
|\ \ | | | | | | Value of properties can be expression.
| * | Value of properties can be expression.Staf Verhaegen2018-01-031-2/+22
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* / Temporarily derive blackbox modules in hierarchy to evaluate port widthsClifford Wolf2018-01-041-1/+14
|/ | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add "no driver for signal bit" error msg to btor back-endClifford Wolf2017-12-241-0/+2
|
* Bugfix in verilog_defaults argument parserClifford Wolf2017-12-241-1/+1
|
* Fix minor typo in "prep" help messageClifford Wolf2017-12-191-1/+1
|
* Simple fix BTOR memory encodingClifford Wolf2017-12-171-2/+2
|
* Improve BTOR memory encodingClifford Wolf2017-12-171-2/+16
|
* Merge branch 'btor-ng'Clifford Wolf2017-12-154-987/+959
|\
| * Add array support to btor back-endClifford Wolf2017-12-151-6/+169
| |
| * Add $anyconst/$anyseq support to btor back-endClifford Wolf2017-12-151-13/+51
| |
| * Merge branch 'master' into btor-ngClifford Wolf2017-12-144-8/+12
| |\ | |/ |/|
* | Add yosys-smtbmc VCD writer support for memories with async writesClifford Wolf2017-12-143-7/+11
| |
* | Fix a bug in clk2fflogic memory handlingClifford Wolf2017-12-141-1/+1
| |
| * Merge branch 'master' into btor-ngClifford Wolf2017-12-149-38/+178
| |\ | |/ |/|
* | Add clk2fflogic memory supportClifford Wolf2017-12-141-1/+77
| |
* | Add smt2 back-end support for async write memoriesClifford Wolf2017-12-141-14/+53
| |
* | Add RTLIL::Const::is_fully_ones()Clifford Wolf2017-12-142-0/+12
| |
* | Add SigSpec::is_fully_ones()Clifford Wolf2017-12-142-0/+16
| |
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-19 09:56:18 +0000