GNU bug report logs - #78016
[PATCH electronics-team] gnu: Add symbiyosys.

Previous Next

To reply to this bug, email your comments to 78016 AT debbugs.gnu.org.

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: Add symbiyosys.
Date: Wed, 23 Apr 2025 17:34:51 +0200

* gnu/packages/electronics.scm (symbiyosys): New variable.

Change-Id: I1a3758e4bf46fc6d57ef63a0c0f5f2e39a862c4d
---
 gnu/packages/electronics.scm | 65 +++++++++++++++++++++++++++++++++++-
 1 file changed, 64 insertions(+), 1 deletion(-)

diff --git a/gnu/packages/electronics.scm b/gnu/packages/electronics.scm
index 12e44f234a..7d0dfc3095 100644
--- a/gnu/packages/electronics.scm
+++ b/gnu/packages/electronics.scm
@@ -46,6 +46,7 @@ (define-module (gnu packages electronics)
   #:use-module (gnu packages documentation)
   #:use-module (gnu packages embedded)
   #:use-module (gnu packages fontutils)
+  #:use-module (gnu packages fpga)
   #:use-module (gnu packages gl)
   #:use-module (gnu packages glib)
   #:use-module (gnu packages graphviz)
@@ -54,6 +55,7 @@ (define-module (gnu packages electronics)
   #:use-module (gnu packages libusb)
   #:use-module (gnu packages linux)
   #:use-module (gnu packages m4)
+  #:use-module (gnu packages maths)
   #:use-module (gnu packages pkg-config)
   #:use-module (gnu packages python)
   #:use-module (gnu packages python-build)
@@ -67,7 +69,8 @@ (define-module (gnu packages electronics)
   #:use-module (gnu packages swig)
   #:use-module (gnu packages tls)
   #:use-module (gnu packages toolkits)
-  #:use-module (gnu packages version-control))
+  #:use-module (gnu packages version-control)
+  #:use-module (gnu packages xml))
 
 (define-public comedilib
   (package
@@ -635,6 +638,66 @@ (define-public sigrok-firmware-fx2lafw
 them usable as simple logic analyzer and/or oscilloscope hardware.")
       (license license:gpl2+))))
 
+(define-public symbiyosys
+  (package
+    (name "symbiyosys")
+    (version "0.52")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://github.com/YosysHQ/sby/")
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32 "06nhkmnl9ymp1wxapc0lnj82knj5q43x0s2rmfshwvs4cijzqm7f"))))
+    (build-system gnu-build-system)
+    (arguments
+     (list
+      #:test-target "test"
+      #:make-flags #~(list (string-append "PREFIX=" #$output))
+      #:phases #~(modify-phases %standard-phases
+                   (delete 'configure)
+                   (delete 'build)
+                   ;; info: requires furo-ys, not yet available
+                   ;; (add-after 'install 'build-info
+                   ;; (lambda _
+                   ;; (invoke "make" "-C" "docs" "info")))
+                   (add-before 'check 'create-git
+                     (lambda _
+                       (invoke "git" "init"))) ;check expects a git repo
+                   (add-after 'create-git 'patch-/usr/bin/env
+                     (lambda _
+                       (substitute* "sbysrc/sby_core.py"
+                         (("\"/usr/bin/env\", ")
+                          ""))
+                       (substitute* "sbysrc/sby.py"
+                         (("/usr/bin/env python")
+                          (which "python3")))))
+                   ;; remove tests which fail
+                   (add-after 'patch-/usr/bin/env 'delete-check-failures
+                     (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"))))))
+    (inputs (list yosys abc))
+    (native-inputs (list
+                    ;; python-sphinx python-sphinx-argparse texinfo ; info
+                    python
+                    python-click
+                    python-xmlschema
+                    git-minimal/pinned
+                    boolector
+                    yices
+                    z3))
+    (home-page "https://github.com/YosysHQ/sby/")
+    (synopsis "Formal verification with yosys")
+    (description
+     "SimbyYosys is a front-end program for yosys-based formal hardware verification
+flows.")
+    (license license:isc)))
+
 (define-public uhdm
   (package
     (name "uhdm")

base-commit: 699ce22ed812cf8cfcdd8d0341829f8fac2c864a
-- 
2.49.0

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

From: Maxim Cournoyer <maxim.cournoyer <at> gmail.com>
To: Cayetano Santos <csantosb <at> inventati.org>
Cc: 78016 <at> debbugs.gnu.org, Ekaitz Zarraga <ekaitz <at> elenq.tech>
Subject: Re: [bug#78016] [PATCH electronics-team] gnu: Add symbiyosys.
Date: Fri, 25 Apr 2025 15:59:40 +0900

Hi,

Cayetano Santos <csantosb <at> inventati.org> writes:

> * gnu/packages/electronics.scm (symbiyosys): New variable.

Neat!

[...]

> +    (arguments
> +     (list
> +      #:test-target "test"
> +      #:make-flags #~(list (string-append "PREFIX=" #$output))
> +      #:phases #~(modify-phases %standard-phases
> +                   (delete 'configure)
> +                   (delete 'build)
> +                   ;; info: requires furo-ys, not yet available

I'd use: TODO: build docs, after furo-ys is packaged.

> +                   ;; (add-after 'install 'build-info
> +                   ;; (lambda _
> +                   ;; (invoke "make" "-C" "docs" "info")))
> +                   (add-before 'check 'create-git

nitpick: I'd name the phase to 'git-init or similar.

> +                     (lambda _
> +                       (invoke "git" "init"))) ;check expects a git repo
> +                   (add-after 'create-git 'patch-/usr/bin/env
> +                     (lambda _
> +                       (substitute* "sbysrc/sby_core.py"
> +                         (("\"/usr/bin/env\", ")
> +                          ""))
> +                       (substitute* "sbysrc/sby.py"
> +                         (("/usr/bin/env python")
> +                          (which "python3")))))

It looks like 'sby' is the test runner, so that should be OK, but just
to make sure: are these source used at runtime?  If so, `which` must not
be used to patch the source, as it picks things from the PATH at *build*
time, which in a cross-compilation setting would not point to the same
binaries.

For non-tests sources, the safe way is to find the file names or
commands via e.g. (search-input-file inputs "bin/python3") for example
(with the 'inputs' key exposed via the phase procedure).

> +                   ;; remove tests which fail

Please use complete sentences for standalone comments [0].  Also try to
explain the failures.  When they cannot be explained it's best to report
them to the upstream project and keep a reference to the opened issue so
that resolution can be tracked.

[0]  See (info "(standards) Comments") from the gnu-standards package.

> +                   (add-after 'patch-/usr/bin/env 'delete-check-failures

I'd name this phase 'disable-problematic-tests.  Note that if this uses
the Automake test harness (it seems it does not, using sby instead),
then setting the make variable (flag) XFAIL_TESTS with the
space-separated names of the failing tests could be a better way, see
(info "(automake) Parallel Test Harness").

> +                     (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"))))))
> +    (inputs (list yosys abc))

Please list in lexicographical order.

> +    (native-inputs (list
> +                    ;; python-sphinx python-sphinx-argparse texinfo ; info

Maybe add a standalone

;; TODO: see above build-info phase comment.

instead of the '; info' margin comment.

nitpick: no need for a space between ';' and the margin comment.

> +                    python
> +                    python-click
> +                    python-xmlschema
> +                    git-minimal/pinned
> +                    boolector
> +                    yices
> +                    z3))

Again, please sort :-)

> +    (home-page "https://github.com/YosysHQ/sby/")
> +    (synopsis "Formal verification with yosys")

I'd say 'Formal hardware verification with yosys'

Other than that it looks good to me!  Could you please send a v2?

-- 
Thanks,
Maxim

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

From: Cayetano Santos <csantosb <at> inventati.org>
To: 78016 <at> debbugs.gnu.org
Cc: Cayetano Santos <csantosb <at> inventati.org>,
 Cayetano Santos via Guix-patches via <guix-patches <at> gnu.org>
Subject: [PATCH v2] gnu: Add symbiyosys.
Date: Fri, 25 Apr 2025 11:30:33 +0200

From: Cayetano Santos via Guix-patches via <guix-patches <at> gnu.org>

* gnu/packages/electronics.scm (symbiyosys): New variable.

Change-Id: I1a3758e4bf46fc6d57ef63a0c0f5f2e39a862c4d
Signed-off-by: Cayetano Santos <csantosb <at> inventati.org>
---
 gnu/packages/electronics.scm | 67 +++++++++++++++++++++++++++++++++++-
 1 file changed, 66 insertions(+), 1 deletion(-)

diff --git a/gnu/packages/electronics.scm b/gnu/packages/electronics.scm
index 12e44f234a..5ca28607b5 100644
--- a/gnu/packages/electronics.scm
+++ b/gnu/packages/electronics.scm
@@ -46,6 +46,7 @@ (define-module (gnu packages electronics)
   #:use-module (gnu packages documentation)
   #:use-module (gnu packages embedded)
   #:use-module (gnu packages fontutils)
+  #:use-module (gnu packages fpga)
   #:use-module (gnu packages gl)
   #:use-module (gnu packages glib)
   #:use-module (gnu packages graphviz)
@@ -54,6 +55,7 @@ (define-module (gnu packages electronics)
   #:use-module (gnu packages libusb)
   #:use-module (gnu packages linux)
   #:use-module (gnu packages m4)
+  #:use-module (gnu packages maths)
   #:use-module (gnu packages pkg-config)
   #:use-module (gnu packages python)
   #:use-module (gnu packages python-build)
@@ -67,7 +69,8 @@ (define-module (gnu packages electronics)
   #:use-module (gnu packages swig)
   #:use-module (gnu packages tls)
   #:use-module (gnu packages toolkits)
-  #:use-module (gnu packages version-control))
+  #:use-module (gnu packages version-control)
+  #:use-module (gnu packages xml))
 
 (define-public comedilib
   (package
@@ -635,6 +638,68 @@ (define-public sigrok-firmware-fx2lafw
 them usable as simple logic analyzer and/or oscilloscope hardware.")
       (license license:gpl2+))))
 
+(define-public symbiyosys
+  (package
+    (name "symbiyosys")
+    (version "0.52")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://github.com/YosysHQ/sby/")
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32 "06nhkmnl9ymp1wxapc0lnj82knj5q43x0s2rmfshwvs4cijzqm7f"))))
+    (build-system gnu-build-system)
+    (arguments
+     (list
+      #:test-target "test"
+      #:make-flags #~(list (string-append "PREFIX=" #$output))
+      #:phases #~(modify-phases %standard-phases
+                   (delete 'configure)
+                   (delete 'build)
+                   ;; TODO: build docs, after furo-ys is packaged.
+                   ;; (add-after 'install 'build-info
+                   ;; (lambda _
+                   ;; (invoke "make" "-C" "docs" "info")))
+                   (add-before 'check 'git-init
+                     (lambda _
+                       (invoke "git" "init"))) ;check expects a git repo
+                   (add-after 'git-init 'patch-/usr/bin/env
+                     (lambda* (#:key inputs #:allow-other-keys)
+                       (substitute* "sbysrc/sby_core.py"
+                         (("\"/usr/bin/env\", ")
+                          ""))
+                       (substitute* "sbysrc/sby.py"
+                         (("/usr/bin/env python")
+                          (search-input-file inputs "bin/python3")))))
+                   ;; The tests related to abc binary used by yosys produce errors
+                   ;; Disable them
+                   (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"))))))
+    (inputs (list abc yosys))
+    (native-inputs (list
+                    ;; TODO: see above build-info phase comment.
+                    ;; python-sphinx python-sphinx-argparse texinfo
+                    boolector
+                    git-minimal/pinned
+                    python
+                    python-click
+                    python-xmlschema
+                    yices
+                    z3))
+    (home-page "https://github.com/YosysHQ/sby/")
+    (synopsis "Formal hardware verification with yosys")
+    (description
+     "SimbyYosys is a front-end program for yosys-based formal hardware verification
+flows.")
+    (license license:isc)))
+
 (define-public uhdm
   (package
     (name "uhdm")

base-commit: 501a9603f5e3cda07f3be8e7fecac31f7af5ce52
-- 
2.49.0

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

From: Cayetano Santos <csantosb <at> inventati.org>
To: Maxim Cournoyer <maxim.cournoyer <at> gmail.com>
Cc: 78016 <at> debbugs.gnu.org, Ekaitz Zarraga <ekaitz <at> elenq.tech>
Subject: Re: [bug#78016] [PATCH electronics-team] gnu: Add symbiyosys.
Date: Fri, 25 Apr 2025 11:37:55 +0200

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

>ven. 25 avril 2025 at 15:59, Maxim Cournoyer <maxim.cournoyer <at> gmail.com> wrote:

Thanks for the review, I have included all of your comments in v2.

>> +                   ;; remove tests which fail
>
> Please use complete sentences for standalone comments [0].  Also try to
> explain the failures.  When they cannot be explained it's best to report
> them to the upstream project and keep a reference to the opened issue so
> that resolution can be tracked.

The failures come from the fact that yosys uses a version of abc which
differs from the one we package, as a submodule of yosys itself.

Submitting issues upstream is kind of useless in this case: as you may
see from their ci actions pipelines, they’re using completely different
(precompiled) binaries (from their cad suite), even using verific
proprietary plugins. Guix departs from this logic.

Let’s keep things as they are, while I explore more in detail the effect of
using different abc versions in our packages.

C.

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

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

From: Cayetano Santos <csantosb <at> inventati.org>
To: guix-patches <at> gnu.org
Cc: maxim.cournoyer <at> gmail.com, 78016 <at> debbugs.gnu.org, ekaitz <at> elenq.tech,
 csantosb <at> inventati.org
Subject: Re: [bug#78016] [PATCH electronics-team] gnu: Add symbiyosys.
Date: Fri, 25 Apr 2025 14:58:48 +0200

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

Ok, the problem is understood.

#78059 is to be used by yosys, which will fix the testing problems with symbiyosys.

We need then to use abc fork by yosyshq with all of their packages.

C.

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

Previous Next

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