diff mbox series

[bug#78215,electronics-team] gnu: symbiyosys: Use abc-yosyshq.

Message ID a66e8d2ae6c2b3134b48982e430a208486a7fab9.1746197524.git.csantosb@inventati.org
State New
Headers
Series [bug#78215,electronics-team] gnu: symbiyosys: Use abc-yosyshq. |

Commit Message

Cayetano Santos May 2, 2025, 2:52 p.m. UTC 
  * gnu/packages/electronics.scm (symbiyosis): Use abc-yosyshq.

Change-Id: I7cc78cbf8cff232996bdb243cbd2585b593b2c89
---

Symbiyosys, by YosysHQ, uses a fork of abc from Berkeley, that guix packages as abc-yosyshq. Using it fixes previous errors in some of the tests, and we can reactivate them.

[arguments] <#:phases> {disable-abc-tests}: Remove.
[inputs]: Replace abc by abc-yosyshq.

 gnu/packages/electronics.scm | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)


base-commit: 5d5c0dfcdaff9205b3fe8f7822f16ad55743df8a
--
2.49.0

Comments

Andreas Enge May 2, 2025, 4:14 p.m. UTC | #1 
Hello Cayetano,

I tried your patch and got a test failure:
SBY 16:08:55 [autotune_div_prove] engine_20 (abc pdr): starting... (0 configurations pending)
SBY 16:08:55 [autotune_div_prove] model 'aig': preparing now...
SBY 16:08:55 [autotune_div_prove] aig: starting process "cd autotune_div_prove/model; yosys -ql design_aiger.log design_aiger.ys"
SBY 16:08:56 [autotune_div_prove] aig: finished (returncode=0)
SBY 16:08:56 [autotune_div_prove] prepared model 'aig'
SBY 16:08:56 [autotune_div_prove] engine_20 (abc pdr): failed (returncode=4 status=UNKNOWN)
SBY 16:08:57 [autotune_div_prove] engine_17 (smtbmc --nopresat --nounroll z3): succeeded (status=PASS)
SBY 16:08:57 [autotune_div_prove] engine_17 (smtbmc --nopresat --nounroll z3): took 20 seconds
SBY 16:09:01 [autotune_div_prove] engine_18 (smtbmc --nounroll z3 -- --noincr): succeeded (status=PASS)
SBY 16:09:01 [autotune_div_prove] engine_18 (smtbmc --nounroll z3 -- --noincr): took 20 seconds
SBY 16:09:02 [autotune_div_prove] engine_19 (smtbmc --nopresat --nounroll z3 -- --noincr): succeeded (status=PASS)
SBY 16:09:02 [autotune_div_prove] engine_19 (smtbmc --nopresat --nounroll z3 -- --noincr): took 19 seconds
SBY 16:09:02 [autotune_div_prove] failed engines:
SBY 16:09:02 [autotune_div_prove]   engine_20: abc pdr (returncode=4 status=UNKNOWN)
...

Andreas
Cayetano Santos May 2, 2025, 6:07 p.m. UTC | #2 
>ven. 02 mai 2025 at 18:14, Andreas Enge <andreas@enge.fr> wrote:

> Hello Cayetano,
>
> I tried your patch and got a test failure:

You need to apply my previous patch before, #78214, to fix yosys (used
by symbiyosys)

Sorry, I though it was clear. I should have sent a single patch with the
two commits instead.

C.
diff mbox series

Patch

diff --git a/gnu/packages/electronics.scm b/gnu/packages/electronics.scm
index d63511ff22..4df7064243 100644
--- a/gnu/packages/electronics.scm
+++ b/gnu/packages/electronics.scm
@@ -724,19 +724,9 @@  (define-public symbiyosys
               (substitute* "sbysrc/sby.py"
                 (("/usr/bin/env python")
                  (search-input-file inputs "bin/python3")))))
-          ;; The tests related to abc (berkeley) binary used currently produce
-          ;; errors.  The abc-yosyshq fork would make the tests pass, but
-          ;; cannot be packaged due to the fork's non-free licensing (see the
-          ;; README, which specifies a non-commercial restriction).
-          (add-after 'patch-/usr/bin/env 'disable-abc-tests
-            (lambda _
-              (delete-file "tests/keepgoing/keepgoing_multi_step.sby")
-              (delete-file-recursively "docs/examples/demos")
-              (delete-file
-               "tests/regression/aim_vs_smt2_nonzero_start_offset.sby")))
           (add-after 'install 'python:wrap
             (assoc-ref python:%standard-phases 'wrap)))))
-    (inputs (list abc
+    (inputs (list abc-yosyshq
                   boolector
                   git-minimal/pinned
                   python