[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / b5 / 03f6f14af8ab146732605b6fe68cb5be204cc4
1 Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
2 Envelope-to: publicinbox@libre-riscv.org
3 Delivery-date: Sat, 16 May 2020 16:00:36 +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 1jZyIl-0001RZ-5V; Sat, 16 May 2020 16:00:35 +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 1jZyIj-0001RN-PZ
11 for libre-riscv-dev@lists.libre-riscv.org; Sat, 16 May 2020 16:00:33 +0100
12 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=lkcl.net;
13 s=201607131;
14 h=Content-Type:To:Subject:Message-ID:Date:From:References:In-Reply-To:MIME-Version;
15 bh=Wlci3yt9WU/XrOieo2h6OglMfUE/5gu0CrDRDZ5IKYc=;
16 b=elUHgc6zwyBNhPWUjg8Duu//yzus99KjeR1yl4id7vCcwwaFs9EG0yOUtUM6x9++gmYY6kVS3tkXyOwMzNOinW+gvjrt8DGav1l1dlusVx7kPlcXCXxF9ed02rkrNVagZUZ6au09u39KjgxmQCuyuh3+upYuasLcQo3kClFRc8I=;
17 Received: from mail-lj1-f170.google.com ([209.85.208.170])
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 1jZyIj-0007EE-Ba
20 for libre-riscv-dev@lists.libre-riscv.org; Sat, 16 May 2020 15:00:33 +0000
21 Received: by mail-lj1-f170.google.com with SMTP id g1so5279780ljk.7
22 for <libre-riscv-dev@lists.libre-riscv.org>;
23 Sat, 16 May 2020 08:00:17 -0700 (PDT)
24 X-Gm-Message-State: AOAM532mZCtcjd4XL2sO1wpszv6aROI7OGpZHPdfR2IwzRFrkIdZdmPC
25 caborjejwMJEctX0iwQ+r4Mz66S4mDG1Vs9C4Rs=
26 X-Google-Smtp-Source: ABdhPJwz9w/xRPZiWcqu8HbJyT9DBH+NJaaiYJMsIZ8I4jCBiOrWeSkmNsqBVUYNZUKrYb7+VE0I4BDRi/BHzCzNJ+Q=
27 X-Received: by 2002:a2e:9081:: with SMTP id l1mr5025738ljg.81.1589641212151;
28 Sat, 16 May 2020 08:00:12 -0700 (PDT)
29 MIME-Version: 1.0
30 Received: by 2002:a05:6504:31aa:0:0:0:0 with HTTP; Sat, 16 May 2020 08:00:11
31 -0700 (PDT)
32 In-Reply-To: <13EDF987-9A19-4C96-89C2-6DB784CF2C96@gatech.edu>
33 References: <13EDF987-9A19-4C96-89C2-6DB784CF2C96@gatech.edu>
34 From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
35 Date: Sat, 16 May 2020 16:00:11 +0100
36 X-Gmail-Original-Message-ID: <CAPweEDzz-i--GwZironqwR7g-qKh3iRsJi0igSsG15HG2d63Fw@mail.gmail.com>
37 Message-ID: <CAPweEDzz-i--GwZironqwR7g-qKh3iRsJi0igSsG15HG2d63Fw@mail.gmail.com>
38 To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
39 X-Content-Filtered-By: Mailman/MimeDel 2.1.23
40 Subject: Re: [libre-riscv-dev] Scoreboard vs Tomasulo
41 X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
42 X-Mailman-Version: 2.1.23
43 Precedence: list
44 List-Id: Libre-RISCV General Development
45 <libre-riscv-dev.lists.libre-riscv.org>
46 List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>,
47 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
48 List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
49 List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
50 List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
51 List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>,
52 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
53 Reply-To: Libre-RISCV General Development
54 <libre-riscv-dev@lists.libre-riscv.org>
55 Content-Type: text/plain; charset="utf-8"
56 Content-Transfer-Encoding: base64
57 Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
58 Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
59
60 T24gU2F0dXJkYXksIE1heSAxNiwgMjAyMCwgWWVob3dzaHVhIDx5aW1tYW51ZWwzQGdhdGVjaC5l
61 ZHU+IHdyb3RlOgoKPiBUaGlzIHdlYnNpdGUgZ2l2ZXMgYW4gZXhjZWxsZW50IGNvbXBhcmlzb24K
62 Pgo+IGh0dHBzOi8vd3d3LmNzLnVtZC5lZHUvfm1lZXNoL2Ntc2M0MTEvd2Vic2l0ZS9wcm9qZWN0
63 cy9keW5hbWljL2ludHJvLmh0bWwKPiA8aHR0cHM6Ly93d3cuY3MudW1kLmVkdS9+bWVlc2gvY21z
64 YzQxMS93ZWJzaXRlL3Byb2plY3RzL2R5bmFtaWMvaW50cm8uaHRtbAo+ID4KCgphaCBnb29kIGZp
65 bmQuICBwYXJ0aWN1bGFybHkgYmVjYXVzZSwgbGlrZSBhbGwgQWNhZGVtaWMgbGl0ZXJhdHVyZSBv
66 biB0aGUKNjYwMCwgaXQgaXMgZmFjdHVhbGx5IHBhcnRpYWxseSBjb3JyZWN0IGJ1dCBhdCB0aGUg
67 c2FtZSB0aW1lIGRhbmdlcm91c2x5Cm1pc2xlYWRpbmcgYW5kIGZhY3R1YWxseSB3cm9uZy4gIHRo
68 aXMgZm9yIGV4YW1wbGUgaXMgd3Jvbmc6CgpIb3dldmVyLCB0aGUgc2NvcmVib2FyZCBpcyBsaW1p
69 dGVkIGluIHRoYXQgaXQgZG9lcyBub3QgaGFuZGxlIFdBUiBhbmQgV0FXCmhhemFyZHMgdmVyeSB3
70 ZWxsLgoKdGhlIG9yaWdpbmFsIDY2MDAgaGFuZGxlcyBXQVIgZXh0cmVtZWx5IHdlbGwsIG9ubHkg
71 c3RhbGxpbmcgb24gV2FXCmNvbmRpdGlvbiwgZGV0ZWN0aW9uIHdoaWNoIGRpZCBub3QgbWF0dGVy
72 IGdyZWF0bHkgYmVjYXVzZSB0aGUgcGlwZWxpbmVzCndlcmUgb25seSBhdCBtb3N0IDIgc3RhZ2Vz
73 IGxvbmcgYW55d2F5IChNaXRjaCBvbmx5IG5vdGljZWQgYWZ0ZXIgcmVyZWFkaW5nCmxhc3QgeWVh
74 ciB0aGF0IHRoZSBGUCBBREQgb2YgdGhlIDY2MDAgd2FzIDIgc3RhZ2UgcGlwZWxpbmVkLiAgbm8g
75 YWNhZGVtaWMKbGl0ZXJhdHVyZSBoYXMgYWNrbm93bGVkZ2VkIG9yIG5vdGljZWQgdGhpcykuCgp5
76 b3UgaGF2ZSB0byB1bmRlcnN0YW5kIHRoYXQgdGhlIG1ham9yaXR5IG9mIGRlc2lnbnMgYXQgdGhl
77 IHRpbWUgd2VyZSBhcm91bmQKMTAgdG8gMTIgY2xvY2tzIHBlciBpbnN0cnVjdGlvbi4gIHRoZSBD
78 REM2NjAwIGdvdCB0aGF0IGRvd24gdG8gRk9VUiBhbmQKY29uc2VxdWVudGx5IHJlcHJlc2VudGVk
79 IGEgMiB0byAzIGZvbGQgaW5jcmVhc2UgaW4gcGVyZm9ybWFuY2UuCgoKCj4gSW4gZ2VuZXJhbCwg
80 aXQgc2F5cyB0aGF0IFRvbWFzdWxvIGlzIGEgZGlzdHJpYnV0ZWQgc2NvcmVib2FyZC4KCgptbW0g
81 bm8uICB0aGUgUk9CLCB3aGljaCBpcyB0aGUga2V5IGNvbXBvbmVudCwgaXMgY2VudHJhbGlzZWQs
82 IGFuZCB0aGUgQ0RCCmlzIGEgY2VudHJhbCByZXNvdXJjZS4KCgoKPiBUaGUgYmlnZ2VzdCBkcmF3
83 YmFjayBvZiBUb21hc3VsbyBpcyB0aGUgY2VudHJhbCBkYXRhIGJ1cyBhcyB0aGUgbWVzc2FnaW5n
84 Cj4gc2NoZW1lLiBPbmUgY291bGQgdXNlIGEgbWVzaCBOT0MgYmV0d2VlbiBmdW5jdGlvbmFsIHVu
85 aXRzLgoKCmFoLCBub3QgcXVpdGUgdGhlIGJpZ2dlc3Q6IGFzIHlvdSBjb3JyZWN0bHkgc2F5LCBh
86 bGwgeW91IG5lZWQgaXMgbXVsdGlwbGUKQ0RCcyBhbmQgdGhhdCBwcm9ibGVtIGlzIHNvbHZlZC4K
87 Cm5vLCB0aGUgYmlnZ2VzdCBkcmF3IG9mIFRvbWFzdWxvIGlzIHRoYXQgdGhlIFJPQiAocmVvcmRl
88 ciBidWZmZXIpIG51bWJlcmluZwppcyBpbiAqYmluYXJ5KiwgYW5kIGJlYXIgaW4gbWluZCB0aGF0
89 IHRoZSBST0IgaXMgYSBDQU0sIHRoZSBsYXJnZXIgdGhhdApnZXRzIHRoZSBtb3JlIHBvd2VyIGl0
90 IHRha2VzLgoKbGV0IHVzIHNheSB3ZSBoYXZlIGEgMzIgZW50cnkgUk9CLCBsZXQgdXMgc2F5IHdl
91 IGhhdmUgNSBiaXRzIGZvciB0aGUgUk9CCkNBTSBrZXkuCgp0aGlzIG5vdCBvbmx5IG1lYW5zIHRo
92 YXQgd2hlbiB0cnlpbmcgdG8gcHV0IGEgcmVzdWx0IGludG8gdGhlIENBTSB3ZSBoYXZlCjV4MzIg
93 WE9SIGdhdGVzIHRvIGZpcmUgLSBvbiBldmVyeSBjeWNsZSAtIGlmIHdlIHdhbnQgMiBDb21tb24g
94 RGF0YSBCdXNlcyB3ZQpub3cgbmVlZCBET1VCTEUgdGhhdC4uLgoKLi4uICphbmQgd2UgbmVlZCBj
95 bGFzaCBkZXRlY3Rpb24qLgoKYnkgY29udHJhc3QsIDY2MDAgc2NvcmVib2FyZHMgaGF2ZSAqdW5h
96 cnkqIG51bWJlcmluZyBhbmQgY29uc2VxdWVudGx5IHRoZQpDQU0gaXMgZGVnZW5lcmF0ZSBhbmQg
97 YmVjb21lcyBhIHNpbmdsZSBBTkQgZ2F0ZSBhY3RpdmF0aW9uLgoKbm90IG9ubHkgdGhhdCBidXQg
98 aWYgeW91IHdpc2ggdG8gY2hlY2sgb3IgYWN0aXZhdGUgbW9yZSB0aGFuIG9uZSByZWdpc3Rlcgpz
99 aW11bHRhbmVvdXNseSB0aGVuIHRoYXQuLi4gaXMuLi4ganVzdC4uLiBtb3JlIHRoYW4gb25lIGNv
100 cnJlc3BvbmRpbmcgQU5ECmdhdGUgYWN0aXZhdGluZyBhdCB0aGUgQ0FNLgoKcGVyZmVjdGx5IHNp
101 bXBsZSwgdmVyeSBsaXR0bGUgcG93ZXIsIHBlcmZlY3QgZm9yIGRyb3BwaW5nIG11bHRpIGlzc3Vl
102 IG9uCnRvcC4KCgoKCj4gR2l2ZW4gdGhhdCB3ZSBoYXZlIHdlbGwgb3ZlciAxNSBmdW5jdGlvbmFs
103 IHVuaXRzLCBJIHdvdWxkIGhhdmUgdGhvdWdodCBhCj4gZGlzdHJpYnV0ZWQgc2NvcmVib2FyZCBp
104 bnN0ZWFkIG9mIGEgY2VudHJhbGl6ZWQgb25lIG1ha2VzIG1vcmUgc2Vuc2UuCgoKdGhlIGRvY3Vt
105 ZW50LCB3aGlsc3QgdXNlZnVsIGFzIGEgc3RhcnRpbmcgcG9pbnQsIGhhcyBtaXNsZWQgeW91IG9u
106 IHR3bwpjb3VudHMgKHNvIGZhcikKCnRoZSBrZXkgaXMgdGhhdCBiaW5hcnkgbnVtYmVyaW5nIHJl
107 cXVpcmVzIHBvd2VyIHN1Y2tpbmcgQ0FNcy4gIGhlbmNlIHdoeQp0aGUgNjYwMCBzY2hlbWUsIGF1
108 Z21lbnRlZCB0byBwcmVjaXNlLCBhbmQgZXZlbiB0aGUgb3JpZ2luYWwgNjYwMCBRIFRhYmxlCm51
109 bWJlcmluZyBoYXMgYmVlbiBjb252ZXJ0ZWQgZnJvbSBiaW5hcnkgdG8gdW5hcnkuCgpub3QgVG9t
110 YXN1bG8uCgphY3R1YWxseS4uLi4gaW4gNjYwMCwgdGhlIERNcyBhcmUgc3RpbGwgY2VudHJhbGlz
111 ZWQsIGl0IGlzIGhvd2V2ZXIgdGhlIGNhc2UKdGhhdCB0aGUgdW5hcnkgbnVtYmVyaW5nIHJlc3Vs
112 dHMgaW1wbGljaXRseSBpbiBvcHBvcnR1bml0aWVzIGZvcgpwYXJhbGxlbGlzbSAoc2VlIGJlbG93
113 KSBhbmQgY29uc2VxdWVudGx5IGNvdWxkIGJlIHRlcm1lZCAiZGlzdHJpYnV0ZWQiLgoKYWxzbywg
114 dGhlIHJvbGUgb2YgdGhlIEZ1bmN0aW9uIFVuaXRzLCB0aGUgR09SRC9SRVEgbGF0Y2hpbmcsIHRo
115 YXQgaXMgZG9uZQphcyBwYXJ0IG9mIHRoZSBjcml0aWNhbCBhY2tub3dsZWRnZW1lbnQgYW5kIGNv
116 bW11bmljYXRpb24gKndpdGgqIHRoZQpzY29yZWJvYXJkcywgYW5kIGlzIGRvbmUgdmVyeSBjbG9z
117 ZSB0byB0aGUgcGlwZWxpbmVzLCAqbm90KiBpbiB0aGUgRE1zCnRoZW1zZWx2ZXMsIHNvIGluIHRo
118 YXQgcmVnYXJkLCB5ZXMgaXQgaXMgImRpc3RyaWJ1dGVkIi4KCkZ1bmN0aW9uIFVuaXRzIGFyZSBl
119 cXVpdmFsZW50IHRvICJSZXNlcnZhdGlvbiBTdGF0aW9uIFJvd3MiIGZyb20gVG9tYXN1bG8KdGVy
120 bWlub2xvZ3kuICB0aGUgbXVsdGlwbGUgcm93cyBwZXIgVG9tYXN1bG8gUmVzZXJ2YXRpb24gU3Rh
121 dGlvbiAqYWxzbyoKcmVxdWlyZXMgdGhhdCB0aG9zZSBiZSBDQU1zIQoKeWV0IG1vcmUgcG93ZXIt
122 c3Vja2luZyEKCmdpdmVuIHRoYXQgSW50ZWwgcHJvY2Vzc29ycyB1c2UgVG9tYXN1bG8sIHdlIHN0
123 YXJ0IHRvIHNlZSB3aHkgSW50ZWwKcHJvY2Vzc29ycyBzdWNrIHNvIG11Y2ggcG93ZXIuCgoKPiBP
124 ZiBjb3Vyc2UsIEkgaGF2ZSBubyBudW1iZXJzIHRvIGJhY2sgdGhpcyB1cC4gQnV0IHRoZXNlIGFy
125 ZSBqdXN0IHNvbWUKPiB0aG91Z2h0cy4KPgo+Cj4gSSBrbm93IHdl4oCZcmUgdXNpbmcgYSByaW5n
126 L2NpcmN1bGFyIGJ1ZmZlciBmb3IgbWVzc2FnaW5nIGF0IHRoZSBtb21lbnQuCgoKeWVzIGZvciB0
127 aGUgZnV0dXJlIHZlcnNpb24uCgpmb3IgdGhlIHNpbXBsZSAxODBubSB2ZXJzaW9uIGl0IHdpbGwg
128 YmUgc2ltcGxlIGRpcmVjdCByZWdmaWxlIHBvcnQKYnJvYWRjYXN0IGJ1c2VzLCBjb25uZWN0ZWQg
129 b25lIHRvIG9uZSB3aXRoIHRoZSBjb3JyZXNwb25kaW5nIEZ1bmN0aW9uIFVuaXQKT3BlcmFuZCBp
130 bnB1dC4KCnRodXMsIEZVIG9wZXJhbmQgMSB3aWxsIGJlIGRpcmVjdGx5IGNvbm5lY3RlZCB0byBS
131 ZWdmaWxlIFBvcnQxIEJyb2FkY2FzdApCdXMuCgpGVSBvcGVyYW5kIDIgLSBpZiB0aGVyZSAqaXMq
132 IGFuIG9wZXJhbmQgMiAtIHdpbGwgY29ubmVjdCB0byBSZWdmaWxlIFBvcnQyCkJyb2FkY2FzdCBC
133 dXMuCgoqaWYgd2UgaGF2ZSB0aW1lKiB0aGVuIHdlIGNhbiBkcm9wIGluIHRoZSBjeWNsaWMgYnVm
134 ZmVycywgYW5kIHdoZW4gZGF0YQpjb21lcyBvdXQgb2YgUmVnZmlsZSBQb3J0MiBpdCBpcyBjeWNs
135 aWNhbGx5IHNoaWZ0ZWQgdG8gT3AuLi4gMSBvciBPcDMgb3IKd2hhdGV2ZXIgaXMgcmVxdWlyZWQu
136 CgoKCj4gR2l2ZW4gdGhhdCB3ZSBoYXZlIGhhcmQgZGVhZGxpbmVzIGFuZCBsaW1pdGVkIHJlc291
137 cmNlcywgd2UgY2FuIHN0aWNrIHdpdGgKPiB0aGlzLiBCdXQgdGhlc2UgYXJlIHF1ZXN0aW9ucyBJ
138 IGRvIHdvbmRlciBhYm91dCB0aGUgYW5zd2VyIHRvLiBJIHdvbmRlciBpZgo+IHRoZXJlIGFyZSBh
139 bnkgcGFwZXJzIHdoZXJlIHRoaXMgaGFzIGJlZW4gZXhwbG9yZWQgYXQgc3VmZmljaWVudCBkZXB0
140 aCB0bwo+IGRyYXcgY29uY2x1c2lvbnMuCgoKaSBlbmNvdW50ZXJlZCB3aGVuIGkgaW52ZXN0aWdh
141 dGVkIFRvbWFzdWxvIGEgd2F5IHRvIGRvIG11bHRpIGlzc3VlIGluIGFuCmFjYWRlbWljIHBhcGVy
142 LgoKdGhlIG1ldGhvZCwgd2hpY2ggaW52b2x2ZWQgc3RyYXRpZnlpbmcgdGhlIFJlb3JkZXIgQnVm
143 ZmVyIGludG8gNCBzZXBhcmF0ZQpzbGljZXMsIHdhcyBhd2Z1bC4KCnRoZSBiaW5hcnkgbnVtYmVy
144 aW5nIG9uIHRoZSBST0IgY2F1c2VzIG1hc3NpdmUgaGVhZGFjaGVzIGJlY2F1c2UgaXQKcmVxdWly
145 ZWQgc3BlY2lhbCBxdWV1ZXMgb2YgYmluYXJ5IFJPQiBpbmRpY2VzIHRvIHJlcHJlc2VudCB0aGUg
146 bXVsdGkgaXNzdWUKcmVxdWVzdHMuCgp3aGVuIGNvbnZlcnRlZCB0byB1bmFyeSwgbXVsdGlwbGUg
147 Yml0cyBtYXkgYmUgc2V0IHRvIGluZGljYXRlIFJFRzEgUkVHNQpSRUc3ICppbiBvbmUgY3ljbGUq
148 IG9uIHRoZSAqc2FtZSB3aXJlcyogYmVjYXVzZSBvbmUgd2lyZSBpcyBkZWRpY2F0ZWQgdG8KZWFj
149 aCByZWcuCgp0aGlzIGlzIHByZWNpc2VseSBhbmQgZXhhY3RseSB3aGF0IHlvdSBuZWVkIGZvciBt
150 dWx0aSBpc3N1ZSBhbmQgaXQgaXMgc28KbGF1Z2hhYmx5IHNpbXBsZS4KCmwgLgoKCi0tIAotLS0K
151 Y3Jvd2QtZnVuZGVkIGVjby1jb25zY2lvdXMgaGFyZHdhcmU6IGh0dHBzOi8vd3d3LmNyb3dkc3Vw
152 cGx5LmNvbS9lb21hNjgKX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f
153 X19fX18KbGlicmUtcmlzY3YtZGV2IG1haWxpbmcgbGlzdApsaWJyZS1yaXNjdi1kZXZAbGlzdHMu
154 bGlicmUtcmlzY3Yub3JnCmh0dHA6Ly9saXN0cy5saWJyZS1yaXNjdi5vcmcvbWFpbG1hbi9saXN0
155 aW5mby9saWJyZS1yaXNjdi1kZXYK
156