aboutsummaryrefslogtreecommitdiffstats
path: root/frontends/verific
Commit message (Collapse)AuthorAgeFilesLines
* Skip verific primitives and operators import by defaultMiodrag Milanovic2022-10-141-0/+1
|
* Add option to import all cells from all librariesMiodrag Milanovic2022-10-141-1/+30
|
* Fix handling of verific -L options, add implicit "-L work"Claire Xenia Wolf2022-10-101-0/+14
| | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* Add support for EDIF file reading using VerificMiodrag Milanovic2022-10-041-1/+47
|
* support file content redirection for verific frontenedMiodrag Milanovic2022-09-281-14/+60
|
* Add comment for future selfMiodrag Milanovic2022-09-281-0/+7
|
* Handle attributes imported from verificMiodrag Milanovic2022-09-281-5/+24
|
* Import memory attributesMiodrag Milanovic2022-09-211-0/+1
|
* verific: better fix for read callbackMiodrag Milanovic2022-09-071-5/+3
|
* verific: fix crash when using prep right after readMiodrag Milanovic2022-09-071-0/+3
|
* Encode filename unprintable charsMiodrag Milanovic2022-08-081-1/+1
|
* verific - make filepath handling compatible with verilog frontendMiodrag Milanovic2022-08-081-15/+29
|
* Setting wire upto in verific importMiodrag Milanovic2022-07-291-2/+5
|
* Update READMEMiodrag Milanović2022-07-281-1/+1
|
* Upadte documentation and changelogMiodrag Milanovic2022-07-041-0/+1
|
* Update to new verific extensions intefaceMiodrag Milanovic2022-06-301-3/+29
|
* Revert "use new verific extensions library"Miodrag Milanovic2022-06-211-70/+54
| | | | This reverts commit 607e957657fc56625de5c28ea9cd43c859017d96.
* use new verific extensions libraryMiodrag Milanovic2022-06-171-54/+70
|
* removed deprecated features codeMiodrag Milanovic2022-06-131-235/+0
|
* verific: Added "-vlog-libext" option to specify search extension for librariesMiodrag Milanovic2022-06-091-1/+16
|
* verific: proper file location for readmem commandsMiodrag Milanovic2022-06-041-0/+33
|
* fix text to fit 80 columnsMiodrag Milanovic2022-05-231-6/+9
|
* Update verific command file documentationMiodrag Milanovic2022-05-231-17/+19
|
* Use analysis mode if set in fileMiodrag Milanovic2022-05-231-2/+2
|
* verific: Use new value change logic also for $stable of wide signals.Jannis Harder2022-05-111-7/+29
| | | | I missed this in the previous PR.
* Merge pull request #3305 from jix/sva_value_change_logicJannis Harder2022-05-091-10/+25
|\ | | | | verific: Improve logic generated for SVA value change expressions
| * verific: Improve logic generated for SVA value change expressionsJannis Harder2022-05-091-10/+25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The previously generated logic assumed an unconstrained past value in the initial state and did not handle 'x values. While the current formal verification flow uses 2-valued logic, SVA value change expressions require a past value of 'x during the initial state to behave in the expected way (i.e. to consider both an initial 0 and an initial 1 as $changed and an initial 1 as $rose and an initial 0 as $fell). This patch now generates logic that at the same time a) provides the expected behavior in a 2-valued logic setting, not depending on any dont-care optimizations, and b) properly handles 'x values in yosys simulation
* | verific: Fix conditions of SVAs with explicit clocks within proceduresJannis Harder2022-05-033-5/+16
|/ | | | | | | | | For SVAs that have an explicit clock and are contained in a procedure which conditionally executes the assertion, verific expresses this using a mux with one input connected to constant 1 and the other output connected to an SVA_AT. The existing code only handled the case where the first input is connected to 1. This patch also handles the other case.
* Ignore merging past ffs that we are not properly mergingMiodrag Milanovic2022-04-291-0/+1
|
* verific: allow memories to be inferred in loops (vhdl)Miodrag Milanovic2022-04-181-0/+1
|
* verific: allow memories to be inferred in loopsN. Engelhardt2022-04-151-0/+1
|
* Preserve internal wires for external netsMiodrag Milanovic2022-04-011-1/+1
|
* Fix valgrind tests when using verificMiodrag Milanovic2022-03-301-0/+8
|
* Properly mark modules importedMiodrag Milanovic2022-03-261-2/+2
|
* Import verific netlist in consistent orderMiodrag Milanovic2022-03-252-23/+27
|
* Remove quotes if any from attributeMiodrag Milanovic2022-02-161-1/+4
|
* Add ability to override verilog mode for verific -f commandMiodrag Milanovic2022-02-091-2/+44
|
* Use bmux for NTO1MUXMiodrag Milanovic2022-02-021-16/+2
|
* Add YOSYS to the implicitly defined verilog macros in verificClaire Xenia Wolf2021-12-131-1/+2
| | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* Merge pull request #3102 from YosysHQ/claire/enumxzMiodrag Milanović2021-12-101-1/+1
|\ | | | | Fix verific import of enum values with x and/or z
| * Fix verific import of enum values with x and/or zClaire Xenia Wolf2021-12-101-1/+1
| | | | | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* | Update verific.ccClaire Xen2021-12-101-4/+7
| | | | | | Ad-hoc fixes/improvements
* | If direction NONE use that from first bitMiodrag Milanovic2021-12-081-0/+7
|/
* Make sure cell names are unique for wide operatorsMiodrag Milanovic2021-12-031-2/+2
|
* No need to alocate more memory than usedMiodrag Milanovic2021-11-101-1/+0
|
* Add "verific -cfg" commandClaire Xenia Wolf2021-11-011-2/+75
| | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* Fix verific gclk handling for async-load FFsClaire Xenia Wolf2021-10-311-12/+67
| | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* Enable async load dff emit by default in VerificMiodrag Milanovic2021-10-271-1/+1
|
* Revert "Compile option for enabling async load verific support"Miodrag Milanovic2021-10-271-4/+1
| | | | This reverts commit b8624ad2aef941776f5b4a08f66f8d43e70f8467.
* Compile option for enabling async load verific supportMiodrag Milanovic2021-10-251-1/+4
|
generated by cgit v1.2.3 (git 2.25.1) at 2025-07-28 03:26:52 +0000