Jannis Harder
dc22d97362
Better checking of available solvers
...
Check for required auxiliary tools and always regenerate the make rules
when the set of available tools changes.
2022-05-30 15:02:26 +02:00
Jannis Harder
939e000036
Makefile: Rename run_tests to test, update help, use .PHONY
2022-05-30 15:02:26 +02:00
Jannis Harder
de00dc71db
Merge pull request #161 from programmerjake/add-div-mod-floor-tests
...
add test for yosys's $divfloor and $modfloor cells
2022-05-26 12:00:05 +02:00
a87d21a802
add depth 1
2022-05-25 03:35:21 -07:00
3f32deb8c9
add test for yosys's $divfloor and $modfloor cells
...
Depends on: https://github.com/YosysHQ/yosys/pull/3335
2022-05-24 17:51:48 -07:00
N. Engelhardt
ad2c33dd37
docs: add instructions for newer btorsim version required
2022-05-24 11:39:10 +02:00
Jannis Harder
d10e472edf
Merge pull request #159 from jix/fix-dpmem-example
...
examples: Fix use of SVA value change expressions
2022-05-11 11:23:57 +02:00
Jannis Harder
fedfae0e9c
examples: Fix use of SVA value change expressions
...
The $stable value change expression cannot be true for a non-x signal in
the initial state. This is now correctly handled by the verific import,
so the dpmem example needs to start assuming `$stable` only after
leaving the initial state.
2022-05-11 10:38:54 +02:00
KrystalDelusion
fc9ff3d733
Initial FIFO description
2022-05-10 12:08:49 +12:00
KrystalDelusion
21dfd35516
Adding new Getting started guide
2022-05-10 11:41:15 +12:00
KrystalDelusion
7ec35dc425
Adding (small) intro to installation guide
...
Also a cross reference link.
2022-05-10 11:41:01 +12:00
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
