From 1ddfcfdc9601e5428250801d2223d1bb23fbe938 Mon Sep 17 00:00:00 2001
From: Cayetano Santos <csantosb@inventati.org>
Date: Sun, 19 Oct 2025 23:41:38 +0200
Subject: [PATCH] gnu: Add eqy.

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

Change-Id: I8ec52ccddc549ca6fa65ef073a905d09fa27000b
---
 gnu/packages/electronics.scm | 59 ++++++++++++++++++++++++++++++++++++
 1 file changed, 59 insertions(+)

diff --git a/gnu/packages/electronics.scm b/gnu/packages/electronics.scm
index 1991f1883bf04353615e8da1eafc8246e60ef1f2..305ca2194d70ee7f5a61398e2047856c69ba4847 100644
--- a/gnu/packages/electronics.scm
+++ b/gnu/packages/electronics.scm
@@ -335,6 +335,65 @@ individual low-level driver modules.")
     (home-page "https://www.comedi.org/")
     (license license:lgpl2.1)))
 
+(define-public eqy
+  (package
+    (name "eqy")
+    (version "0.59")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+              (url "https://github.com/YosysHQ/eqy/")
+              (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32 "1lbi3pn4d2zmqy2pd3pvdv007znildr06ink2g8sh6c9zb74xrk4"))))
+    (build-system gnu-build-system)
+    (arguments
+     (list
+      #:imported-modules (append %default-gnu-imported-modules
+                                 %python-build-system-modules)
+      #:make-flags
+      #~(list (string-append "PREFIX=" #$output))
+      #:phases
+      #~(modify-phases %standard-phases
+          (delete 'configure)
+          (delete 'build)
+          (delete 'check)
+          (add-after 'unpack 'build-info
+            (lambda _
+              (invoke "make" "-C" "docs" "info")
+              (install-file "docs/build/texinfo/yosyshqeqy.info"
+                            (string-append #$output "/share/info"))))
+          (add-after 'unpack 'patch-/usr/bin/env
+            (lambda _
+              (substitute* "src/eqy_job.py"
+                (("\"/usr/bin/env\", ") ""))))
+          (add-after 'install 'check-after-install
+            (lambda* (#:key tests? #:allow-other-keys)
+              (when tests?
+                (setenv "PATH"
+                        (string-append #$output "/bin:" (getenv "PATH")))
+                ;; make test fails on upstream, see:
+                ;; https://github.com/YosysHQ/eqy/actions/runs/18767539188/job/53545383858
+                (invoke "make" "-C" "examples/spm")
+                (invoke "make" "-C" "examples/simple"))))
+          (add-after 'install 'python:wrap
+            (@@ (guix build python-build-system) wrap)))))
+    (native-inputs
+     (list clang python-minimal-wrapper python-sphinx texinfo yosys-clang))
+    (inputs
+     (list python-click python-json5 readline))
+    (home-page "https://yosyshq.readthedocs.io/projects/eqy/en/latest/")
+    (synopsis "Equivalence checking using formal verification with Yosys")
+    (description
+     "@command{Eqy} is a front-end driver program for Yosys-based formal
+hardware equivalence checking.  It performs formal verification on two
+designs, such as ensuring that a synthesis tool has not introduced functional
+changes into a design, or ensuring that a design refactor preserves
+correctness in all conditions.")
+    (license license:isc)))
+
 (define-public ieee-p1076
   (package
     (name "ieee-p1076")