[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileAr...

diff --git a/0a/0adae50556bb33be5f4f9215d5f62c6954acd8 b/0a/0adae50556bb33be5f4f9215d5f62c6954acd8
new file mode 100644 (file)
index 0000000..5385536
--- /dev/null
+++ b/0a/0adae50556bb33be5f4f9215d5f62c6954acd8
@@ -0,0 +1,109 @@
+Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
+Envelope-to: publicinbox@libre-riscv.org
+Delivery-date: Sun, 31 May 2020 19:20:15 +0100
+Received: from localhost ([::1] helo=libre-riscv.org)
+       by libre-soc.org with esmtp (Exim 4.89)
+       (envelope-from <libre-riscv-dev-bounces@lists.libre-riscv.org>)
+       id 1jfSZC-0003vm-FR; Sun, 31 May 2020 19:20:14 +0100
+Received: from localhost ([127.0.0.1] helo=bugs.libre-soc.org)
+ by libre-soc.org with esmtp (Exim 4.89)
+ (envelope-from <bugzilla-daemon@libre-soc.org>) id 1jfSZA-0003vZ-Nj
+ for libre-riscv-dev@lists.libre-riscv.org; Sun, 31 May 2020 19:20:12 +0100
+From: bugzilla-daemon@libre-soc.org
+To: libre-riscv-dev@lists.libre-riscv.org
+Date: Sun, 31 May 2020 18:20:13 +0000
+X-Bugzilla-Reason: CC
+X-Bugzilla-Type: changed
+X-Bugzilla-Watch-Reason: None
+X-Bugzilla-Product: Libre-SOC's first SoC
+X-Bugzilla-Component: Formal Verification
+X-Bugzilla-Version: unspecified
+X-Bugzilla-Keywords: 
+X-Bugzilla-Severity: enhancement
+X-Bugzilla-Who: cestrauss@gmail.com
+X-Bugzilla-Status: CONFIRMED
+X-Bugzilla-Resolution: 
+X-Bugzilla-Priority: ---
+X-Bugzilla-Assigned-To: colepoirier@gmail.com
+X-Bugzilla-Flags: 
+X-Bugzilla-Changed-Fields: cc
+Message-ID: <bug-353-13-ML7jgkS6VV@https.bugs.libre-soc.org/>
+In-Reply-To: <bug-353-13@https.bugs.libre-soc.org/>
+References: <bug-353-13@https.bugs.libre-soc.org/>
+X-Bugzilla-URL: https://bugs.libre-soc.org/
+Auto-Submitted: auto-generated
+MIME-Version: 1.0
+Subject: [libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes
+ RegFile and RegFileArray needed
+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>
+
+aHR0cHM6Ly9idWdzLmxpYnJlLXNvYy5vcmcvc2hvd19idWcuY2dpP2lkPTM1MwoKQ2VzYXIgU3Ry
+YXVzcyA8Y2VzdHJhdXNzQGdtYWlsLmNvbT4gY2hhbmdlZDoKCiAgICAgICAgICAgV2hhdCAgICB8
+UmVtb3ZlZCAgICAgICAgICAgICAgICAgICAgIHxBZGRlZAotLS0tLS0tLS0tLS0tLS0tLS0tLS0t
+LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tCiAg
+ICAgICAgICAgICAgICAgQ0N8ICAgICAgICAgICAgICAgICAgICAgICAgICAgIHxjZXN0cmF1c3NA
+Z21haWwuY29tCgotLS0gQ29tbWVudCAjMjkgZnJvbSBDZXNhciBTdHJhdXNzIDxjZXN0cmF1c3NA
+Z21haWwuY29tPiAtLS0KKEluIHJlcGx5IHRvIEx1a2UgS2VubmV0aCBDYXNzb24gTGVpZ2h0b24g
+ZnJvbSBjb21tZW50ICMyNykKPiBiYXNpY2FsbHkgaSBoYXZlIG5vIGlkZWEgd2hhdCBpIGFtIGRv
+aW5nIHdpdGggRm9ybWFsIFByb29mcy4gIGkgY2FuIHJlYWQKPiB0aGVtLCBpIGNhbiAqbWF5YmUq
+IHNwb3Qgb21pc3Npb25zIG9uY2UgdGhleSdyZSB3cml0dGVuLCBhbmQgaSBjYW4ganVzdCBhYm91
+dAo+IG1hbmFnZSBjb21iaW5hdG9yaWFsIG9uZXMuICB0aGVzZSBzeW5jL3RpbWUtYmFzZWQgb25l
+czogcmVhbGx5IG5vIGlkZWEuCgpIaSBMdWtlLAoKQXMgSSBsZWFybmVkIGFib3V0IGZvcm1hbCB2
+ZXJpZmljYXRpb24sIEkgZm91bmQgdGhlIGluaXRpYWwgc2xpZGVzIG9mCmh0dHA6Ly93d3cuY2xp
+ZmZvcmQuYXQvcGFwZXJzLzIwMTcvc210Ym1jLXNieS9zbGlkZXMucGRmIHZlcnkgZW5saWdodGVu
+aW5nIGZvcgpiYXNpYyBjb25jZXB0cy4gU2VlIGZvciBpbnN0YW5jZSBzbGlkZXMgNiB0byAxNi4K
+CihJbiByZXBseSB0byBMdWtlIEtlbm5ldGggQ2Fzc29uIExlaWdodG9uIGZyb20gY29tbWVudCAj
+MjgpCj4gaHR0cHM6Ly96aXBjcHUuY29tL2Jsb2cvMjAxOC8wMy8xMC9pbmR1Y3Rpb24tZXhlcmNp
+c2UuaHRtbAo+IAo+IGFsbCBpIGNhbiBzYXkgaXM6IGFyZ2ggOikKClRoaXMgaWxsdXN0cmF0ZXMg
+dGhlIGRpZmZpY3VsdGllcyBpbiBpbmR1Y3Rpb24gcHJvb2ZzLgoKSXQgaXMgYXBwYXJlbnQsIGZy
+b20gdGhlIGNpcmN1aXQsIHRoYXQgdGhlIHR3byBzaGlmdC1yZWdpc3RlcnMgd2lsbCBiZSBlcXVh
+bApmb3IgYWxsIHRpbWUsIHNvIHRoZSBYT1Igb3V0cHV0IHdpbGwgYmUgYWx3YXlzIHplcm8uCgpI
+b3dldmVyLCBib3VuZGVkIG1vZGVsIGNoZWNrIGNhbiBvbmx5IGNoZWNrIGZvciBhIGZpbml0ZSBu
+dW1iZXIgb2YgY3ljbGVzLiBUbwpwcm92ZSBpdCBmb3IgYWxsIHRpbWUsIHlvdSBwcm92ZSBpdCB0
+aGF0LCB3aGVuZXZlciB0aGUgYXNzZXJ0aW9ucyBob2xkIGZvciBuCmN5Y2xlcywgaXQgd2lsbCBo
+b2xkIGZvciB0aGUgbisxIGN5Y2xlLgoKVGhlIHByb2JsZW0gd2l0aCBpbmR1Y3Rpb24sIGlzIHRo
+YXQgaXQgZG9lcyBub3Qgc3RhcnQgd2l0aCB0aGUgaW5pdGlhbCBzdGF0ZQooc2VlIHNsaWRlIDEx
+KS4gU28sIHRoZSAiaW5pdGlhbCIgc3RhdGUgY2FuIGJlIGluIHRoZSB1bnJlYWNoYWJsZSBzdGF0
+ZSBhcmVhCihzZWUgc2xpZGUgOSkuCgpJbiB0aGUgZXhhbXBsZSwgYW4gaW5pdGlhbCBzdGF0ZSBp
+biB3aGljaCB0aGUgc2hpZnQgcmVnaXN0ZXIgYXJlIGRpZmZlcmVudCwgaXMKdW5yZWFjaGFibGUu
+IEJ1dCB0aGUgcHJvb2YgY2hlY2tlciBkb2VzIG5vdCBrbm93IHRoYXQuIFNvLCBpdCBjYW4gY2hv
+b3NlIGFuCmluaXRpYWwgc3RhdGUgd2hlcmUgdGhlIGxhc3QgYml0IGlzIGVxdWFsLCBwYXNzaW5n
+IHRoZSBhc3NlcnRpb24sIGJ1dCB0aGUKbmV4dC10by1sYXN0IGJpdCBpcyBkaWZmZXJlbnQuCgpU
+aGVuLCBpdCBob2xkcyB0aGUgc2hpZnQgZW5hYmxlIGRlLWFzc2VydGVkIGZvciBuIGN5Y2xlcyBh
+bmQgYXNzZXJ0cyBpdCBmb3IgdGhlCm4rMSBjeWNsZSwgZmluYWxseSBzaGlmdGluZyBvdXQgdGhl
+IGRpZmZlcmluZyBiaXRzLiBTbywgaXQgcGFzc2VzIGZvciBuIGN5Y2xlcywKYnV0IGZhaWxzIGlu
+IG4rMS4KClRoZSBlYXN5IHdheSB0byBzb2x2ZSB0aGlzIGlzIHRvIGFzc2VydCB0aGF0IHRoZSBz
+aGlmdCByZWdpc3RlciBjb250ZW50cyBhcmUKYWx3YXlzIGVxdWFsLgoKQW5vdGhlciB3YXkgaXMg
+bGltaXRpbmcgdGhlIHRpbWUgaW4gd2hpY2ggdGhlIHNoaWZ0LWVuYWJsZSBjYW4gYmUga2VwdApk
+ZS1hc3NlcnRlZC4gVGhpcyBpcyBkb25lIHdpdGggYW4gYXNzdW1wdGlvbi4KCldpdGhvdXQgYW4g
+YXNzdW1wdGlvbiwgdGhlIHByb29mIGNoZWNrZXIgaXMgZnJlZSB0byB0b2dnbGUgYW55IHVuY29u
+bmVjdGVkCmlucHV0IHNpZ25hbCwgaW4gdGhlIG1vc3QgcGVydmVyc2Ugd2F5IHBvc3NpYmxlLCB0
+byBtYWtlIHRoZSBwcm9vZiBmYWlsLiBJbgpyZWFsaXR5LCB0aGUgaW5wdXQgc2lnbmFscyBtdXN0
+IG9iZXkgc29tZSBwcm90b2NvbC4gRm9yIGluc3RhbmNlLCB5b3UgdGVsbCB0aGUKcHJvb2YgY2hl
+Y2tlciB0aGF0IGl0IG11c3Qga2VlcCAoYXNzdW1lKSBpc3N1ZV9pIGxvdyB3aGVuZXZlciBidXN5
+X28gaXMgaGlnaC4KT3RoZXJ3aXNlIGl0IHdvdWxkIGJlIGZyZWUgdG8gYXNzZXJ0IGlzc3VlX2kg
+aW4gdGhlIG1pZGRsZSBvZiBhIGJ1c3lfbyBjeWNsZSwKd2hpY2ggaXQncyBhIHZpb2xhdGlvbiBv
+ZiB0aGUgcHJvdG9jb2wuCgpIb3BlIGl0IGhlbHBzLAoKQ2VzYXIKCi0tIApZb3UgYXJlIHJlY2Vp
+dmluZyB0aGlzIG1haWwgYmVjYXVzZToKWW91IGFyZSBvbiB0aGUgQ0MgbGlzdCBmb3IgdGhlIGJ1
+Zy4KX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KbGlicmUt
+cmlzY3YtZGV2IG1haWxpbmcgbGlzdApsaWJyZS1yaXNjdi1kZXZAbGlzdHMubGlicmUtcmlzY3Yu
+b3JnCmh0dHA6Ly9saXN0cy5saWJyZS1yaXNjdi5vcmcvbWFpbG1hbi9saXN0aW5mby9saWJyZS1y
+aXNjdi1kZXYK
+