yosys-et-al

   1 mkdir hdl
   2 cd hdl
   3 git clone https://github.com/cliffordwolf/yosys.git
   4 cd yosys
   5 make config-clang
   6 make -j$(nproc)
   7 make -j$(nproc) test
   8 make install
   9
  10 cd ../
  11 git clone https://github.com/YosysHQ/SymbiYosys.git SymbiYosys
  12 cd SymbiYosys
  13 make install
  14
  15 cd ../
  16 git clone https://github.com/SRI-CSL/yices2.git yices2
  17 cd yices2
  18 autoconf
  19 ./configure
  20 make -j$(nproc)
  21 make install
  22
  23 cd ../
  24 git clone https://github.com/Z3Prover/z3.git z3
  25 cd z3
  26 python scripts/mk_make.py
  27 cd build
  28 make -j$(nproc)
  29 make install
  30
  31 cd ../../
  32 hg clone https://bitbucket.org/sterin/super_prove_build
  33 cd super_prove_build
  34 patch -u abc-zz/MetaSat/MiniSat2/System.cc <(echo "diff -r bde167bca3cd MetaSat/MiniSat2/System.cc
  35 --- a/MetaSat/MiniSat2/System.cc        Thu Sep 14 01:44:08 2017 -0700
  36 +++ b/MetaSat/MiniSat2/System.cc        Thu May 14 20:10:24 2020 +0000
  37 @@ -20,6 +20,7 @@
  38
  39  #include <signal.h>
  40  #include <stdio.h>
  41 +#include <stdlib.h>
  42
  43  #include "System.hh"
  44
  45 @@ -27,7 +28,6 @@
  46
  47  #if defined(__linux__)
  48
  49 -#include <stdlib.h>
  50
  51  static inline int memReadStat(int field)
  52  {
  53 ")
  54 patch -u abc-zz/Bip/Main_bip.cc <(echo "diff -r bde167bca3cd Bip/Main_bip.cc
  55 --- a/Bip/Main_bip.cc   Thu Sep 14 01:44:08 2017 -0700
  56 +++ b/Bip/Main_bip.cc   Thu May 14 20:08:52 2020 +0000
  57 @@ -508,8 +508,8 @@
  58  void writeCex(Out& out, NetlistRef N, const Cex& cex, uint orig_num_pis)
  59  {
  60      Vec<Pair<int,GLit> > ffs, pis;
  61 -    For_Gatetype(N, gate_Flop, w) ffs.push(tuple(attr_Flop(w).number, w));
  62 -    For_Gatetype(N, gate_PI  , w) pis.push(tuple(attr_PI  (w).number, w));
  63 +    For_Gatetype(N, gate_Flop, w) ffs.push(ZZ::tuple(attr_Flop(w).number, w));
  64 +    For_Gatetype(N, gate_PI  , w) pis.push(ZZ::tuple(attr_PI  (w).number, w));
  65      sort(ffs);
  66      sort(pis);
  67
  68 ")
  69 mkdir build && cd build
  70 cmake -DCMAKE_BUILD_TYPE=Release -G Ninja ..
  71 ninja
  72 ninja package
  73 SPBIN=`find . -maxdepth 1 -name "super_prove*-Release.tar.gz"`
  74 tar xvf $SPBIN -C /usr/local/bin/
  75 cat << "EOF" > /usr/local/bin/suprove
  76 #!/bin/bash
  77 tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi
  78 exec /usr/local/bin/super_prove/bin/${tool}.sh "$@"
  79 EOF
  80 chmod +x /usr/local/bin/suprove
  81 suprove