aboutsummaryrefslogtreecommitdiffstats
path: root/tests
Commit message (Collapse)AuthorAgeFilesLines
* Fix tests for check in equiv_optJannis Harder2022-10-0713-15/+31
|
* Re-enable opt_dff_sr equiv_opt checksClaire Xenia Wolf2022-10-071-13/+12
| | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* Test fixes for latest iverilogMiodrag Milanovic2022-09-211-2/+12
|
* Add test for bug 3462Miodrag Milanovic2022-08-292-0/+15
|
* write_aiger: Fix non-$_FF_ FFsJannis Harder2022-08-181-0/+7
| | | | This broke while switching sby's formal flows to always use $_FF_'s.
* smtbmc: Add native json based witness format + smt2 backend supportJannis Harder2022-08-161-0/+8
| | | | | | | | | | | | | | | | | | | | This adds a native json based witness trace format. By having a common format that includes everything we support, and providing a conversion utility (yosys-witness) we no longer need to implement every format for every tool that deals with witness traces, avoiding a quadratic opportunity to introduce subtle bugs. Included: * smt2: New yosys-smt2-witness info lines containing full hierarchical paths without lossy escaping. * yosys-smtbmc --dump-yw trace.yw: Dump results in the new format. * yosys-smtbmc --yw trace.yw: Read new format as constraints. * yosys-witness: New tool to convert witness formats. Currently this can only display traces in a human-readable-only format and do a passthrough read/write of the new format. * ywio.py: Small python lib for reading and writing the new format. Used by yosys-smtbmc and yosys-witness to avoid duplication.
* Merge pull request #3277 from YosysHQ/lofty/rename-scramble_nameN. Engelhardt2022-08-111-0/+31
|\
| * rename: add -scramble-name option to randomly rename selectionsLofty2022-08-081-0/+31
| |
* | support file locations containing spacesMiodrag Milanovic2022-08-083-9/+10
|/
* gatemate: Add test for LUT tree mappinggatecat2022-06-273-0/+813
| | | | Signed-off-by: gatecat <gatecat@ds0.me>
* Adding expected error message.Archie2022-06-221-0/+1
|
* Adding testcase for issue 3374Archie2022-06-221-0/+3
|
* smt2: emit smtlib2_comb_expr outputs after all inputsJannis Harder2022-06-072-6/+6
|
* don't use sed -i because it won't work on macosJacob Lifshay2022-06-032-2/+3
|
* smtlib2_module: try to fix test on macosJacob Lifshay2022-06-021-1/+1
|
* smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressionsJacob Lifshay2022-06-024-0/+127
|
* verilog: fix width/sign detection for functionsZachary Snow2022-05-302-0/+46
|
* verilog: fix size and signedness of array querying functionsJannis Harder2022-05-301-0/+52
| | | | | | | | | | genrtlil.cc and simplify.cc had inconsistent and slightly broken handling of signedness for array querying functions. These functions are defined to return a signed result. Simplify always produced an unsigned and genrtlil always a signed 32-bit result ignoring the context. Includes tests for the the relvant edge cases for context dependent conversions.
* verilog: fix $past's signednessJannis Harder2022-05-251-0/+35
|
* verilog: fix signedness when removing unreachable casesJannis Harder2022-05-241-0/+33
|
* Add memory_bmux2rom pass.Marcelina Kościelnicka2022-05-181-0/+27
|
* Add memory_libmap tests.Marcelina Kościelnicka2022-05-1821-0/+1499
|
* efinix: Use `memory_libmap` pass.Marcelina Kościelnicka2022-05-181-12/+1
|
* ice40: Use `memory_libmap` pass.Marcelina Kościelnicka2022-05-181-56/+0
|
* xilinx: Use `memory_libmap` pass.Marcelina Kościelnicka2022-05-183-46/+15
|
* nexus: Use `memory_libmap` pass.Marcelina Kościelnicka2022-05-181-2/+2
|
* ecp5: Use `memory_libmap` pass.Marcelina Kościelnicka2022-05-181-135/+18
|
* proc_rom: Add special handling of const-0 address bits.Marcelina Kościelnicka2022-05-181-0/+146
|
* Merge pull request #3314 from jix/sva_value_change_logic_wideJannis Harder2022-05-162-2/+43
|\ | | | | verific: Use new value change logic also for $stable of wide signals.
| * verific: Use new value change logic also for $stable of wide signals.Jannis Harder2022-05-112-2/+43
| | | | | | | | I missed this in the previous PR.
* | Add proc_rom pass.Marcelina Kościelnicka2022-05-131-0/+43
|/
* Merge pull request #3305 from jix/sva_value_change_logicJannis Harder2022-05-097-1/+96
|\ | | | | verific: Improve logic generated for SVA value change expressions
| * verific: Improve logic generated for SVA value change expressionsJannis Harder2022-05-097-1/+96
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* | Merge pull request #3297 from jix/sva_nested_clk_elseJannis Harder2022-05-091-0/+11
|\ \ | |/ |/| verific: Fix conditions of SVAs with explicit clocks within procedures
| * verific: Fix conditions of SVAs with explicit clocks within proceduresJannis Harder2022-05-031-0/+11
| | | | | | | | | | | | | | | | | | 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.
* | Fix running sva testsMiodrag Milanovic2022-05-091-4/+3
| |
* | opt_mem: Remove constant-value bit lanes.Marcelina Kościelnicka2022-05-072-15/+2
|/
* sv: fix always_comb auto nosync for nested and function blocksZachary Snow2022-04-052-0/+30
|
* opt_merge: Add `-keepdc` option required for formal verificationJannis Harder2022-04-011-0/+50
| | | | | | | | The `-keepdc` option prevents merging flipflops with dont-care bits in their initial value, as, in general, this is not a valid transform for formal verification. The keepdc option of `opt` is passed along to `opt_merge` now.
* Fix valgrind tests when using verificMiodrag Milanovic2022-03-304-8/+8
|
* Proper example codeMiodrag Milanovic2022-03-142-1/+3
|
* intel_alm: M10K write-enable is negative-trueLofty2022-03-091-1/+2
|
* Merge pull request #3207 from nakengelhardt/json_escape_quotesMiodrag Milanović2022-03-042-0/+15
|\ | | | | fix handling of escaped chars in json backend and frontend (mostly)
| * fix handling of escaped chars in json backend and frontendN. Engelhardt2022-02-182-0/+15
| |
* | test dlatchsr and adlatchMiodrag Milanovic2022-02-164-4/+94
| |
* | Added test casesMiodrag Milanovic2022-02-1638-0/+896
|/
* verilog: support for time scale delay valuesZachary Snow2022-02-141-0/+25
|
* Fix access to whole sub-structs (#3086)Kamil Rakoczy2022-02-144-5/+51
| | | | | | * Add support for accessing whole struct * Update tests Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>
* verilog: fix dynamic dynamic range asgn elabZachary Snow2022-02-112-0/+108
|
* verilog: fix const func eval with upto variablesZachary Snow2022-02-112-0/+84
|
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-01 10:44:13 +0000