Commit Graph

413 Commits

Author SHA1 Message Date
Jannis Harder 7c409e2d5a
Merge pull request #5285 from jix/abstract_initstates
abstract: Add -initstates option
2025-08-18 15:39:09 +02:00
KrystalDelusion 6d55ca204b
Merge pull request #5281 from suisseWalter/add_parameterised_cells_stat
STAT: Add parameterised cells
2025-08-18 09:21:45 +12:00
clemens 9278bed853 removed copyright notice on lib file.
Should be covered by the yosys license not  anything else.
2025-08-16 09:40:03 +02:00
clemens 73d1177665 testcases
one testcase for single parameter cells.
one testcase for double parameter cells.
2025-08-16 09:40:03 +02:00
clemens d8fb4da437 updated testcase 2025-08-16 09:32:08 +02:00
Krystine Sherwin ec18d1aede
rename.cc: Fixup ports after -unescape 2025-08-15 10:48:32 +12:00
clemens 71307b4a51 add Testcases
Fix existing testcases
Fix edgecase where modules where counted as cells.
2025-08-13 14:46:01 +02:00
Jannis Harder 77089a8d03 rename: add -move-to-cell option in -wire mode 2025-08-13 11:11:52 +02:00
Jannis Harder 1f876f3a22 abstract: Add -initstates option 2025-08-12 15:37:12 +02:00
KrystalDelusion 1ae82d7b9d
Merge pull request #5233 from YosysHQ/krys/equiv_assume
Assumptions for equiv_*
2025-08-09 10:39:04 +12:00
Krystine Sherwin f9e8127e2b
tests: Add equiv_induct to equiv_assume.ys 2025-08-06 15:13:04 +12:00
Robert O'Callahan 8b75c06141 Add a general tests/.gitignore and remove redundant entries in subdirectory .gitignore files. 2025-07-22 10:38:38 +00:00
N. Engelhardt d009bcc9b6
Merge pull request #5198 from YosysHQ/nak/lcov 2025-07-17 11:57:58 +02:00
N. Engelhardt fb6974dcd7 print summary of line coverage to log 2025-07-16 13:40:07 +02:00
Krystine Sherwin 5ec189a2f5
Tests: Extra equiv_assume tests 2025-07-16 21:06:04 +12:00
Krystine Sherwin d30f934d0d
equiv_simple: Add -set-assumes option
Based on existing code for input cone and the `sat` handling of `-set-assumes`.
Update `equiv_assume.ys` to use `-set-assumes` option.
2025-07-16 21:04:41 +12:00
Krystine Sherwin a57c593c41
tests: Add equiv_assume.ys 2025-07-16 15:32:47 +12:00
N. Engelhardt 02323295b0
Merge pull request #5179 from YosysHQ/krys/assert2cover 2025-07-10 14:53:22 +02:00
N. Engelhardt 8a4f465143 update test to use suggested selection for assertions 2025-07-01 11:46:27 +02:00
N. Engelhardt ef3f541501 add linecoverage command to generate lcov report from selection 2025-06-26 13:21:53 +02:00
Emil J. Tywoniak 2b659626a3 rename: add -unescape 2025-06-24 12:33:33 +02:00
Krystine Sherwin 45131f4425
chformal: Add -assert2cover option
Also add to chformal tests.
2025-06-14 10:54:23 +12:00
Emil J. Tywoniak 239c265093 splitnets: handle single-bit vectors consistently 2025-06-05 10:58:06 +02:00
Krystine Sherwin 7c89355b70
cutpoint: Re-add whole module optimization
Also add a test script for it.
2025-05-06 09:57:34 +12:00
N. Engelhardt 84c49e1f33
Merge pull request #5041 from jix/declockgate-v2 2025-04-28 13:31:11 +00:00
Emil J 6a2f2f1818
Merge pull request #5031 from suisseWalter/fix_sequential_area
stat: fix sequential area not being included in addition/multiplication
2025-04-21 11:02:40 +02:00
cwalter 41375a5f05 create testcase to check correct addition of areas. 2025-04-20 16:44:22 +02:00
clemens 01d80c7403 add testcase 2025-04-19 20:41:10 +02:00
Jannis Harder 31d6d0ac17 formalff: Fix -declockgate test and missing emit for memories 2025-04-18 18:57:59 +02:00
Jannis Harder bd154a7188 formalff: Add -declockgate option 2025-04-18 17:44:34 +02:00
Krystine Sherwin 87d3b09988
cutpoint.cc: Fold -instances into -blackbox
Replace `cutpoint -blackbox` behaviour with `cutpoint -blackbox -instances` behaviour.
Drop `-instances` flag.
Add `-noscopeinfo` flag.
Use `RTLIL::Selection::boxed_module()` helper to shortcut blackbox check.
Update `cutpoint_blackbox.ys` tests to match.
2025-04-11 04:12:35 +12:00
Krystine Sherwin 779a1fddf6
Testing cutpoint with boxed selections 2025-04-11 04:12:34 +12:00
Krystine Sherwin cf44a9124f
cutpoint: Test -blackbox with parameter
Modify `cutpoint_blackbox.ys` to check that parameters on blackbox modules are maintained after the cutpoint.
Also adjusts the test to check that each instance gets the `$anyseq` cell.
2025-04-11 04:12:34 +12:00
Krystine Sherwin 583771ef5b
cutpoint: Add -blackbox option
Replace the contents of all blackboxes in the design with a formal cut point.
Includes test script.
2025-04-11 04:12:34 +12:00
Emil J 1b25e1cee0
Merge pull request #4942 from Anhijkt/fix-ice40dsp
ice40_dsp: fix log_assert issue
2025-03-28 13:32:17 +01:00
Emil J ec8b745929
Merge pull request #4733 from antmicro/fix-setundef-pass-for-params
Fix setting bits of parameters in setundef pass
2025-03-28 13:06:04 +01:00
Anhijkt cb03a1ec21 ice40_dsp: fix test 2025-03-26 15:13:05 +02:00
Emil J. Tywoniak 980a0a15c1 stat: allow gzipped liberty files 2025-03-19 13:43:44 +01:00
Anhijkt 5ae32efca5 ice40_dsp: add test 2025-03-15 20:05:57 +02:00
Anhijkt be3dfdc5ad splitcells: add tests 2025-03-10 19:41:22 +02:00
Emil J b4a169527d
Merge pull request #4894 from YosysHQ/emil/abstract
Add `abstract` pass for formal verification
2025-02-25 11:16:37 +01:00
Emil J. Tywoniak 3f60a2cc67 abstract: test -slice from:to for -init 2025-02-25 00:22:14 +01:00
Emil J. Tywoniak 3cb7054e53 abstract: test -slice for all modes, -rtlilslice for -init 2025-02-25 00:18:16 +01:00
Emil J. Tywoniak 5bd18613bb abstract: test -init 2025-02-19 23:03:43 +01:00
Emil J. Tywoniak 34e3fcbb31 abstract: test -value 2025-02-18 17:08:45 +01:00
Emil J. Tywoniak d3a90021ad abstract: test -state 2025-02-18 17:08:45 +01:00
Emil J. Tywoniak 387d0de383 abstract: -state allow partial abstraction, don't use buffer-normalized mode 2025-02-18 17:08:45 +01:00
Emil J. Tywoniak 6027030215 abstract: -value MVP, use buffer-normalized mode 2025-02-18 17:08:45 +01:00
Emil J. Tywoniak 4637fa74e3 abstract: -init MVP 2025-02-18 17:08:45 +01:00
Emil J. Tywoniak e4ca7b8846 abstract: -state MVP 2025-02-18 17:08:45 +01:00