Commit c3420851 authored by Roland Coeurjoly's avatar Roland Coeurjoly Committed by Austin Seipp
Browse files

sby: 2021.11.30 -> 0.44, run tests, rename from symbiyosys

parent 965ba5d5

pkgs/applications/science/logic/symbiyosys/default.nix→pkgs/by-name/sb/sby/package.nix

+106 −0
Original line number Diff line number Diff line 
{ lib, stdenv, fetchFromGitHub

, bash, python3, yosys

, yices, boolector, z3, aiger

{

  lib,

  stdenv,

  fetchFromGitHub,

  bash,

  python3,

  yosys,

  yices,

  boolector,

  z3,

  aiger,

  python3Packages,

  nix-update-script,

}:



stdenv.mkDerivation {

  pname = "symbiyosys";

  version = "2021.11.30";

let

  pythonEnv = python3.withPackages (ps: with ps; [ click ]);

in



stdenv.mkDerivation rec {

  pname = "sby";

  version = "0.44";



  src = fetchFromGitHub {

    owner = "YosysHQ";

    repo  = "SymbiYosys";

    rev   = "b409b1179e36d2a3fff66c85b7d4e271769a2d9e";

    hash  = "sha256-S7of2upntiMkSdh4kf1RsrjriS31Eh8iEcVvG36isQg=";

    repo = "sby";

    rev = "yosys-${version}";

    hash = "sha256-/oDbbdZuWPdg0Xrh+c4i283vML9QTfyWVu8kryb4WaE=";

  };



  buildInputs = [ ];

  nativeBuildInputs = [ bash ];

  buildInputs = [

    pythonEnv

    yosys

    boolector

    yices

    z3

    aiger

  ];



  patchPhase = ''

    patchShebangs .
@@ -33,7 +56,7 @@ stdenv.mkDerivation { 
      --replace '##yosys-program-prefix##' '"${yosys}/bin/"'



    substituteInPlace sbysrc/sby.py \

      --replace '/usr/bin/env python3' '${python3}/bin/python'

      --replace '/usr/bin/env python3' '${pythonEnv}/bin/python'

  '';



  buildPhase = "true";
@@ -47,15 +70,36 @@ stdenv.mkDerivation { 
    chmod +x $out/bin/sby

  '';



  doCheck = false; # not all provers are yet packaged...

  nativeCheckInputs = [ python3 yosys boolector yices z3 aiger ];

  checkPhase = "make test";

  doCheck = true;

  nativeCheckInputs = [

    pythonEnv

    yosys

    boolector

    yices

    z3

    aiger

  ];

  checkPhase = ''

    runHook preCheck

    make test

    runHook postCheck

  '';



  passthru.updateScript = nix-update-script {

    extraArgs = [

      "--version-regex"

      "yosys-([0-9].*)"

    ];

  };



  meta = {

    description = "Tooling for Yosys-based verification flows";

    description = "SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows";

    homepage = "https://symbiyosys.readthedocs.io/";

    license = lib.licenses.isc;

    maintainers = with lib.maintainers; [ thoughtpolice ];

    maintainers = with lib.maintainers; [

      thoughtpolice

      rcoeurjoly

    ];

    mainProgram = "sby";

    platforms = lib.platforms.all;

  };

pkgs/development/python-modules/amaranth/default.nix

+2 −2
Original line number Diff line number Diff line
@@ -13,7 +13,7 @@ 


  # for tests

  pytestCheckHook,

  symbiyosys,

  sby,

  yices,

  yosys,

}:
@@ -47,7 +47,7 @@ buildPythonPackage rec { 


  nativeCheckInputs = [

    pytestCheckHook

    symbiyosys

    sby

    yices

    yosys

  ];

pkgs/top-level/aliases.nix

+1 −0
Original line number Diff line number Diff line
@@ -1432,6 +1432,7 @@ mapAliases ({ 
  swift-im = throw "swift-im has been removed as it is unmaintained and depends on deprecated Python 2 / Qt WebKit"; # Added 2023-01-06

  swtpm-tpm2 = swtpm; # Added 2021-02-26

  Sylk = sylk; # Added 2024-06-12

  symbiyosys = sby; # Added 2024-08-18

  syncthing-cli = syncthing; # Added 2021-04-06

  syncthingtray-qt6 = syncthingtray; # Added 2024-03-06

pkgs/top-level/all-packages.nix

+0 −2
Original line number Diff line number Diff line
@@ -37659,8 +37659,6 @@ with pkgs; 














  bitwuzla = callPackage ../applications/science/logic/bitwuzla { };



























  symbiyosys = callPackage ../applications/science/logic/symbiyosys { };



























  symfpu = callPackage ../applications/science/logic/symfpu { };





























  uhdm = callPackage ../applications/science/logic/uhdm { };