3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-06 14:24:08 +00:00
Commit graph

352 commits

Author SHA1 Message Date
KrystalDelusion ee15ebd0f1 Title case for license.rst 2022-05-10 11:40:17 +12:00
KrystalDelusion 7468e7655d Alignment fixing 2022-05-10 11:03:40 +12:00
KrystalDelusion 12b854b554 Headings for optional/required installs 2022-05-04 10:50:38 +12:00
KrystalDelusion 8f22733698 Revert change from yosyshq.net to yosyshq.com 2022-05-04 10:07:31 +12:00
KrystalDelusion 60de15293d Now actually fills up properly
As opposed to only storing MAX-1
2022-05-02 12:34:57 +12:00
KrystalDelusion 48d846d529 Adjusting for use with OSS
i.e. doesn't use concurrent assertions
2022-05-02 12:20:27 +12:00
KrystalDelusion f33c2eda52 Updating/rearranging links 2022-05-02 10:44:28 +12:00
KrystalDelusion e8c5ae678d Adding instructions for CAD
Currently taken verbatim from this repo's README.md
2022-05-02 10:31:51 +12:00
KrystalDelusion e106d5c161 Adjusting assumptions 2022-04-27 09:36:44 +12:00
KrystalDelusion ec02e25f5c Split fifo.sv into two files
fifo.sv contains the components, top.sv for toplevel design.
2022-04-27 09:24:14 +12:00
KrystalDelusion 679df4d898 Fixing .gitignore to ignore just directories 2022-04-27 09:05:16 +12:00
KrystalDelusion ee769996d0 Initial add of fifo example
Has tests which pass, committing before messing with it while tidying.
2022-04-27 09:02:16 +12:00
Jannis Harder 832888f0f0
Merge pull request #156 from jix/refactor-tests
Refactor tests
2022-04-25 11:21:21 +02:00
Jannis Harder 8da6f07cb3 Refactor tests
Organize tests into subdirectories and use a new makefile that scans
.sby files and allows selecting tests by mode, engine, solver and/or
subdirectory. Automatically skips tests that use engines/solvers that
are not found in the PATH.

See `cd tests; make help` for a description of supported make targets.
2022-04-11 17:50:38 +02:00
Jannis Harder 6daa434d85 Add --dumptaskinfo option to output some .sby metadata as json 2022-04-11 17:44:10 +02:00
Jannis Harder a190994098 Add envvar to enable automatic .gitignore creation for workdirs 2022-04-11 17:44:10 +02:00
Miodrag Milanović 1e1aea0b1e
Merge pull request #140 from nakengelhardt/junit_jny
junit: use write_jny instead of write_json
2022-04-08 15:26:48 +02:00
N. Engelhardt 8ce526c22d junit: use write_jny instead of write_json 2022-04-06 18:35:01 +02:00
Miodrag Milanović 4886ed7e19
Merge pull request #155 from jix/invalid_ff_dcinit_merge
Regression test: do not merge FFs with unconstrained initvals
2022-04-03 12:15:58 +02:00
Jannis Harder ef236eeddc Regression test: do not merge FFs with unconstrained initvals
Currently done by `opt -keepdc` via `opt_merge` but not valid in a
formal context.
2022-04-01 19:25:09 +02:00
Jannis Harder 25e982c238
Merge pull request #154 from jix/sby_design-fixes
sby_design fixes
2022-03-31 16:35:40 +02:00
Jannis Harder 4b512668b2 Fix design_hierarchy handling of $paramod cells 2022-03-31 15:51:58 +02:00
Jannis Harder a78eaa57db Fix variable name in find_property_by_cellname's error path 2022-03-31 13:12:15 +02:00
Jannis Harder 43a79965c3
Merge pull request #151 from jix/prefer-first-trace
Prefer the first tracefile for each failing assertion
2022-03-30 14:48:04 +02:00
Jannis Harder b725bfed0c Prefer the first tracefile for each failing assertion 2022-03-30 13:47:14 +02:00
N. Engelhardt 2e0087fd2f
Merge pull request #150 from nakengelhardt/fix_junit_type_assignment
note unexpected return statuses in junit
2022-03-30 12:53:48 +02:00
Jannis Harder 81e8b6737b
Merge pull request #147 from jix/smtbmc-keepgoing
Support and tests for smtbmc `--keep-going`
2022-03-30 11:42:48 +02:00
Jannis Harder 2d3d96478a Tests for --keep-going
This also changes the test Makefile to run `.check.py` files after
running the corresponding `.sby` file to allow more precise testing of
the keep going feature.
2022-03-30 11:26:58 +02:00
N. Engelhardt 008d020c4d note unexpected return statuses in junit 2022-03-29 19:10:29 +02:00
N. Engelhardt adacad7908
Merge pull request #148 from nakengelhardt/docs_updates
documentation updates
2022-03-28 16:34:00 +02:00
N. Engelhardt 53abf14514
Merge pull request #145 from nakengelhardt/fix_junit_tracefile
junit: handle multiple asserts failing with the same trace
2022-03-28 16:32:54 +02:00
N. Engelhardt 3d8f56b89a
Merge pull request #142 from nakengelhardt/fix_backslash_smt2
translate backslashes in cell names the same way as smt2 backend does
2022-03-28 16:32:10 +02:00
Miodrag Milanović 7a4a8e6bf6
Merge pull request #146 from jix/aim_vs_smt2_nonzero_start_offset
Test and fix signals with nonzero start offsets in aim files with smtbmc
2022-03-26 08:20:57 +01:00
N. Engelhardt 3834fe7622 document btor engine, add overview of mode/engine/solver combinations, remove unimplemented modes 2022-03-25 18:01:09 +01:00
Jannis Harder a434252ca1 Test signals with nonzero start offsets in aim files with smtbmc 2022-03-25 15:18:45 +01:00
Jannis Harder 079df4d95f Use -no-startoffset, avoiding index mismatch between aiger and smt2 2022-03-25 11:41:08 +01:00
Jannis Harder 7824460e27 Initial support for the new smtbmc --keep-going option
So far this only passes on the option and adjusts the trace_prefix to
support multiple numbered traces. Further changes are needed to
correctly associate individual traces with the assertions failing in
that trace.
2022-03-24 16:57:16 +01:00
N. Engelhardt c7e4785a8a junit: handle multiple asserts failing with the same trace 2022-03-22 16:16:02 +01:00
N. Engelhardt 5dc7fc9a4d translate backslashes in cell names the same way as smt2 backend does 2022-03-22 11:14:48 +01:00
Claire Xen fa5d5ad831
Merge pull request #120 from ythoma/patch-1
Update install.rst
2022-03-15 16:33:46 +01:00
N. Engelhardt b14270bedb
Merge pull request #139 from nakengelhardt/housekeeping
housekeeping
2022-03-15 16:06:52 +01:00
N. Engelhardt 2441940653 ci housekeeping 2022-03-15 15:12:59 +01:00
N. Engelhardt 419ef76f82
Merge pull request #133 from nakengelhardt/sby_junit
improve SBY JUnit report
2022-03-07 16:25:47 +01:00
N. Engelhardt 8a81b61321 fix ci 2022-03-07 08:34:01 +01:00
N. Engelhardt 7142f790e4 add testcase for overall run result 2022-02-24 22:44:11 +01:00
N. Engelhardt 89ed843ff1 validate junit files (with extra attributes added to schema) 2022-02-22 16:16:37 +01:00
N. Engelhardt 7ee357fcc8 fix induction 2022-02-07 22:01:52 +01:00
N. Engelhardt 7d3545dc86 fix junit error/failure/skipped count 2022-02-07 19:20:29 +01:00
N. Engelhardt 53eb25fcae handle unreached cover properties 2022-02-07 15:29:36 +01:00
N. Engelhardt 5abaccab69 refactor junit print into own function 2022-02-07 12:29:27 +01:00