GNU bug report logs - #78215
[PATCH electronics-team] gnu: symbiyosys: Use abc-yosyshq.

Previous Next

To reply to this bug, email your comments to 78215 AT debbugs.gnu.org.
There is no need to reopen the bug first.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Cayetano Santos <csantosb <at> inventati.org>
To: guix-patches <at> gnu.org
Cc: Cayetano Santos <csantosb <at> inventati.org>
Subject: [PATCH electronics-team] gnu: symbiyosys: Use abc-yosyshq.
Date: Fri,  2 May 2025 16:52:04 +0200

* 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(-)

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

base-commit: 5d5c0dfcdaff9205b3fe8f7822f16ad55743df8a
--
2.49.0

Message #8 received at 78215 <at> debbugs.gnu.org (full text, mbox):

From: Andreas Enge <andreas <at> enge.fr>
To: Cayetano Santos <csantosb <at> inventati.org>
Cc: 78215 <at> debbugs.gnu.org
Subject: Re: [PATCH electronics-team] gnu: symbiyosys: Use abc-yosyshq.
Date: Fri, 2 May 2025 18:14:34 +0200

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

Message #11 received at 78215 <at> debbugs.gnu.org (full text, mbox):

From: Cayetano Santos <csantosb <at> inventati.org>
To: Andreas Enge <andreas <at> enge.fr>
Cc: 78215 <at> debbugs.gnu.org
Subject: Re: [PATCH electronics-team] gnu: symbiyosys: Use abc-yosyshq.
Date: Fri, 02 May 2025 20:07:11 +0200

[Message part 1 (text/plain, inline)]

>ven. 02 mai 2025 at 18:14, Andreas Enge <andreas <at> 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.

[signature.asc (application/pgp-signature, inline)]

Message #16 received at 78215-done <at> debbugs.gnu.org (full text, mbox):

From: Andreas Enge <andreas <at> enge.fr>
To: Cayetano Santos <csantosb <at> inventati.org>
Cc: 78215-done <at> debbugs.gnu.org, 78214-done <at> debbugs.gnu.org
Subject: Re: [PATCH electronics-team] gnu: symbiyosys: Use abc-yosyshq.
Date: Sat, 3 May 2025 18:08:17 +0200

Hello Cayetano,

Am Fri, May 02, 2025 at 08:07:11PM +0200 schrieb Cayetano Santos:
> 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.

maybe it would have been clear had I seen the first patch, but I just
picked a random one from the list of untreated issues :)

Both are pushed now, thanks!

Andreas

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.