mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 22:14:08 +00:00
Code Activity
445 commits 7 branches 26 tags 1.3 MiB
Commit graph

135 commits

Author SHA1 Message Date
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 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
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
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
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 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
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 ff802086b4 test uninited FFs with const clks and fix btor script for this 2022-07-04 14:03:56 +02:00
Jannis Harder e3123283ea
Merge pull request #170 from programmerjake/add-simcheck-option 
switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules
 2022-07-03 11:47:22 +02:00
Jannis Harder b4458d43d7 Automatic engine selection 2022-06-27 15:58:42 +02:00
Jannis Harder 5014d74023 sby_design: Extract total memory size and forall usage 2022-06-24 13:50:26 +02:00
Jacob Lifshay db740839b7 switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules. 
Fixes: #168

Depends on: https://github.com/YosysHQ/yosys/pull/3391
 2022-06-22 21:17:29 -07:00
Jannis Harder 0fe8c223cf Decouple taskloop from task 2022-06-15 16:28:09 +02:00
Jannis Harder d1c04f79d6 Use monotonic clock for timeouts 2022-06-15 14:11:25 +02:00
Jannis Harder d0c59a3155 Don't use python asserts to handle unexpected solver output 2022-06-15 13:25:21 +02:00
Jannis Harder e99884e319 SbyProc: New error_callback instead of exit_callback for failing procs 2022-06-15 13:25:21 +02:00
Jannis Harder 6daa434d85 Add --dumptaskinfo option to output some .sby metadata as json 2022-04-11 17:44:10 +02:00
N. Engelhardt 8ce526c22d junit: use write_jny instead of write_json 2022-04-06 18:35:01 +02:00
N. Engelhardt 008d020c4d note unexpected return statuses in junit 2022-03-29 19:10:29 +02:00
Jannis Harder 079df4d95f Use -no-startoffset, avoiding index mismatch between aiger and smt2 2022-03-25 11:41:08 +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
N. Engelhardt d7e7f2c530 refactor model to have single base 2022-01-31 12:35:56 +01:00
N. Engelhardt 1cf27e7c31 parse solver location output for assert failures (cover not functional yet) 2022-01-27 13:41:07 +01:00
N. Engelhardt 7f3c4137c1 create json export and read in properties 2022-01-19 19:34:11 +01:00
N. Engelhardt 257a57d8ed create only a single bad when using pono solver; workaround for #137 2022-01-12 13:18:54 +01:00
N. Engelhardt 7c9e5b026b Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion. Config file tasks now correspond to SbyTasks. 2022-01-11 17:08:56 +01:00
Claire Xenia Wolf 5d19e4641a Add support for directories in [files] section 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2021-10-31 14:43:02 +01:00
Claire Xenia Wolf 1b3832cf92 Fixed names and links 2021-10-31 14:42:39 +01:00
piegames 2d7d48885b Turn .format() strings into f-strings 2021-06-26 19:46:30 +02:00
piegames 99aca04638 Print paths as absolute 
This generally makes debugging path issues easier.
 2021-06-21 22:31:53 +02:00
Miodrag Milanovic ecf7b8f1b0 Windows specific fixes 2021-03-22 16:48:33 +01:00