mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-10-30 20:42:30 +00:00
Code Activity
677 commits 9 branches 33 tags 2.7 MiB
Commit graph

677 commits

This branch
This branch
All branches
Author SHA1 Message Date
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 (this is why regular testing is important).
 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
N. Engelhardt
3ff2c9affc avoid erroring out when coarse-grain logic loops can be resolved by mapping to fine grain operators 2022-07-25 16:22:32 +02:00
Jannis Harder
b4dd638311
Merge pull request #197 from YosysHQ/Autotune-grammar-check 
Autotune grammar/spelling check
 2022-07-25 09:53:39 +02:00
Jannis Harder
07d19b202b
Merge pull request #195 from jix/sbyproc-truncated-output 
Fix a race-condition SbyProc that could truncate output
 2022-07-13 17:30:36 +02:00
Jannis Harder
b8a1bdd40a
Merge pull request #193 from jix/abc_pdr_v 
abc pdr: Enable log output by default
 2022-07-13 16:07:04 +02:00
Jannis Harder
5d3f784beb Fix a race-condition SbyProc that could truncate output 
Present for a long time, but was not easy to hit. Some of my work in
progress changes made this much more likely and running the complete
test suite in parallel had a good chance of reproducing this for at
least one of the tests.
 2022-07-13 16:01:49 +02:00
KrystalDelusion
ca3429e328
Autotune grammar/spelling check 2022-07-11 21:21:31 +12:00
matt venn
4ab610ce87
Update autotune.rst 2022-07-11 11:10:45 +02:00
Jannis Harder
cea760bd52
Merge pull request #194 from jix/autotune_rst_fixes 
docs: Don't use linebreaks within inline code spans.
 2022-07-08 14:46:41 +02:00
Jannis Harder
bc2bb5c863 docs: Don't use linebreaks within inline code spans. 2022-07-08 14:31:57 +02:00
Jannis Harder
92e7eb2e32 abc pdr: Enable log output by default 
This makes it consistent with the other abc solvers and shows whether
abc pdr is making progress.
 2022-07-08 12:36:44 +02:00
Jannis Harder
de43a4c936
Merge pull request #191 from jix/early-readconfig 
Read config before creating a workdir
 2022-07-06 12:05:13 +02:00
Jannis Harder
f42ed5eb10
Merge pull request #192 from jix/win_retcode 
Make SbyProc hide Windows differences in retcode handling
 2022-07-06 12:05:03 +02:00
Jannis Harder
b3b315a473 Make SbyProc hide Windows differences in retcode handling 
Without this, we don't properly detect missing solver binaries and do
not properly handle the return status of the pono solver.
 2022-07-06 11:22:59 +02:00
Jannis Harder
566edad13c Read config before creating a workdir 
When using a task name not defined in the config, this now produces an
error before creating an unnecessary workdir for that non-existing task.
 2022-07-05 17:20:55 +02:00
Jannis Harder
ff1f87e169
Merge pull request #190 from jix/windows_fixes 
tests: Windows fixes
 2022-07-05 16:09:54 +02:00
Jannis Harder
ea7fc7dc2c tests: Windows fixes 
Make tests runnable on Windows, as long as a unix like environment as
e.g. provided by MSYS2 is available.
 2022-07-05 15:34:27 +02:00
Jannis Harder
ab98938faa
Merge pull request #187 from jix/const_clocks 
Test uninitialized FFs with constant clocks and fix btor script for this
 2022-07-04 17:47:16 +02:00
Jannis Harder
ff802086b4 test uninited FFs with const clks and fix btor script for this 2022-07-04 14:03:56 +02:00
Jannis Harder
9016031f32
Merge pull request #186 from jix/ff_xinit_opt 
tests: Test for invalid x-value FF init optimizations
 2022-07-04 14:03:06 +02:00
Jannis Harder
e01ac8b848 tests: Test for invalid x-value FF init optimizations 2022-07-04 13:33:39 +02:00
KrystalDelusion
cc27d27c05 More literalincludes 
Tidying up of newstart.rst and fifo.sv to include as much code as possible by reference.
Should reduce repetition and make it easier if changes occur in source.
 2022-07-04 11:53:40 +12:00