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