Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: NixOS/nixpkgs
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: 572a63faf8d6
Choose a base ref
...
head repository: NixOS/nixpkgs
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: 7e66ce29bfe1
Choose a head ref
  • 2 commits
  • 3 files changed
  • 1 contributor

Commits on Feb 28, 2020

  1. symbiyosys: fix calls to external programs 

    4808582 broke symbiyosys when it needed to call `yosys-abc`: when
`ABCEXTERNAL` is set in the Makefile, then `yosys-abc` is not built.

But in general `sby` was just calling programs out of the ambient
environment. Fix that for most programs it can invoke: it now has a
direct dependency on boolector, aiger, abc, yosys, etc.

This also does some other minor clean up.

Signed-off-by: Austin Seipp <aseipp@pobox.com>
    @thoughtpolice
    thoughtpolice committed Feb 28, 2020
    Copy the full SHA
    3d8efec View commit details

  2. mcy: init at 2020.02.05 

    Signed-off-by: Austin Seipp <aseipp@pobox.com>
    @thoughtpolice
    thoughtpolice committed Feb 28, 2020
    Copy the full SHA
    7e66ce2 View commit details
Showing with 67 additions and 12 deletions.
  1. +41 −0 pkgs/applications/science/logic/mcy/default.nix
  2. +24 −12 pkgs/applications/science/logic/symbiyosys/default.nix
  3. +2 −0 pkgs/top-level/all-packages.nix
41 changes: 41 additions & 0 deletions pkgs/applications/science/logic/mcy/default.nix
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
{ stdenv, fetchFromGitHub
, yosys, symbiyosys, python3
}:

let
python = python3.withPackages (p: with p; [ flask ]);
in
stdenv.mkDerivation {
pname = "mcy";
version = "2020.02.05";

src = fetchFromGitHub {
owner = "YosysHQ";
repo = "mcy";
rev = "83deeddd12d583a89ad4aa1d2147efa4d6adc33c";
sha256 = "1i0cabiqr68zflwzc6z894i4n7k6m3hbfck58vzh8zb9jwxwizav";
};

buildInputs = [ python ];
patchPhase = ''
substituteInPlace mcy.py \
--replace yosys '${yosys}/bin/yosys' \
--replace 'os.execvp("mcy-dash"' "os.execvp(\"$out/libexec/mcy/mcy-dash.py\""
'';

# the build needs a bit of work...
buildPhase = "true";
installPhase = ''
mkdir -p $out/bin $out/libexec/mcy
install mcy.py $out/bin/mcy && chmod +x $out/bin/mcy
install mcy-dash.py $out/libexec/mcy/mcy-dash.py
'';

meta = {
description = "Mutation-based coverage testing for hardware designs, with Yosys";
homepage = "https://github.com/YosysHQ/mcy";
license = stdenv.lib.licenses.isc;
maintainers = with stdenv.lib.maintainers; [ thoughtpolice ];
platforms = stdenv.lib.platforms.all;
};
}
36 changes: 24 additions & 12 deletions pkgs/applications/science/logic/symbiyosys/default.nix
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
{ stdenv, fetchFromGitHub, yosys, bash, python3, yices }:
{ stdenv, fetchFromGitHub
, bash, python3, yosys
, yices, boolector, aiger, abc-verifier
}:

stdenv.mkDerivation {
pname = "symbiyosys";
@@ -11,29 +14,38 @@ stdenv.mkDerivation {
sha256 = "1pwbirszc80r288x81nx032snniqgmc80i09bbha2i3zd0c3pj5h";
};

buildInputs = [ python3 yosys ];
buildInputs = [ python3 ];
patchPhase = ''
patchShebangs .
propagatedBuildInputs = [ yices ];
# Fix up Yosys imports
substituteInPlace sbysrc/sby.py \
--replace "##yosys-sys-path##" \
"sys.path += [p + \"/share/yosys/python3/\" for p in [\"$out\", \"${yosys}\"]]"
# Fix various executable references
substituteInPlace sbysrc/sby_core.py \
--replace '"/usr/bin/env", "bash"' '"${bash}/bin/bash"' \
--replace ': "btormc"' ': "${boolector}/bin/btormc"' \
--replace ': "yosys"' ': "${yosys}/bin/yosys"' \
--replace ': "yosys-smtbmc"' ': "${yosys}/bin/yosys-smtbmc"' \
--replace ': "yosys-abc"' ': "${abc-verifier}/bin/abc"' \
--replace ': "aigbmc"' ': "${aiger}/bin/aigbmc"' \
'';

buildPhase = "true";
installPhase = ''
mkdir -p $out/bin $out/share/yosys/python3
cp sbysrc/sby_*.py $out/share/yosys/python3/
cp sbysrc/sby.py $out/bin/sby
chmod +x $out/bin/sby
# Fix up shebang and Yosys imports
patchShebangs $out/bin/sby
substituteInPlace $out/bin/sby \
--replace "##yosys-sys-path##" \
"sys.path += [p + \"/share/yosys/python3/\" for p in [\"$out\", \"${yosys}\"]]"
substituteInPlace $out/share/yosys/python3/sby_core.py \
--replace '"/usr/bin/env", "bash"' '"${bash}/bin/bash"'
chmod +x $out/bin/sby
'';

meta = {
description = "Tooling for Yosys-based verification flows";
homepage = https://symbiyosys.readthedocs.io/;
homepage = "https://symbiyosys.readthedocs.io/";
license = stdenv.lib.licenses.isc;
maintainers = with stdenv.lib.maintainers; [ thoughtpolice emily ];
platforms = stdenv.lib.platforms.all;
2 changes: 2 additions & 0 deletions pkgs/top-level/all-packages.nix
View file
Original file line number Diff line number Diff line change
@@ -24503,6 +24503,8 @@ in

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

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

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

### SCIENCE / ELECTRONICS