Re: [libre-riscv-dev] daily kan-ban update 14may2020

From: Cole Poirier <colepoirier@gmail.com>
To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
Cc: "libre-riscv-dev@lists.libre-riscv.org"
	<libre-riscv-dev@lists.libre-riscv.org>
Subject: Re: [libre-riscv-dev] daily kan-ban update 14may2020
Date: Thu, 14 May 2020 15:29:20 -0700
Message-ID: <D51FC0DE-B374-474E-9FD3-E274B2452E18@getmailspring.com> (raw)
In-Reply-To: <1b10f48d-7ca9-a0ea-9f5c-9b0aafd754b2@gmail.com>

On May 14 2020, at 3:00 pm, Michael Nolan <mtnolan2640@gmail.com> wrote:
> I've never been able to/never bothered to install super_prove or aiger 
> for use with SymbiYosys. For running the formal proofs Libre-Soc has 
> done, I think you only need one of the SMTBMC solvers (my
> recommendation 
> is yices2).
> 
> --Michael

Thanks for the tip Michael! I'll definitely keep your reccomendation to
use yices2 in mind when setting the default engine in the script (if I
do end up needing to set one, I'm not done yet), and for myself when I
start trying to use nmigen.

In that regard, Luke, after I am done with the scripts and the
modifications to the docs on the wiki, is there some testing
infrastructure that needs to be worked on, or should I try to start
learning to make nmigen HDL contributions to the project? Essentially,
what do you reccomend I do next that would be most helpful to the project?

Here is my code for a working super_prove installation in case you are
interested in trying it out:
```
 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
```

Cole

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
