yosys-et-al

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