[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / 03 / 271979e73d58401463ec84e2940303fa345108
1 Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
2 Envelope-to: publicinbox@libre-riscv.org
3 Delivery-date: Wed, 20 May 2020 02:04:14 +0100
4 Received: from localhost ([::1] helo=libre-riscv.org)
5 by libre-soc.org with esmtp (Exim 4.89)
6 (envelope-from <libre-riscv-dev-bounces@lists.libre-riscv.org>)
7 id 1jbD9Z-0007Gn-RF; Wed, 20 May 2020 02:04:13 +0100
8 Received: from localhost ([127.0.0.1] helo=bugs.libre-soc.org)
9 by libre-soc.org with esmtp (Exim 4.89)
10 (envelope-from <bugzilla-daemon@libre-soc.org>) id 1jbD9X-0007GY-VS
11 for libre-riscv-dev@lists.libre-riscv.org; Wed, 20 May 2020 02:04:12 +0100
12 From: bugzilla-daemon@libre-soc.org
13 To: libre-riscv-dev@lists.libre-riscv.org
14 Date: Wed, 20 May 2020 01:04:12 +0000
15 X-Bugzilla-Reason: CC
16 X-Bugzilla-Type: changed
17 X-Bugzilla-Watch-Reason: None
18 X-Bugzilla-Product: Libre-SOC's first SoC
19 X-Bugzilla-Component: Source Code
20 X-Bugzilla-Version: unspecified
21 X-Bugzilla-Keywords:
22 X-Bugzilla-Severity: normal
23 X-Bugzilla-Who: programmerjake@gmail.com
24 X-Bugzilla-Status: CONFIRMED
25 X-Bugzilla-Resolution:
26 X-Bugzilla-Priority: Normal
27 X-Bugzilla-Assigned-To: colepoirier@gmail.com
28 X-Bugzilla-Flags:
29 X-Bugzilla-Changed-Fields:
30 Message-ID: <bug-316-13-aJQsGElPw9@https.bugs.libre-soc.org/>
31 In-Reply-To: <bug-316-13@https.bugs.libre-soc.org/>
32 References: <bug-316-13@https.bugs.libre-soc.org/>
33 X-Bugzilla-URL: https://bugs.libre-soc.org/
34 Auto-Submitted: auto-generated
35 MIME-Version: 1.0
36 Subject: [libre-riscv-dev] [Bug 316] bperm TODO
37 X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
38 X-Mailman-Version: 2.1.23
39 Precedence: list
40 List-Id: Libre-RISCV General Development
41 <libre-riscv-dev.lists.libre-riscv.org>
42 List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>,
43 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
44 List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
45 List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
46 List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
47 List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>,
48 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
49 Reply-To: Libre-RISCV General Development
50 <libre-riscv-dev@lists.libre-riscv.org>
51 Content-Type: text/plain; charset="utf-8"
52 Content-Transfer-Encoding: base64
53 Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
54 Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
55
56 aHR0cHM6Ly9idWdzLmxpYnJlLXNvYy5vcmcvc2hvd19idWcuY2dpP2lkPTMxNgoKLS0tIENvbW1l
57 bnQgIzYyIGZyb20gSmFjb2IgTGlmc2hheSA8cHJvZ3JhbW1lcmpha2VAZ21haWwuY29tPiAtLS0K
58 KEluIHJlcGx5IHRvIEx1a2UgS2VubmV0aCBDYXNzb24gTGVpZ2h0b24gZnJvbSBjb21tZW50ICM1
59 OCkKPiAoSW4gcmVwbHkgdG8gSmFjb2IgTGlmc2hheSBmcm9tIGNvbW1lbnQgIzU1KQo+ID4gKElu
60 IHJlcGx5IHRvIENvbGUgUG9pcmllciBmcm9tIGNvbW1lbnQgIzU0KQo+ID4gPiBBaCB5ZXMsIGFw
61 cHJlY2lhdGVkLCBJIHdpbGwgZ3JlcCBmaXJzdCBpbiB0aGUgZnV0dXJlLiBGb3IgY2xhcmlmaWNh
62 dGlvbiwgdGhlCj4gPiA+IHdheSB0byBydW4gdGhlIHRlc3RzIGlzIGJ5IGNkJ2luZyB0byB0aGUg
63 c29jL2RlY29kZXIgZGlyZWN0b3J5IHRoZW4gcnVubmluZwo+ID4gPiAncHl0aG9uMyB0ZXN0L3t0
64 ZXN0X2ZpbGUucHl9JyBmb3IgZWFjaCBvZiB0aGUgZmlsZXMgaW4gdGhlIHRlc3RzIGRpcmVjdG9y
65 eT8KPiAKPiBiZWNhdXNlIGkgcnVuIGN0YWdzIGluIG9uZSBkaXJlY3RvcnkgKHVzdWFsbHkgdGhl
66 IHRvcCBsZXZlbCBvciBjbG9zZSB0byBpdCkKPiBhbmQgc3RheSB0aGVyZS4KPiAKPiBpIGdlbmVy
67 YWxseSBydW4gZS5nLiBweXRob24zIGZ1L2FsdS90ZXN0L3Rlc3RfcGlwZV9jYWxsZXIucHkgb3Ig
68 c29tZXRoaW5nLgo+IGNvbnN0YW50bHkgZG9pbmcgImNkIiBpIGZpbmQgdmVyeSBhbm5veWluZy4K
69 PiAKPiB0byBmaW5kIHByZXZpb3VzbHktcnVuIGNvbW1hbmRzIGlzIGEgbWF0dGVyIG9mIHJ1bm5p
70 bmcgImhpc3RvcnkiIGZvbGxvd2VkIGJ5Cj4gIWluc2VydGhpc3RvcnludW1iZXIKPiAKPiB0aGlz
71 IHNhdmVzIHR5cGluZyB0aGUgY29tbWFuZCBvdXQgcmVwZWF0ZWRseSAtIGFsc28gdmVyeSBhbm5v
72 eWluZy4KPiAKPiBsb3RzIG9mIGFubm95aW5nbmVzcy4uLiA6KQoKQXQgdGhlIGJhc2ggcHJvbXB0
73 LCB0eXBlIEN0cmwtUiB0aGVuIHNvbWUgcG9ydGlvbiBvZiB0aGUgcHJldmlvdXMgY29tbWFuZCwg
74 aXQncwp0aGUgcmVhZGxpbmUgc2hvcnRjdXQgZm9yIHNlYXJjaCB0aHJvdWdoIGhpc3RvcnkgZnJv
75 bSBtb3N0IHRvIGxlYXN0IHJlY2VudC4gWW91CmNhbiBhbHNvIGtlZXAgcHJlc3NpbmcgQ3RybC1S
76 IHRvIGdvIHRvIHRoZSBwcmV2aW91cyBvY2N1cnJlbmNlLgoKPiAKPiBob3dldmVyICphZnRlciog
77 dGhhdCBmYXN0LWl0ZXJhdGl2ZSBjeWNsZSAoZXhwbGljaXRseSBydW5uaW5nIG9ubHkgdGhlCj4g
78 cmVsZXZhbnQKPiB0ZXN0KSwgaXQgaXMga2luZGEgaW1wb3J0YW50IHRvIHJ1biBtb3JlIChub3Nl
79 dGVzdHMzLCBweXRob24zIHNldHVwLnB5IHRlc3QpCj4ganVzdAo+IHRvIG1ha2UgYWJzb2x1dGVs
80 eSBzdXJlIHlvdSBkaWRuJ3QgYnJlYWsgYW55dGhpbmcgdW5yZWxhdGVkLiAgZG9uJ3QgdGVsbAo+
81 IG5vLW9uZQo+IGkgdGVuZCBub3QgdG8gZG8gdGhhdCB2ZXJ5IG9mdGVuLi4uIDopCgpzaG91bGQg
82 ZG8gaXQgbW9yZSBvZnRlbiwgc2luY2Ugb3RoZXJ3aXNlIHN0dWZmIG5ldmVyIGdldHMgZml4ZWQu
83 IFBhcnQgb2Ygd2h5IEkKd2VudCB0byBsb3RzIG9mIGVmZm9ydCB0byBnZXQgQ0kgc2V0dXAgYW5k
84 IHdvcmtpbmcgKHdoaWNoIHN0aWxsIG5lZWRzIHNvbWVvbmUKdG8gZmluaXNoIHNldHRpbmcgdXAg
85 dGhlIENJIG1haWxpbmcgbGlzdCBhbmQgdGhlIHNlbmRtYWlsIHNjcmlwdCBmb3IgdXNlIHdpdGgK
86 Z2l0bGFiLWNpLWFyY2hpdmVyKS4KCi0tIApZb3UgYXJlIHJlY2VpdmluZyB0aGlzIG1haWwgYmVj
87 YXVzZToKWW91IGFyZSBvbiB0aGUgQ0MgbGlzdCBmb3IgdGhlIGJ1Zy4KX19fX19fX19fX19fX19f
88 X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KbGlicmUtcmlzY3YtZGV2IG1haWxpbmcg
89 bGlzdApsaWJyZS1yaXNjdi1kZXZAbGlzdHMubGlicmUtcmlzY3Yub3JnCmh0dHA6Ly9saXN0cy5s
90 aWJyZS1yaXNjdi5vcmcvbWFpbG1hbi9saXN0aW5mby9saWJyZS1yaXNjdi1kZXYK
91