[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / 5c / df2aad62cc8f92bc1afcf23e46df563cfeaeeb
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 18:22:47 +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 1jbSQY-0007C5-Lp; Wed, 20 May 2020 18:22:46 +0100
8 Received: from lkcl.net ([217.147.94.29])
9 by libre-soc.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
10 (Exim 4.89) (envelope-from <lkcl@lkcl.net>) id 1jbSQW-0007Bz-Si
11 for libre-riscv-dev@lists.libre-riscv.org; Wed, 20 May 2020 18:22:44 +0100
12 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=lkcl.net;
13 s=201607131;
14 h=Content-Transfer-Encoding:Content-Type:To:Subject:Message-ID:Date:From:In-Reply-To:References:MIME-Version;
15 bh=lbN5AQt4I0NqPAQUCZI97Ykn3OZc4PxXqP7Qsw9I3qo=;
16 b=XUfeLC/LWT/0qKsDHbR9FWUur4RRFzAKoya6eVk36/fq4zuZ0fMDumMHFUyrnIZJJMHxRyJf+PtmmWRQ/iGfCIBNd34gUjakt+qpQlg+1DCGs3CWmCO6uQDp2ezX2Af3cHjMFj9O7NnEPseORORpwkVdT1OTz8WcDFXKQ15dlpU=;
17 Received: from mail-lf1-f50.google.com ([209.85.167.50])
18 by lkcl.net with esmtpsa (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
19 (Exim 4.84_2) (envelope-from <lkcl@lkcl.net>) id 1jbSQW-0008Aa-Iq
20 for libre-riscv-dev@lists.libre-riscv.org; Wed, 20 May 2020 17:22:44 +0000
21 Received: by mail-lf1-f50.google.com with SMTP id 202so2800899lfe.5
22 for <libre-riscv-dev@lists.libre-riscv.org>;
23 Wed, 20 May 2020 10:22:29 -0700 (PDT)
24 X-Gm-Message-State: AOAM532IkhcuczD6r8nakUGgZEhQCrAVeDYptFLlu0rEUzUGg+UuybRB
25 5enLr+MKbKHXycFf3gwtAyJpY6qxIZXhMEiMmi4=
26 X-Google-Smtp-Source: ABdhPJyPq7cbE9JzsLcTX7RU8S8wWN2V+2ADbD71GPS546aTTglzrK65Fv0AGVRu90RvQwGOBIr+KMeEqGdqyGc6RDQ=
27 X-Received: by 2002:a05:6512:62:: with SMTP id
28 i2mr3006038lfo.152.1589995343446;
29 Wed, 20 May 2020 10:22:23 -0700 (PDT)
30 MIME-Version: 1.0
31 References: <CAPweEDw862-S1=Au1YbsKNy0629pa56eShp+2o_Avd96Auz8mw@mail.gmail.com>
32 <9191058ea0912f2b508a6f73ea567e5f@f-cpu.org>
33 <CAPweEDzdkhVJuJ3_UqZTbd7i7vXJ5iiu3qz+LUBsFRJrzCcEmQ@mail.gmail.com>
34 <63e8b9ce54648590e2a6fc51bc2110dde7585f5e.camel@fibraservi.eu>
35 <CAPweEDx5zV3K3y=gjpArhpZ5VrKYL01=938EYA4xd0PjROqppg@mail.gmail.com>
36 <803285a5aa4bed5be9c8d4bc5855f49174742f33.camel@fibraservi.eu>
37 In-Reply-To: <803285a5aa4bed5be9c8d4bc5855f49174742f33.camel@fibraservi.eu>
38 From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
39 Date: Wed, 20 May 2020 18:22:11 +0100
40 X-Gmail-Original-Message-ID: <CAPweEDxRMyVdga44mJ6GL+jOHxAz=DrwqFJEB013Eh3rVqCb6A@mail.gmail.com>
41 Message-ID: <CAPweEDxRMyVdga44mJ6GL+jOHxAz=DrwqFJEB013Eh3rVqCb6A@mail.gmail.com>
42 To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
43 Subject: Re: [libre-riscv-dev] Debug port (was Re: minimum viable ASIC)
44 X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
45 X-Mailman-Version: 2.1.23
46 Precedence: list
47 List-Id: Libre-RISCV General Development
48 <libre-riscv-dev.lists.libre-riscv.org>
49 List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>,
50 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
51 List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
52 List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
53 List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
54 List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>,
55 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
56 Reply-To: Libre-RISCV General Development
57 <libre-riscv-dev@lists.libre-riscv.org>
58 Content-Type: text/plain; charset="utf-8"
59 Content-Transfer-Encoding: base64
60 Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
61 Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
62
63 T24gV2VkLCBNYXkgMjAsIDIwMjAgYXQgNTo0NCBQTSBTdGFmIFZlcmhhZWdlbiA8c3RhZkBmaWJy
64 YXNlcnZpLmV1PiB3cm90ZToKPgo+IEx1a2UgS2VubmV0aCBDYXNzb24gTGVpZ2h0b24gc2NocmVl
65 ZiBvcCB2ciAwOC0wNS0yMDIwIG9tIDIzOjE5IFsrMDEwMF06Cj4gPiAtLS1jcm93ZC1mdW5kZWQg
66 ZWNvLWNvbnNjaW91cyBoYXJkd2FyZTogaHR0cHM6Ly93d3cuY3Jvd2RzdXBwbHkuY29tL2VvbWE2
67 OAo+ID4KPiA+IE9uIEZyaSwgTWF5IDgsIDIwMjAgYXQgNjoyMyBQTSBTdGFmIFZlcmhhZWdlbiA8
68 c3RhZkBmaWJyYXNlcnZpLmV1PiB3cm90ZToKPiA+Cj4gPiBhaC4gIGFzIGEgc29mdHdhcmUgZW5n
69 aW5lZXIsIHRoZSBwcmFjdGljZSBvZiB1c2luZyB3aWxkY2FyZCBpbXBvcnRzIGlzYW4gZXh0cmVt
70 ZWx5IGJhZCBvbmUuICBpIHN0cm9uZ2x5IGFkdm9jYXRlICpub3QqIGdldHRpbmcgaW50byB0aGVo
71 YWJpdCBvZiBkb2luZyAiZnJvbSBubWlnZW4gaW1wb3J0ICoiIGV2ZXJ5d2hlcmUgLSBpdCB3aWxs
72 IG1ha2UgeW91cmxpZmUgLSBhbmQgb3RoZXIgdXNlcnMgbGl2ZXMgLSBhYnNvbHV0ZSBoZWxsIHdo
73 ZW4gaXQgY29tZXMgdG8gdHJ5aW5ndG8gdHJhY2sgYW5kIGRlYnVnIGNvZGUuCj4gPiBtaW5lcnZh
74 IGhhcyBhIEpUQUcgaW50ZXJmYWNlIGFzIHdlbGwuICBpIGNvcnJlY3RlZCB0aGUgcHJhY3RpY2Ug
75 b2Z1c2luZyAiaW1wb3J0ICoiIGluIHRoaXMgb25lCj4KPiBXb3VsZCAnaW1wb3J0IG5taWdlbiBh
76 cyBubScgd29yayBmb3IgeW91PwoKYW5kIHRoZW4gaGF2ZSBldmVyeXRoaW5nIGFzICJ4ID0gbm0u
77 U2lnbmFsKCkuLi4uIiBhbmQgc28gb24/ICB5ZXMgdGhhdAp3b3VsZCBiZSByZWFsbHkgZ29vZC4g
78 IGkgYWN0dWFsbHkgd29ya2VkIGZvciBhIGNvbXBhbnkgdGhhdCBtYWRlIGl0Cm1hbmRhdG9yeSB0
79 byB1c2UgdGhlIGZ1bGwgZXhwbGljaXQgbW9kdWxlIG5hbWUgKGFuZCB1c2VkIHRoaXMgdHJpY2sg
80 dG8KZ2V0IHJvdW5kIHRoZSBpc3N1ZSBvZiByaWRpY3Vsb3VzbHkgbG9uZyBuYW1lcykuCgp0aGV5
81 IHJlcXVpcmVkOgoKaW1wb3J0IG5taWdlbgp4ID0gbm1pZ2VuLlNpZ25hbCgpCi4uLgoKaG93ZXZl
82 ciBpdCBnZXRzIHZlcnksIHZlcnkgdGVkaW91cy4KCmltcG9ydCBubWlnZW4gYXMgbm0KeCA9IG5t
83 LlNpZ25hbCgpCgppcyBhY3R1YWxseSBhIHJlYWxseSBnb29kIGlkZWEuICBzYXZlcyBzcGFjZSwg
84 ZXhwbGljaXRseSBzYXlzIHdoZXJlCnRoZSAidGhpbmciIChTaWduYWwgZXRjLikgY29tZSBmcm9t
85 LgoKCj4gSSBkaWQgbm90IHRvdWNoIGNvZGUgZm9yIGEgZmV3IG1vbnRocyBhbmQgaW4gdGhlIG1l
86 YW4gdGltZSBJIGRvIHVzZSBhIG1vcmUgUEVQIGNvbXBsaWFudCBjb2RlIHN0eWxlLgo+IEJ1dCBJ
87 IGFtIGFubm95ZWQgYnkgdGhlIGluZGl2aWR1YWwgbGlzdCBvZiB0aGluZ3MgdG8gaW1wb3J0LgoK
88 U3RhZjogdHJ1c3QgbWUgb24gdGhpcyBvbmUuICB0aGUgaGVsbCBpdCBjcmVhdGVzIGZvciBwZW9w
89 bGUgb3RoZXIgdGhhbgp5b3Vyc2VsZiBpcyBiZXlvbmQgbWVhc3VyZS4gIHRoZSBpbXBvcnRzIHNl
90 cnZlIGEgc2Vjb25kYXJ5IGNyaXRpY2FsbHkKaW1wb3J0YW50IHB1cnBvc2Ugb2YgZG9jdW1lbnRp
91 bmcgX3doZXJlXyBhIGdpdmVuIHZhcmlhYmxlIChjbGFzcykgbWF5CmJlIGxvY2F0ZWQuCgoiaW1w
92 b3J0ICoiIGNvbXBsZXRlbHkgYW5kIHV0dGVybHkgb2JsaXRlcmF0ZXMgdGhhdCB0cmFpbCwgbWFr
93 aW5nCm1haW50ZW5hbmNlIGFuZCBjb2RlLXJlYWRhYmlsaXR5IGJ5IG90aGVyIHBlb3BsZSBhbiBh
94 YnNvbHV0ZQpuaWdodG1hcmUuCgo+IEZvciBubWlnZW4gb3IgSHVycmljYW5lIHRoZXJlIGlzIHR5
95 cGljYWxseSBhIGZldyBsaW5lcyBvZiB0aGVzZSBpbmNsdWRlcy4KCnlvdSBxdWlja2x5IGdldCB1
96 c2VkIHRvIGN1dC9wYXN0aW5nIGZyb20gb3RoZXIgZmlsZXMuCgo+IFdoZW4gSSBjaGFuZ2UgZm9y
97 IGV4YW1wbGUgYSBQYWQgdG8gYSBSZWN0aWxpbmVhciBJIG1heSBoYXZlIHRvIHVwZGF0ZSB0aGUg
98 aW1wb3J0IGxpc3QuCgphbmQgb3RoZXIgcGVvcGxlIHdoZW4gdGhleSByZWFkIHRoYXQgY29kZSB3
99 aWxsIGJlIGFibGUgdG8gdHJhY2sgdGhhdApjaGFuZ2UuICBpIGhhdmUgYWJzb2x1dGVseSBubyBp
100 ZGVhIHdoYXQgUGFkIGlzLCBub3IgUmVjdGlsaW5lYXIsIGZvcgpleGFtcGxlLgoKd2hlcmUgc2hv
101 dWxkIGkgc3RhcnQgbG9va2luZyBmb3IgaXQ/Cgp3aGljaCBtb2R1bGU/Cgp3aGljaCAqcGFja2Fn
102 ZSogZXZlbj8KCmFyZSB0aGV5IGluLi4uIG5taWdlbj8KCmFyZSB0aGV5IGluIEh1cnJpY2FuZT8K
103 CmFyZSB0aGV5IGluIHNvbWV0aGluZyBlbHNlIHRoYXQgaGFzIGJlZW4gd2lsZC1jYXJkIGltcG9y
104 dGVkPwoKaSAqbGl0ZXJhbGx5KiBjYW5ub3QgdGVsbCwgYW5kIHRoYXQgbWFrZXMgZXZlcnlvbmUn
105 cyBsaWZlIGFic29sdXRlCmhlbGwuICB3ZSAtIGFzIHVzZXJzIG9mIHRoYXQgY29kZSAtICpsaXRl
106 cmFsbHkqIGhhdmUgdG8gZG8gImdyZXAgLXIKUGFkIiBpbiBNVUxUSVBMRSBzb3VyY2UgY29kZSBk
107 aXJlY3RvcmllcyAtIGZvciBjb21wbGV0ZWx5IGRpZmZlcmVudApwYWNrYWdlcyAoUVRZIDIgaW4g
108 dGhpcyBvbmUgZXhhbXBsZSBhbG9uZSkgLSB0byB0cmFjayBkb3duIHdoZXJlIHRoZQpkZWZpbml0
109 aW9uIG9mICJQYWQiIGFuZCAiUmVjdGlsaW5lYXIiIGV4aXN0IQoKCj4gSSBkb24ndCBzZWUgdmFs
110 dWUgYWRkIG9mIHRoaXMgYW5kIGl0IGFubm95cyBtZSBhIGxvdC4KCnRoaXMgaXMgZG93biB0byBp
111 bmV4cGVyaWVuY2Ugd2l0aCBjb2xsYWJvcmF0aXZlIHB5dGhvbiBkZXZlbG9wbWVudC4gIGkKc2F5
112 IHRoYXQgd2l0aCBubyBkaXNyZXNwZWN0OiBpdCdzIGp1c3QgdGhhdCBpJ3ZlIHVzZWQgcHl0aG9u
113 IGZvciAyMAp5ZWFycyBhbmQgaGF2ZSBzZWVuIGEgbG90LgoKPiBTbyBJIGFtIHRoaW5raW5nIG9m
114 IHN3aXRjaGluZyB0byAnaW1wb3J0IEh1cnJpY2FuZSBhcyBodXInIGFuZCAnaW1wb3J0IG5taWdl
115 biBhcyBubScKCj4gVG8gbWUgdGhlIG9ubHkgdmFsaWQgcmVhc29uIGZvciBub3QgdXNpbmcgd2ls
116 ZCBjYXJkcyBpcyB0aGF0IGEgbGF0ZXIgd2lsZAo+IGNhcmQgaW1wb3J0IG1heSByZXBsYWNlIHNv
117 bWV0aGluZyB5b3UgZGlkIGltcG9ydCBiZWZvcmU7Cgp0d28gdGhpbmdzIChib3RoIGVxdWFsbHkg
118 YXMgaW1wb3J0YW50KToKCjEuIHRoYXQgaXMgZG93biB0byBpbmV4cGVyaWVuY2UgZnJvbSBkZXZl
119 bG9waW5nIHB5dGhvbi4gICpub2JvZHkqIHdobwppcyBhbiBleHBlcmllbmNlZCBweXRob24gZGV2
120 ZWxvcGVyIHVzZXMgd2lsZGNhcmQgaW1wb3J0cyBleGNlcHQgaW4KdmVyeSwgdmVyeSBzcGVjaWFs
121 IG1pdGlnYXRpbmcgY2FzZXMKCjIuIHlvdSBhcmUgYWJzb2x1dGVseSBjb3JyZWN0OiB0aGlzIGlz
122 ICphbm90aGVyKiBpbXBvcnRhbnQgcmVhc29uLgoKdGhlcmUgYXJlIG1hbnkgbW9yZS4KCj4gdGhp
123 cyBpcyBhdm9pZGVkIGJ5IG5hbWVzcGFjaW5nIHRoZSBpbXBvcnQgd2l0aCAnaW1wb3J0IC4uLiBh
124 cyAuLi4nLgoKeWVzLCBpdCBpcyBhIGdvb2QgdHJpY2suCgo+ID4gYWxzbyBwcm92aWRlZCBhIHdp
125 c2hib25lIG1hc3RlciBpbnRlcmZhY2U6Cj4gPiBodHRwczovL2dpdC5saWJyZS1zb2Mub3JnLz9w
126 PXNvYy5naXQ7YT1ibG9iO2Y9c3JjL3NvYy9taW5lcnZhL3VuaXRzL2RlYnVnL3dibWFzdGVyLnB5
127 O2g9ZGIwMmFmOTViNGViM2VmOGFjMjViMzQ4ZjNhYmFhMmJjYmU3ZDk2ZjtoYj1hNTRhZGNiNjVi
128 YWQzN2IzOThiMTFlMzNhODI0YzdkMDhjNWZlNTA5Cj4KPiBUaGF0IGNvZGUgc2VlbXMgdG8gZm9j
129 dXMgb24gdGhlIGRlYnVnZ2luZyBwcm90b2NvbCBvdmVyIHRoZSBKVEFHIGludGVyZmFjZSB0aGUg
130 bG93ZXIgbGV2ZWwgcGFydCBzZWVtcyB0byBiZSBtaXNzaW5nLkluIGRlYnVnL3RvcC5weTouLi4K
131 PiAjIEZJWE1FOiBmaWd1cmUgb3V0IHdoZXJlIEpUQUdUYXAgaXMKPiAjIGZyb20ganRhZ3RhcCBp
132 bXBvcnQgSlRBR1RhcAo+Cj4KPiBjbGFzcyBKVEFHVGFwOgo+ICAgICBkZWYgX19pbml0X18oc2Vs
133 Zik6Cj4gICAgICAgICByYWlzZSBOb3RJbXBsZW1lbnRlZEVycm9yKAo+ICAgICAgICAgICAgICJq
134 dGFndGFwIHBhY2thZ2Ugbm90IGZvdW5kOiBmaWd1cmUgb3V0IHdoZXJlIEpUQUdUYXAgaXMiKQo+
135 IC4uLgo+Cj4gTXkgSlRBRyBpbnRlcmZhY2UgZG9lcyBhY3R1YWxseSB0aGUgbG93IGxldmVsIHBh
136 cnQsCgphaGggdGhhdCdzIHZlcnkgaW50ZXJlc3RpbmcgdG8gbm90ZS4gIGFoIHRoYXQncyB0aGVu
137 IGEgcmVhbGx5IGdvb2QKY29tYmluYXRpb24sIG9mIHRoZSB0d28uICBvbmUgaXMgdGhlIGV4dGVy
138 bmFsIGludGVyZmFjZSwgdGhlIG90aGVyCm1vcmUgaW50ZXJuYWwuCgo+IHRoZSBwcm90b2NvbCBo
139 YXMgdG8gYmUgZG9uZSBieSB0aGUgdXNlciBvbiB0b3Agb2YgaXQuIEkgZG8gdGhpbmsgSSBoYXZl
140 IGEgZmxleGlibGUgd2F5IG9mIGFkZGluZyBleHRyYSBzaGlmdCByZWdpc3RlcnMgYW5kIGp0YWcg
141 Y29tbWFuZHMuIEkgYWxzbyBkbyBwcm92aWRlIGJvdW5kYXJ5IHNjYW4gZm9yIHRoZSBJTyBwaW5z
142 IHdoaWNoIHNob3VsZCBtYWtlIFBDQiB0ZXN0aW5nIG11Y2ggZWFzaWVyIChCVFcsIHRoaXMgd2Fz
143 IGFjdHVhbGx5IHRoZSBvcmlnaW5hbCB1c2UgY2FzZSBmb3IgSlRBRykuCgphaCwgcmVhbGx5IGFw
144 cHJlY2lhdGVkLgoKbC4KCl9fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f
145 X19fX19fCmxpYnJlLXJpc2N2LWRldiBtYWlsaW5nIGxpc3QKbGlicmUtcmlzY3YtZGV2QGxpc3Rz
146 LmxpYnJlLXJpc2N2Lm9yZwpodHRwOi8vbGlzdHMubGlicmUtcmlzY3Yub3JnL21haWxtYW4vbGlz
147 dGluZm8vbGlicmUtcmlzY3YtZGV2Cg==
148