[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / 5b / c7e11cae49bc3c22b593e80c3897e615471057
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:52:35 +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 1jZz74-0002R6-4b; Sat, 16 May 2020 16:52:34 +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 1jZz72-0002Qz-Jz
11 for libre-riscv-dev@lists.libre-riscv.org; Sat, 16 May 2020 16:52:32 +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=ZmLQEs2zAErXaC35Q2RMHDhA+hKvNJEwdjnuGwLbUQI=;
16 b=ZjpD8UNY6s0nSX7RK2uaLgVogMUiqHvBSU52HsplHmH5awOgozjWpe2colx0LY6dAttmdta4HNbnhBlnXQusWOpKBzBx/tFB1EjVvRk0sskl/lwg3stt7KlFBy+i0xs9gt7gxIi7wrBasMnXNStQxRWRKzZZoBq/vsC3T/Fsbkc=;
17 Received: from mail-lf1-f45.google.com ([209.85.167.45])
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 1jZz72-0007Ic-73
20 for libre-riscv-dev@lists.libre-riscv.org; Sat, 16 May 2020 15:52:32 +0000
21 Received: by mail-lf1-f45.google.com with SMTP id c12so879152lfc.10
22 for <libre-riscv-dev@lists.libre-riscv.org>;
23 Sat, 16 May 2020 08:52:16 -0700 (PDT)
24 X-Gm-Message-State: AOAM5324Zhy61hKZxESCROMFxMpX8ejhncUoy8q5OdkbgeppHyP07iQZ
25 oExOuiS7AN4+nktOfJf1aKMV/SSxnBlCmnq3mqA=
26 X-Google-Smtp-Source: ABdhPJyLoPJV0E+zB7C4Vhkj/wCMlnRRI64e6nTTRR0hOgxJJFfLccpIUeiEY12wbIhaBPXeF81KXAYHkoHCWo4P4jo=
27 X-Received: by 2002:a05:6512:31c5:: with SMTP id
28 j5mr5965466lfe.26.1589644331305;
29 Sat, 16 May 2020 08:52:11 -0700 (PDT)
30 MIME-Version: 1.0
31 Received: by 2002:a05:6504:31aa:0:0:0:0 with HTTP; Sat, 16 May 2020 08:52:10
32 -0700 (PDT)
33 In-Reply-To: <CAPweEDyw+LSW2S4sKWk-V24NSHYe2qqWO+KFqikQ34Q1Guhaig@mail.gmail.com>
34 References: <13EDF987-9A19-4C96-89C2-6DB784CF2C96@gatech.edu>
35 <CAPweEDyDcmAJbJx+PKkL8MotPMNyHyFOEtuNOKP+V2PmmY5HvA@mail.gmail.com>
36 <CAPweEDyw+LSW2S4sKWk-V24NSHYe2qqWO+KFqikQ34Q1Guhaig@mail.gmail.com>
37 From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
38 Date: Sat, 16 May 2020 16:52:10 +0100
39 X-Gmail-Original-Message-ID: <CAPweEDweXSC5c_ROQ8a3Y4hQMaJYmD_jAriadcZk9PRrkjOXvA@mail.gmail.com>
40 Message-ID: <CAPweEDweXSC5c_ROQ8a3Y4hQMaJYmD_jAriadcZk9PRrkjOXvA@mail.gmail.com>
41 To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
42 X-Content-Filtered-By: Mailman/MimeDel 2.1.23
43 Subject: Re: [libre-riscv-dev] Scoreboard vs Tomasulo
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 aHR0cHM6Ly93d3cuY3MudW1kLmVkdS9+bWVlc2gvY21zYzQxMS93ZWJzaXRlL3Byb2plY3RzL2R5
64 bmFtaWMvbW9kZXJuLmh0bWwKCnRoaXMgZW50aXJlIHNlY3Rpb24gaXMgbWlzbGVhZGluZyBpbiBz
65 ZXZlcmFsIHdheXMuIGl0J3Mgbm90IHdyb25nIHBlciBzZSwKaXQncyBqdXN0IG5vdCB0aGUgb25s
66 eSBzb2x1dGlvbi4KCnRoZSAqb3RoZXIqIHNvbHV0aW9uIGlzIHRvIGhhdmUgInByZWNpc2Ugc2hh
67 ZG93aW5nIi4KCnRoaXMgaXMgYSBzeXN0ZW0gKGRlc2NyaWJlZCBhdCB0aGUgZW5kIG9mIE1pdGNo
68 IDJuZCBjaGFwdGVyKSB3aGljaCBhbGxvd3MKcmVzdWx0ICpjb21wdXRhdGlvbiogdG8gcnVuIGFo
69 ZWFkIGJ1dCB3aGVyZSByZXN1bHQgKmNvbW1pdCogaXMgcHJldmVudGVkCmFuZCBwcm9oaWJpdGVk
70 LgoKKHRoZSBnYXRlIGNvdW50IHJlcXVpcmVkIHRvIGRvIHNvIGlzIGV4dHJlbWVseSBsb3cuKQoK
71 dGhpcyBvbiB0aGUgZmFjZSBvZiBpdCB3b3VsZCBzZWVtIHRvIHN0b3AgRlVzIGZyb20gcHJvZ3Jl
72 c3NpbmcgYmVjYXVzZSB0aGV5CmNhbm5vdCBkbyBzbyB1bnRpbCB0aGV5IHJlY2VpdmUgdGhlaXIg
73 b3BlcmFuZHMuLi4gYW5kIHVtIGhvdyBjb3VsZCB0aGV5IGRvCnRoYXQgaWYgd3JpdGluZyB0byB0
74 aGUgcmVnZmlsZSBpcyBwcm9oaWJpdGVkPwoKdGhlIGFuc3dlciBpcyB2ZXJ5IHNpbXBsZTogdGhh
75 dCBpcyB3aGF0IE9wZXJhbmQgRm9yd2FyZGluZyBpcyBmb3IsIGFrYQoiQ29tbW9uIERhdGEgQnVz
76 KGVzKSIuCgpzbyBieSBwcmV2ZW50aW5nIHdyaXRlIGNvbW1pdCwgd2UgY2FuIHJ1biBhaGVhZCBm
77 b3IgYSBjb25zaWRlcmFibGUgdGltZSwgbm8Kc3RhbGxpbmcgYXQgYWxsLgoKd2hlbiB0aGUgYnJh
78 bmNoIHByZWRpY3Rpb24gcmVzb2x2ZXMsIHdlIHRoZW4gZWl0aGVyOgoKKiByZWxlYXNlIHRoZSBz
79 aGFkb3cgd2hpY2ggYWxsb3dzIGEgdG9uIG9mIHJlc3VsdHMgdG8gYmVnaW4gY29tbWl0dGluZy4K
80 b3JkZXIgaXMgbm90IHN0cmljdGx5IHJlbGV2YW50IGV4Y2VwdCBhcyBwcmVzZXJ2ZWQgYnkgdGhl
81 IGhhemFyZCBkZXRlY3Rpb24KCiogY2FsbCB0aGUgImdvIGRpZSIgbGluZSB3aGljaCBkcm9wcyBh
82 YnNvbHV0ZWx5IGV2ZXJ5IGRvd25zdHJlYW0gcmVzdWx0IGFuZApwYXJ0aWFsIGNvbXB1dGF0aW9u
83 IHVuZGVyd2F5IG9uIHRoZSBmbG9vci4gIHRoZSBQQyB0aGVuIGlzc3VlcyBvcHMgZG93biB0aGUK
84 YWx0ZXJuYXRpdmUgcGF0aC4KCihpIGRpZCBhY3R1YWxseSB0cnkgZHVhbCBwYXRoIGV4ZWN1dGlv
85 bjogdGhlb3JldGljYWxseSBvdXIgZW5naW5lIGNhbiBkbwppdCwgaSBqdXN0IGNvdWxkIG5vdCBn
86 ZXQgaXQgdG8gd29yayBsYXN0IHllYXIsIGl0IHdhcyB0YWtpbmcgdG9vIGxvbmcgdG8KZGVidWcs
87 IGFuZCBpIGhhZCB0byBmb2N1cyBvbiBvdGhlciB0aGluZ3MpLgoKCnRoZSB0aGluZyB0aGF0IGlz
88 IHBhcnRpY3VsYXJseSBtaXNsZWFkaW5nIGFib3V0IHRoaXMgcGFydGljdWxhciBzZWN0aW9uIGlz
89 CnRoYXQgaXQgaW5zdGlsbHMgaW4gdGhlIHJlYWRlcidzIG1pbmQgdGhlIGZhbHNlIGltcHJlc3Np
90 b24gdGhhdCB0aGVyZSBpcyBhCm1hbmRhdG9yeSBjb3JyZWxhdGlvbiBiZXR3ZWVuIHNwZWN1bGF0
91 aXZlIGV4ZWN1dGlvbiBhbmQgb3BlcmFuZCBvcmRlcgpjb21taXR0aW5nLgoKdGhpcyBpcyBqdXN0
92 IGZhbHNlLgoKaWYgdGhlIGNvbW1pdCBjYW4gYmUgc3RhbGxlZCB1bnRpbCBpdCBpcyBndWFyYW50
93 ZWVkIGtub3duIHRoYXQsIGFmdGVyIHRoYXQKcG9pbnQgaXQgaXMgcGVyZmVjdGx5ICpzYWZlKiB0
94 byBjb21taXQgKHRoZSBvcGVyYXRpb24gaXMgMTAwJSBnb2luZyB0bwpzdWNjZWVkKQoKICAgIEFO
95 RAoKaWYgdGhlcmUgYXJlIG5vIGhhemFyZHMgcmVtYWluaW5nCgogICBUSEVOCgp3aG8gX2NhcmVz
96 XyB3aGF0IG9yZGVyIHJlc3VsdHMgYXJlIGNvbW1pdHRlZD8gYW5zd2VyOiBub2JvZHkuCgoKCnNv
97 Li4uIHVzZWZ1bCBpbmFzbXVjaCBhcyBpdCBpcyB3cml0dGVuIGJ5IGFuIGFjYWRlbWljIGFuZCB0
98 aHVzIGlzIHJlYWxseQpyZWFkYWJsZS4KCnNhZGx5IHRob3VnaCBpdCBjb250YWlucyB0aGUgdXN1
99 YWwgZ2xhcmluZyBlcnJvcnMsIG1pc3VuZGVyc3RhbmRpbmdzIGFuZApvbWlzc2lvbnMgd2hpY2gg
100 YXJlIHdpZGVseSBwZXJ2YXNpdmUgYW5kIGNvbW1vbiB0aHJvdWdob3V0IHRoZSAqZW50aXJlKgph
101 Y2FkZW1pYyB3b3JsZCwgZXZlbiBieSB0aG9zZSB3aG8gY2xhaW0gdG8gaGF2ZSBzdHVkaWVkIDY2
102 MDAgc2NvcmVib2FyZHMsCmV2ZW4gYnkgdGhvc2Ugd2hvIGNsYWltIHRvIGJlIGV4cGVydHMgb24g
103 UklTQyBkZXNpZ24uCgpmb3IgdGhlIG1vc3QgcGFydCB0aGF0IGludm9sdmVzIGN1cnNvcnkgcmVh
104 ZGluZyB0aGUgcGF0ZW50IG9uIDY2MDAgUQpUYWJsZXMsICpub3QqIHN0dWR5aW5nIFRob3JudG9u
105 J3MgYm9vayBpbiBncmVhdCBkZXB0aCBhbmQgdGFraW5nIHRoZSB0aW1lCnRvIHRyYW5zbGF0ZSB0
106 aGUgKG5vdyBhcmNoYWljKSB0cmFuc2lzdG9yIGxldmVsIGRpYWdyYW1zIGludG8gbW9kZXJuIElF
107 RUUKc3RhbmRhcmQgZWxlY3Ryb25pY3Mgc3ltYm9scyAtIHNvbWV0aGluZyB0aGF0IE1pdGNoIHdl
108 bnQgdG8gYSBsb3Qgb2YKdHJvdWJsZSB0byBkby4KCmkgdHJ1c3QgdGhhdCB0aGlzIGdpdmVzIHlv
109 dSBzb21ldGhpbmcgb2YgYW4gZXllb3BlbmVyIGludG8gdGhlIGV4dGVudCBvZgp0aGUgbWlzYXBw
110 cmVoZW5zaW9ucyB0aGF0IHRoZSBBY2FkZW1pYyBjb21tdW5pdHkgaXMgdW5kZXIsIHJlZ2FyZGlu
111 ZyBvdXQgb2YKb3JkZXIgZW5naW5lIGRlc2lnbi4KCnRoZSBjbG9zZXN0IHdvcmtpbmcgaW1wbGVt
112 ZW50YXRpb24gaSBoYXZlIHNlZW4gc2ltaWxhciB0byB3aGF0IHdlIGFyZSBkb2luZwppcyBhIGNv
113 bnZlcnNpb24gb2YgYW4gZXhpc3RpbmcgUlYzMiBkZXNpZ24gdG8gc3VwZXJzY2FsYXIgYW5kIG11
114 bHRpIGlzc3VlCmJ5IGEgY2hpbmVzZSBndXkgd2hvIGhhcyBub3QgcmV2ZWFsZWQgaGlzIG5hbWUs
115 IG9ubGluZS4KCmhlIGFsc28gZGlkIG11bHRpLWJpdCB1bmFyeSB0cmFuc2l0aXZlIHJlbGF0aW9u
116 c2hpcHMgYW5kIGRlcGVuZGVuY3kKdHJhY2tpbmcgaW4gZXhhY3RseSB0aGUgc2FtZSB3YXkgdGhh
117 dCB3ZSB3aWxsLCBoYXZpbmcgcmUtZGVyaXZlZCA2NjAwCnNjb3JlYm9hcmRzIHdpdGggbm8gcmVm
118 ZXJlbmNlIHRvIGFueSBhY2FkZW1pYyBsaXRlcmF0dXJlLgoKaG93ZXZlciBoZSBkaWQgbm90IGF0
119 IHRoZSBzYW1lIHRpbWUgaW5jcmVhc2UgbG9hZCBzdG9yZSBkYXRhIGJhbmR3aWR0aCwgYW5kCm9u
120 IHRvcCBvZiBSVjMySSBpdCBpcyBhIGhlbGwgb2YgYSBsb3Qgb2YgZXh0cmEgd29yayB0byBicmlu
121 ZyB1cCB0byB3aGVyZSB3ZQpjYW4gdXNlIGl0Li4uIGFuZCBpdCdzIGFsbCBpbiB2ZXJpbG9nLgoK
122 bC4KCgoKCi0tIAotLS0KY3Jvd2QtZnVuZGVkIGVjby1jb25zY2lvdXMgaGFyZHdhcmU6IGh0dHBz
123 Oi8vd3d3LmNyb3dkc3VwcGx5LmNvbS9lb21hNjgKX19fX19fX19fX19fX19fX19fX19fX19fX19f
124 X19fX19fX19fX19fX19fX19fX18KbGlicmUtcmlzY3YtZGV2IG1haWxpbmcgbGlzdApsaWJyZS1y
125 aXNjdi1kZXZAbGlzdHMubGlicmUtcmlzY3Yub3JnCmh0dHA6Ly9saXN0cy5saWJyZS1yaXNjdi5v
126 cmcvbWFpbG1hbi9saXN0aW5mby9saWJyZS1yaXNjdi1kZXYK
127