Aki Van Ness
e8b8816143
docs: removed empty line
2022-08-18 05:36:11 -04:00
Aki Van Ness
a6c220dd5d
docs: Cut out the in-progress docs in preperation for a merge
2022-08-18 05:36:11 -04:00
Aki Van Ness
841e0cb797
sby: core: Added unsupported messages to the new sections
2022-08-18 05:36:11 -04:00
Aki Van Ness
637095a8ec
sby: fixed the sby task execution to accept the new engine internal layout
2022-08-18 05:36:11 -04:00
Aki Van Ness
da56a3c6d1
docs: started working on a rough draft of the docs for the new sections and changes to existing sections
2022-08-18 05:36:11 -04:00
Aki Van Ness
98fdcd7772
sby: core: fixed up the [setup] section
2022-08-18 05:36:11 -04:00
Aki Van Ness
6c959577f3
sby: core: cleaned up the [stage] section parsing
2022-08-18 05:36:11 -04:00
Aki Van Ness
ad4f506d2a
sby: core: fixed up the engines section parser
2022-08-18 05:36:10 -04:00
Aki Van Ness
2f841e5d55
sby: core: updated the parsing to match the changes in PR #206
2022-08-18 05:36:10 -04:00
Aki Van Ness
e4a7f624c1
sby: core: config: fixed the engines section parsing where it was not setting the engine mode when parsing the section
2022-08-18 05:36:10 -04:00
Aki Van Ness
987e439967
tests: parser: added the stages option to the options test file
2022-08-18 05:36:10 -04:00
Aki Van Ness
4abd8a7d69
tests: parser: updated the parser tests that caused a failure due to the lack of engines section
2022-08-18 05:36:10 -04:00
Aki Van Ness
204869bfed
sby: core: config: updated the error messages for the new setctions to make them more descriptive
2022-08-18 05:36:10 -04:00
Aki Van Ness
9293081308
modified the mode runners to accept the modified engine layout in preperation for the per-mode engine sections
2022-08-18 05:36:10 -04:00
Aki Van Ness
f1a645bb18
sby: core: config: Updated the [stage] section to use commas for the parents
2022-08-18 05:36:09 -04:00
Aki Van Ness
a0d366e58a
some cleanup, added some rough parser tests, and started altering the engines section
2022-08-18 05:36:09 -04:00
Aki Van Ness
0ab158eea1
sby: core: minor update to the stage parsing
2022-08-18 05:36:09 -04:00
Aki Van Ness
ed82c78acc
sby: core: Added preliminary support for [stage] sections
2022-08-18 05:36:08 -04:00
Aki Van Ness
4cccbf77fa
sby: core: Added preliminary support for the [setup] section
2022-08-18 05:36:08 -04:00
Jannis Harder
9a14f4d238
Merge pull request #210 from jix/witness_flow
...
Updated formal flow with new witness format
2022-08-17 16:57:11 +02:00
Jannis Harder
0aebf0b4d0
aig model: Call memory_map late to avoid performance issues
...
This requires running simplemap on the output as memory_map produces
coarse-grained cells even though we already have a fine-grained design.
2022-08-17 16:41:32 +02:00
KrystalDelusion
d6d7119cd5
Rewrite of non verific underfill/overfill
...
w_underfill should provide identical results regardless of whether
or not Verific is used. w_overfill doesn't have the extra check
for prettiness without Verific because I'm too lazy to do it.
Replaced $past function with past_nwen register to ensure correct
operation.
Expanded w_underfill under Verific to use a property block to more
easily compare the two versions side by side.
Changed Concurrent assertions section of doc to compare the two
implementations of w_underfill. Should provide a better example
for why using verific makes it easier.
2022-08-09 11:48:40 +12:00
KrystalDelusion
1d4716a5f9
Add noverific task to test the non verific code
...
Mostly for CI to ensure fallback code still functions as intended.a
Also reverted the change in the grep command to 1 line after.
2022-08-09 11:32:59 +12:00
KrystalDelusion
ad8730fa44
Fix typo
2022-08-08 21:30:31 +12:00
Jannis Harder
3412ea859b
New "none" engine to be used with the "make_model" option
2022-08-05 16:31:15 +02:00
Jannis Harder
231f0b80aa
Add make_model option to generate models not required by the task
...
Useful to do custom things (like counter example minimization) but still
use sby's flow to prepare models.
2022-08-05 16:31:15 +02:00
Jannis Harder
22585b33dc
Use 'rename -witness' instead of multiple 'rename -enumerate'
2022-08-05 16:31:15 +02:00
Jannis Harder
d3520037b9
Write native yosys witness traces
2022-08-05 16:31:15 +02:00
Jannis Harder
acaf6ef0c2
Use new memory_map -formal for aiger/_nomem
2022-08-05 16:31:15 +02:00
Jannis Harder
5265a52b65
Refactor flow to use a common prep model
...
The goal of this is to make sure that all backend flows are compatible
and we can map between them, so that e.g. the aiger model can be used to
minimize a counterexample trace produced by smtbmc. Reducing the parts
that differ per backend (including parts that receive different input
depending on the used backend) also makes testing more effective as the
common parts are easier to cover.
2022-08-05 16:31:15 +02:00
Jannis Harder
edb068bff4
Fix print_junit_results failure during some error conditions
...
There is a small window between setting self.precise_prop_status and
initializing self.design. I've only managed to produce an error within
that windows during development, but getting unrelated stacktraces from
print_junit_result failing distracts from debugging the issue at hand.
2022-08-05 16:31:15 +02:00
Aki Van Ness
46ca20f8ec
sby: core: ensured to strip the line of any uneeded whitespace
2022-08-04 06:13:28 -04:00
Aki Van Ness
9368f3f987
sby: core: explicitly split the the entries for the [options] section params to be at most one,
2022-08-04 06:13:28 -04:00
Aki Van Ness
10234fef00
sby: core: changed how the split for the section header and arguments are done, with a prior strip to remove and extra whitespace
2022-08-04 06:13:28 -04:00
Aki Van Ness
8133aaa8f8
sby: core: changed how the sections and their arguments are handled and cleared up the strangly worded error messages related to that
2022-08-04 06:13:28 -04:00
Jannis Harder
8d2fa9b304
Merge pull request #207 from jix/fix_smt_shift
...
Regression test for YosysHQ/yosys#3433
2022-08-03 17:04:10 +02:00
Jannis Harder
523b7a252e
Regression test for YosysHQ/yosys#3433
2022-08-03 16:08:19 +02:00
KrystalDelusion
cfa4352bae
Changes to reset
...
Active high.
Removed init.
Better over/underfill cover properties for verific. Moved basic cover statement to only be used when there is no verific.
Other general tidy up.
Also updated/fixed a couple minor things in newstart.rst.
2022-08-02 12:11:09 +12:00
KrystalDelusion
a76286ed34
Check output of fifo.sby
...
False positive exit 0 if fifo.sby was giving returncode=2.
2022-08-02 10:28:06 +12:00
KrystalDelusion
93d8ef9663
Fixed bigtest
...
Accidentally broke it in cc27d27
2022-08-02 10:12:33 +12:00
Aki Van Ness
59dc27ed73
sby: core: config: cleaned up the error messages to make them less opaque
2022-08-01 10:16:05 -04:00
Jannis Harder
c200690160
Merge pull request #201 from jix/autotune_example_in_docs
...
Autotune example in docs
2022-08-01 12:13:38 +02:00
KrystalDelusion
b2d0368e26
Testing fifo things in CI
...
Turns out the bigtest golden ref is failing a_count_diff, need to fix that before removing the default statement.
Base example code is fine. New shell script to run default case and then nofullskip.
Expects returncode=2 after running nofullskip.
2022-08-01 22:06:03 +12:00
KrystalDelusion
ed9b291d2b
Remove redundancies in certain logic checks
...
A | A' === True, A | (A' & B) === A | B
2022-08-01 20:36:19 +12:00
KrystalDelusion
672a559b92
Merge branch 'YosysHQ:master' into fifo_example
2022-08-01 20:25:15 +12:00
Jannis Harder
4ec278e6ec
Autotune example in docs
2022-07-26 16:35:57 +02:00
Jannis Harder
0395b8a439
Merge pull request #200 from jix/autotune_example
...
example for autotune
2022-07-26 16:21:16 +02:00
Jannis Harder
9293e66092
example for autotune
2022-07-26 16:06:02 +02:00
Jannis Harder
a498e1e9a1
Merge pull request #199 from nakengelhardt/add_cvc5_tool_rule
...
add cvc5 executable to required tool mapping
2022-07-25 17:27:43 +02:00
N. Engelhardt
1cf206fc1c
add cvc5 executable to required tool mapping
2022-07-25 17:01:17 +02:00
