From 1dad1ba44695036dabd4f9ba87d3fc83dff5d5c8 Mon Sep 17 00:00:00 2001 From: bugzilla-daemon Date: Sun, 31 May 2020 18:20:13 +0000 Subject: [PATCH] [libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed --- 0a/0adae50556bb33be5f4f9215d5f62c6954acd8 | 109 ++++++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 0a/0adae50556bb33be5f4f9215d5f62c6954acd8 diff --git a/0a/0adae50556bb33be5f4f9215d5f62c6954acd8 b/0a/0adae50556bb33be5f4f9215d5f62c6954acd8 new file mode 100644 index 0000000..5385536 --- /dev/null +++ b/0a/0adae50556bb33be5f4f9215d5f62c6954acd8 @@ -0,0 +1,109 @@ +Return-path: +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 ) + 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 ) 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: +In-Reply-To: +References: +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 + +List-Unsubscribe: , + +List-Archive: +List-Post: +List-Help: +List-Subscribe: , + +Reply-To: Libre-RISCV General Development + +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" + +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 + -- 2.30.2