From: colepoirier <colepoirier@gmail.com>
Date: Thu, 14 May 2020 22:31:57 +0000 (-0700)
Subject: First working draft of 'yosys-et-al' script for building and
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1a2955211a5ecafab2ac8f70152c00516bd4ce71;p=dev-env-setup.git

First working draft of 'yosys-et-al' script for building and
installing all necessary yosys related tools from source
---

diff --git a/yosys-et-al b/yosys-et-al
new file mode 100755
index 0000000..1e73470
--- /dev/null
+++ b/yosys-et-al
@@ -0,0 +1,81 @@
+mkdir hdl
+cd hdl
+git clone https://github.com/cliffordwolf/yosys.git
+cd yosys
+make config-clang
+make -j$(nproc)
+make -j$(nproc) test
+make install
+
+cd ../
+git clone https://github.com/YosysHQ/SymbiYosys.git SymbiYosys
+cd SymbiYosys
+make install
+
+cd ../
+git clone https://github.com/SRI-CSL/yices2.git yices2
+cd yices2
+autoconf
+./configure
+make -j$(nproc)
+make install
+
+cd ../
+git clone https://github.com/Z3Prover/z3.git z3
+cd z3
+python scripts/mk_make.py
+cd build
+make -j$(nproc)
+make install
+
+cd ../../
+hg clone https://bitbucket.org/sterin/super_prove_build
+cd super_prove_build
+patch -u abc-zz/MetaSat/MiniSat2/System.cc <(echo "diff -r bde167bca3cd MetaSat/MiniSat2/System.cc
+--- a/MetaSat/MiniSat2/System.cc	Thu Sep 14 01:44:08 2017 -0700
++++ b/MetaSat/MiniSat2/System.cc	Thu May 14 20:10:24 2020 +0000
+@@ -20,6 +20,7 @@
+ 
+ #include <signal.h>
+ #include <stdio.h>
++#include <stdlib.h>
+ 
+ #include "System.hh"
+ 
+@@ -27,7 +28,6 @@
+ 
+ #if defined(__linux__)
+ 
+-#include <stdlib.h>
+ 
+ static inline int memReadStat(int field)
+ {
+")
+patch -u abc-zz/Bip/Main_bip.cc <(echo "diff -r bde167bca3cd Bip/Main_bip.cc
+--- a/Bip/Main_bip.cc	Thu Sep 14 01:44:08 2017 -0700
++++ b/Bip/Main_bip.cc	Thu May 14 20:08:52 2020 +0000
+@@ -508,8 +508,8 @@
+ void writeCex(Out& out, NetlistRef N, const Cex& cex, uint orig_num_pis)
+ {
+     Vec<Pair<int,GLit> > ffs, pis;
+-    For_Gatetype(N, gate_Flop, w) ffs.push(tuple(attr_Flop(w).number, w));
+-    For_Gatetype(N, gate_PI  , w) pis.push(tuple(attr_PI  (w).number, w));
++    For_Gatetype(N, gate_Flop, w) ffs.push(ZZ::tuple(attr_Flop(w).number, w));
++    For_Gatetype(N, gate_PI  , w) pis.push(ZZ::tuple(attr_PI  (w).number, w));
+     sort(ffs);
+     sort(pis);                             
+ 
+")
+mkdir build && cd build
+cmake -DCMAKE_BUILD_TYPE=Release -G Ninja ..
+ninja
+ninja package
+SPBIN=`find . -maxdepth 1 -name "super_prove*-Release.tar.gz"`
+tar xvf $SPBIN -C /usr/local/bin/
+cat << "EOF" > /usr/local/bin/suprove
+#!/bin/bash
+tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi
+exec /usr/local/bin/super_prove/bin/${tool}.sh "$@"
+EOF
+chmod +x /usr/local/bin/suprove
+suprove