aboutsummaryrefslogtreecommitdiffstats
path: root/tests
Commit message (Collapse)AuthorAgeFilesLines
* Replace GNU specific invocation of basename(1) with the equivalentLloyd Parkes2022-10-231-1/+1
| | | | POSIX one. The tests now complete on BSD as well as GNU/Linux.
* smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFsJannis Harder2022-10-121-7/+7
| | | | | | | The witness metadata was missing fine grained FFs completely and for coarse grained FFs where the output connection has multiple chunks it lacked the offset of the chunk within the SMT expression. This fixes both, the later by adding an "smtoffset" field to the metadata.
* Merge pull request #3502 from jix/equiv_opt_fixesJannis Harder2022-10-1125-82/+95
|\ | | | | equiv_opt and clk2fflogic fixes
| * Reenable existing equiv_opt testsJannis Harder2022-10-0713-54/+52
| |
| * 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>
* | Merge pull request #3452 from ALGCDG/masterMiodrag Milanović2022-10-101-0/+9
|\ \ | |/ |/| Add BLIF names command input plane size check
| * Adding check for BLIF names command input plane size.Archie2022-08-211-0/+9
| |
* | 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
| |
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 04:35:36 +0000