From 23979c94e3b7e03997d00672cb3c4e7ee53b6201 Mon Sep 17 00:00:00 2001 From: bugzilla-daemon Date: Mon, 1 Jun 2020 18:07:21 +0000 Subject: [PATCH] [libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed --- 91/a0200ce2204797969ff6c4f318ab4e6cfa766b | 109 ++++++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 91/a0200ce2204797969ff6c4f318ab4e6cfa766b diff --git a/91/a0200ce2204797969ff6c4f318ab4e6cfa766b b/91/a0200ce2204797969ff6c4f318ab4e6cfa766b new file mode 100644 index 0000000..9408189 --- /dev/null +++ b/91/a0200ce2204797969ff6c4f318ab4e6cfa766b @@ -0,0 +1,109 @@ +Return-path: +Envelope-to: publicinbox@libre-riscv.org +Delivery-date: Mon, 01 Jun 2020 19:07:23 +0100 +Received: from localhost ([::1] helo=libre-riscv.org) + by libre-soc.org with esmtp (Exim 4.89) + (envelope-from ) + id 1jfoqJ-0003w9-5h; Mon, 01 Jun 2020 19:07:23 +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 1jfoqH-0003vx-LF + for libre-riscv-dev@lists.libre-riscv.org; Mon, 01 Jun 2020 19:07:21 +0100 +From: bugzilla-daemon@libre-soc.org +To: libre-riscv-dev@lists.libre-riscv.org +Date: Mon, 01 Jun 2020 18:07:21 +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: colepoirier@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: +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" + +aHR0cHM6Ly9idWdzLmxpYnJlLXNvYy5vcmcvc2hvd19idWcuY2dpP2lkPTM1MwoKLS0tIENvbW1l +bnQgIzM2IGZyb20gQ29sZSBQb2lyaWVyIDxjb2xlcG9pcmllckBnbWFpbC5jb20+IC0tLQooSW4g +cmVwbHkgdG8gQ2VzYXIgU3RyYXVzcyBmcm9tIGNvbW1lbnQgIzI5KQo+IChJbiByZXBseSB0byBM +dWtlIEtlbm5ldGggQ2Fzc29uIExlaWdodG9uIGZyb20gY29tbWVudCAjMjcpCj4gPiBiYXNpY2Fs +bHkgaSBoYXZlIG5vIGlkZWEgd2hhdCBpIGFtIGRvaW5nIHdpdGggRm9ybWFsIFByb29mcy4gIGkg +Y2FuIHJlYWQKPiA+IHRoZW0sIGkgY2FuICptYXliZSogc3BvdCBvbWlzc2lvbnMgb25jZSB0aGV5 +J3JlIHdyaXR0ZW4sIGFuZCBpIGNhbiBqdXN0IGFib3V0Cj4gPiBtYW5hZ2UgY29tYmluYXRvcmlh +bCBvbmVzLiAgdGhlc2Ugc3luYy90aW1lLWJhc2VkIG9uZXM6IHJlYWxseSBubyBpZGVhLgo+IAo+ +IEhpIEx1a2UsCj4gCj4gQXMgSSBsZWFybmVkIGFib3V0IGZvcm1hbCB2ZXJpZmljYXRpb24sIEkg +Zm91bmQgdGhlIGluaXRpYWwgc2xpZGVzIG9mCj4gaHR0cDovL3d3dy5jbGlmZm9yZC5hdC9wYXBl +cnMvMjAxNy9zbXRibWMtc2J5L3NsaWRlcy5wZGYgdmVyeSBlbmxpZ2h0ZW5pbmcKPiBmb3IgYmFz +aWMgY29uY2VwdHMuIFNlZSBmb3IgaW5zdGFuY2Ugc2xpZGVzIDYgdG8gMTYuCj4gCj4gKEluIHJl +cGx5IHRvIEx1a2UgS2VubmV0aCBDYXNzb24gTGVpZ2h0b24gZnJvbSBjb21tZW50ICMyOCkKPiA+ +IGh0dHBzOi8vemlwY3B1LmNvbS9ibG9nLzIwMTgvMDMvMTAvaW5kdWN0aW9uLWV4ZXJjaXNlLmh0 +bWwKPiA+IAo+ID4gYWxsIGkgY2FuIHNheSBpczogYXJnaCA6KQo+IAo+IFRoaXMgaWxsdXN0cmF0 +ZXMgdGhlIGRpZmZpY3VsdGllcyBpbiBpbmR1Y3Rpb24gcHJvb2ZzLgo+IAo+IEl0IGlzIGFwcGFy +ZW50LCBmcm9tIHRoZSBjaXJjdWl0LCB0aGF0IHRoZSB0d28gc2hpZnQtcmVnaXN0ZXJzIHdpbGwg +YmUgZXF1YWwKPiBmb3IgYWxsIHRpbWUsIHNvIHRoZSBYT1Igb3V0cHV0IHdpbGwgYmUgYWx3YXlz +IHplcm8uCj4gCj4gSG93ZXZlciwgYm91bmRlZCBtb2RlbCBjaGVjayBjYW4gb25seSBjaGVjayBm +b3IgYSBmaW5pdGUgbnVtYmVyIG9mIGN5Y2xlcy4KPiBUbyBwcm92ZSBpdCBmb3IgYWxsIHRpbWUs +IHlvdSBwcm92ZSBpdCB0aGF0LCB3aGVuZXZlciB0aGUgYXNzZXJ0aW9ucyBob2xkCj4gZm9yIG4g +Y3ljbGVzLCBpdCB3aWxsIGhvbGQgZm9yIHRoZSBuKzEgY3ljbGUuCj4gCj4gVGhlIHByb2JsZW0g +d2l0aCBpbmR1Y3Rpb24sIGlzIHRoYXQgaXQgZG9lcyBub3Qgc3RhcnQgd2l0aCB0aGUgaW5pdGlh +bCBzdGF0ZQo+IChzZWUgc2xpZGUgMTEpLiBTbywgdGhlICJpbml0aWFsIiBzdGF0ZSBjYW4gYmUg +aW4gdGhlIHVucmVhY2hhYmxlIHN0YXRlIGFyZWEKPiAoc2VlIHNsaWRlIDkpLgo+IAo+IEluIHRo +ZSBleGFtcGxlLCBhbiBpbml0aWFsIHN0YXRlIGluIHdoaWNoIHRoZSBzaGlmdCByZWdpc3RlciBh +cmUgZGlmZmVyZW50LAo+IGlzIHVucmVhY2hhYmxlLiBCdXQgdGhlIHByb29mIGNoZWNrZXIgZG9l +cyBub3Qga25vdyB0aGF0LiBTbywgaXQgY2FuIGNob29zZQo+IGFuIGluaXRpYWwgc3RhdGUgd2hl +cmUgdGhlIGxhc3QgYml0IGlzIGVxdWFsLCBwYXNzaW5nIHRoZSBhc3NlcnRpb24sIGJ1dCB0aGUK +PiBuZXh0LXRvLWxhc3QgYml0IGlzIGRpZmZlcmVudC4KPiAgCj4gVGhlbiwgaXQgaG9sZHMgdGhl +IHNoaWZ0IGVuYWJsZSBkZS1hc3NlcnRlZCBmb3IgbiBjeWNsZXMgYW5kIGFzc2VydHMgaXQgZm9y +Cj4gdGhlIG4rMSBjeWNsZSwgZmluYWxseSBzaGlmdGluZyBvdXQgdGhlIGRpZmZlcmluZyBiaXRz +LiBTbywgaXQgcGFzc2VzIGZvciBuCj4gY3ljbGVzLCBidXQgZmFpbHMgaW4gbisxLgo+IAo+IFRo +ZSBlYXN5IHdheSB0byBzb2x2ZSB0aGlzIGlzIHRvIGFzc2VydCB0aGF0IHRoZSBzaGlmdCByZWdp +c3RlciBjb250ZW50cyBhcmUKPiBhbHdheXMgZXF1YWwuCj4gCj4gQW5vdGhlciB3YXkgaXMgbGlt +aXRpbmcgdGhlIHRpbWUgaW4gd2hpY2ggdGhlIHNoaWZ0LWVuYWJsZSBjYW4gYmUga2VwdAo+IGRl +LWFzc2VydGVkLiBUaGlzIGlzIGRvbmUgd2l0aCBhbiBhc3N1bXB0aW9uLgo+IAo+IFdpdGhvdXQg +YW4gYXNzdW1wdGlvbiwgdGhlIHByb29mIGNoZWNrZXIgaXMgZnJlZSB0byB0b2dnbGUgYW55IHVu +Y29ubmVjdGVkCj4gaW5wdXQgc2lnbmFsLCBpbiB0aGUgbW9zdCBwZXJ2ZXJzZSB3YXkgcG9zc2li +bGUsIHRvIG1ha2UgdGhlIHByb29mIGZhaWwuIEluCj4gcmVhbGl0eSwgdGhlIGlucHV0IHNpZ25h +bHMgbXVzdCBvYmV5IHNvbWUgcHJvdG9jb2wuIEZvciBpbnN0YW5jZSwgeW91IHRlbGwKPiB0aGUg +cHJvb2YgY2hlY2tlciB0aGF0IGl0IG11c3Qga2VlcCAoYXNzdW1lKSBpc3N1ZV9pIGxvdyB3aGVu +ZXZlciBidXN5X28gaXMKPiBoaWdoLiBPdGhlcndpc2UgaXQgd291bGQgYmUgZnJlZSB0byBhc3Nl +cnQgaXNzdWVfaSBpbiB0aGUgbWlkZGxlIG9mIGEgYnVzeV9vCj4gY3ljbGUsIHdoaWNoIGl0J3Mg +YSB2aW9sYXRpb24gb2YgdGhlIHByb3RvY29sLgo+IAo+IEhvcGUgaXQgaGVscHMsCj4gCj4gQ2Vz +YXIKClRoYW5rIHlvdSB2ZXJ5IG11Y2ggZm9yIHNoYXJpbmcgdGhpcyB0byBoZWxwIG1lIENlc2Fy +LCBpdCdzIHN1cGVyIGhlbHBmdWwsIGFuZApJJ20gaW5jcmVkaWJseSBncmF0ZWZ1bCBmb3IgeW91 +ciBoZWxwLgoKQ29sZQoKLS0gCllvdSBhcmUgcmVjZWl2aW5nIHRoaXMgbWFpbCBiZWNhdXNlOgpZ +b3UgYXJlIG9uIHRoZSBDQyBsaXN0IGZvciB0aGUgYnVnLgpfX19fX19fX19fX19fX19fX19fX19f +X19fX19fX19fX19fX19fX19fX19fX19fXwpsaWJyZS1yaXNjdi1kZXYgbWFpbGluZyBsaXN0Cmxp +YnJlLXJpc2N2LWRldkBsaXN0cy5saWJyZS1yaXNjdi5vcmcKaHR0cDovL2xpc3RzLmxpYnJlLXJp +c2N2Lm9yZy9tYWlsbWFuL2xpc3RpbmZvL2xpYnJlLXJpc2N2LWRldgo= + -- 2.30.2