From mboxrd@z Thu Jan 1 00:00:00 1970 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" Archived-At: List-Archive: 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=