[libre-riscv-dev] New formal verification checking tool

diff --git a/a8/84fda6695befbb10784905783ba4917fe432c1 b/a8/84fda6695befbb10784905783ba4917fe432c1
new file mode 100644 (file)
index 0000000..d26bcc1
--- /dev/null
+++ b/a8/84fda6695befbb10784905783ba4917fe432c1
@@ -0,0 +1,75 @@
+Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
+Envelope-to: publicinbox@libre-riscv.org
+Delivery-date: Sat, 21 Mar 2020 03:21:03 +0000
+Received: from localhost ([::1] helo=libre-riscv.org)
+       by libre-riscv.org with esmtp (Exim 4.89)
+       (envelope-from <libre-riscv-dev-bounces@lists.libre-riscv.org>)
+       id 1jFUh3-0002QQ-K3; Sat, 21 Mar 2020 03:21:01 +0000
+Received: from mail-io1-f46.google.com ([209.85.166.46])
+ by libre-riscv.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
+ (Exim 4.89) (envelope-from <sam.falvo@gmail.com>) id 1jFUh1-0002QK-VI
+ for libre-riscv-dev@lists.libre-riscv.org; Sat, 21 Mar 2020 03:21:00 +0000
+Received: by mail-io1-f46.google.com with SMTP id h131so8419217iof.1
+ for <libre-riscv-dev@lists.libre-riscv.org>;
+ Fri, 20 Mar 2020 20:20:59 -0700 (PDT)
+DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
+ h=mime-version:from:date:message-id:subject:to;
+ bh=q3PZ7/ozmoW8Wv+CBQpvL5eh0UxOop3liK/zOUON/5k=;
+ b=CYy9+2kZzuGW3rqtgSQoE1P53mFcll/CqOyZjmP2YsmB2rfE5PRvrLp8CZc2cBDu5S
+ xhHgtk67iUb9s/L59gbhp4xtfeoLQHFvOIX4RDjrynCPBvrtkfxP+C4GqrdW2YxOT1ts
+ StdFDMNlFy5aGH4Nd870qXOeXOsheZZdq5fEo/Nk2ZoHV2O6Wt6QAzYU0SJ3Hxul7eZ4
+ uDsX0FvwBnXdU8X7wDdZn4W73roi0+qeuPz7GBDiZjKR8CIrtvdKqlRmZzEZ/6q9pY1Q
+ zU0GO/5iALoj7ydE8VcR+AhtvU6GwOasxKYF+3Mr1d5j1SWTCY/EP+Nn7n+L/JBS5goA
+ 2USg==
+X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
+ d=1e100.net; s=20161025;
+ h=x-gm-message-state:mime-version:from:date:message-id:subject:to;
+ bh=q3PZ7/ozmoW8Wv+CBQpvL5eh0UxOop3liK/zOUON/5k=;
+ b=iVInW9aKSho31sA9CD+/43rxjuXb2p13CCqNBnkZakUYwssFYD+ZX6n5trgd8yInDR
+ L8LwSpOlbaXuz6q2l8GuU9m2t1LpPsN9G6iPN2Va8XwTYYFMGb/V2WmTrbGC/3b7xNLq
+ cDiG7IDtP3pdOG1+xbEi153gy/Jv7tdKX8AOtcfm3kjq2dmIh0uCO6lOzGiGyquLtzjd
+ bXrWi4rfGhQp1jOQUG/f/bmGR7rDCPMc7cSpkxW205DpWB0niburD2o0oHC+RmwgKhPA
+ QK5C1D0HZbJsHJsH9lJGFFvovzK2D68mvR+uV8aPBwUnnuXWXRsRP2Z4lFm8az8T4r/A
+ hkUQ==
+X-Gm-Message-State: ANhLgQ1mf5akRWQMZ3QGqjqRYys+jeqOHG0lKR4tTW5V/b4Qj4DE0m4D
+ f5e/RccD1Tbbpxx9rVoPu1a8GC37sNibPXD6ReiF5Tjg
+X-Google-Smtp-Source: ADFU+vuui1GsQeIHEhdF7Xlhv54plvsUcx56OGhTN1H3RAHmVtAFxYF9P5WEzBzUPzZdIifANP986eKBdVa/AfxNzB8=
+X-Received: by 2002:a02:1485:: with SMTP id 127mr2216911jag.122.1584760858098; 
+ Fri, 20 Mar 2020 20:20:58 -0700 (PDT)
+MIME-Version: 1.0
+From: Samuel Falvo II <sam.falvo@gmail.com>
+Date: Fri, 20 Mar 2020 20:20:47 -0700
+Message-ID: <CAEz=somJ3zNUJkCPhjGpsu7KFnGUcSUgzKr4bvNuVch7KmMd4A@mail.gmail.com>
+To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
+X-Content-Filtered-By: Mailman/MimeDel 2.1.23
+Subject: [libre-riscv-dev] New formal verification checking tool
+X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
+X-Mailman-Version: 2.1.23
+Precedence: list
+List-Id: Libre-RISCV General Development
+ <libre-riscv-dev.lists.libre-riscv.org>
+List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>, 
+ <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
+List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
+List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
+List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
+List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>, 
+ <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
+Reply-To: Libre-RISCV General Development
+ <libre-riscv-dev@lists.libre-riscv.org>
+Content-Type: text/plain; charset="utf-8"
+Content-Transfer-Encoding: base64
+Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
+Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
+
+SSBzYXcgYSB0d2VldCBvbiBteSB0aW1lbGluZSB3aGljaCBhbm5vdW5jZWQgYSBuZXcgdGVzdCBj
+b3ZlcmFnZSBhbmFseXNpcwp0b29sIHdoaWNoIHVzZXMgWW9zeXMnIHN1cHBvcnQgZm9yIGZvcm1h
+bCBtZXRob2RzIHRvIGNhbGN1bGF0ZSB5b3VyIHRlc3QKY292ZXJhZ2UuCgpJIGRvbid0IGtub3cg
+aG93IGFwcGxpY2FibGUgdGhpcyB3b3VsZCBiZSB0byB0aGlzIHByb2plY3QsIGJ1dCB0aG91Z2h0
+IEknZApwYXNzIGl0IGFsb25nIGluIHRoZSBob3BlcyB0aGF0IGl0J2QgYmUgdXNlZnVsLgoKaHR0
+cHM6Ly93d3cueW91dHViZS5jb20vd2F0Y2g/dj1OS3pxUnVtMWtzZyZmZWF0dXJlPWVtYl90aXRs
+ZQoKCi0tIApTYW11ZWwgQS4gRmFsdm8gSUkKX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f
+X19fX19fX19fX19fX19fX18KbGlicmUtcmlzY3YtZGV2IG1haWxpbmcgbGlzdApsaWJyZS1yaXNj
+di1kZXZAbGlzdHMubGlicmUtcmlzY3Yub3JnCmh0dHA6Ly9saXN0cy5saWJyZS1yaXNjdi5vcmcv
+bWFpbG1hbi9saXN0aW5mby9saWJyZS1yaXNjdi1kZXYK
+