[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / e1 / f08cd7fceafdc0c6d407c2c952ff6988e953d8
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 18:33:30 +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 1ja0gj-0003aO-UZ; Sat, 16 May 2020 18:33:29 +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 1ja0gi-0003aI-0z
11 for libre-riscv-dev@lists.libre-riscv.org; Sat, 16 May 2020 18:33:28 +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=B0Mks1zsmd7volcoS9h1our36FXdI41N23kemE4ydnA=;
16 b=aW1MZ7s9PISjr+kFp33aEC9DYDJGEk7aIShlI/FsoqIPctzZ6LL8LlkVrHQkkXkKoBHQ1OcnLZRqagOaq4ciRJCV0IKU9/zFbJvcTy91NJP34NLnfW4IqBcMGiu52mqqcNHzwdEVb0eH9yXoSC7/XpOQeoz9bNqRLlOKj68B3yM=;
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 1ja0gh-0007OZ-Ma
20 for libre-riscv-dev@lists.libre-riscv.org; Sat, 16 May 2020 17:33:27 +0000
21 Received: by mail-lf1-f50.google.com with SMTP id 82so4503513lfh.2
22 for <libre-riscv-dev@lists.libre-riscv.org>;
23 Sat, 16 May 2020 10:33:12 -0700 (PDT)
24 X-Gm-Message-State: AOAM530t+doijLnU7r9Y7PtSJ7Nyi2WxdTFiKpiHokLF7Wzlb7gy+bDn
25 3Gr47fttZACkfIROQwxQGVcSpbPMVfH3ACIMgAM=
26 X-Google-Smtp-Source: ABdhPJyjrN+pH+jVwGLV6roAwg9xaoX7PmyRjE8cV6AHT/YyyPW/efGozq06voB16QVE1h87YQIOTOnb5Nr4mjjcNjI=
27 X-Received: by 2002:ac2:47f4:: with SMTP id b20mr6099052lfp.88.1589650386619;
28 Sat, 16 May 2020 10:33:06 -0700 (PDT)
29 MIME-Version: 1.0
30 Received: by 2002:a05:6504:31aa:0:0:0:0 with HTTP; Sat, 16 May 2020 10:33:05
31 -0700 (PDT)
32 In-Reply-To: <25AC8A2E-D48F-439F-AF9D-0EB3DC08D7CC@gatech.edu>
33 References: <13EDF987-9A19-4C96-89C2-6DB784CF2C96@gatech.edu>
34 <CAPweEDyDcmAJbJx+PKkL8MotPMNyHyFOEtuNOKP+V2PmmY5HvA@mail.gmail.com>
35 <CAPweEDyw+LSW2S4sKWk-V24NSHYe2qqWO+KFqikQ34Q1Guhaig@mail.gmail.com>
36 <CAPweEDweXSC5c_ROQ8a3Y4hQMaJYmD_jAriadcZk9PRrkjOXvA@mail.gmail.com>
37 <25AC8A2E-D48F-439F-AF9D-0EB3DC08D7CC@gatech.edu>
38 From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
39 Date: Sat, 16 May 2020 18:33:05 +0100
40 X-Gmail-Original-Message-ID: <CAPweEDx_TMOxQHLrhbdhnXsBE1s-u2mz3xD2DDFCMi6m9BZCZg@mail.gmail.com>
41 Message-ID: <CAPweEDx_TMOxQHLrhbdhnXsBE1s-u2mz3xD2DDFCMi6m9BZCZg@mail.gmail.com>
42 To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
43 X-Content-Filtered-By: Mailman/MimeDel 2.1.23
44 Subject: Re: [libre-riscv-dev] Scoreboard vs Tomasulo
45 X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
46 X-Mailman-Version: 2.1.23
47 Precedence: list
48 List-Id: Libre-RISCV General Development
49 <libre-riscv-dev.lists.libre-riscv.org>
50 List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>,
51 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
52 List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
53 List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
54 List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
55 List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>,
56 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
57 Reply-To: Libre-RISCV General Development
58 <libre-riscv-dev@lists.libre-riscv.org>
59 Content-Type: text/plain; charset="utf-8"
60 Content-Transfer-Encoding: base64
61 Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
62 Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
63
64 T24gU2F0dXJkYXksIE1heSAxNiwgMjAyMCwgWWVob3dzaHVhIDx5aW1tYW51ZWwzQGdhdGVjaC5l
65 ZHU+IHdyb3RlOgoKPiBUaGlzIGlzIGEgdmVyeSBpbnRyaWNhdGUgYW5kIGNvbXBsaWNhdGVkIHN1
66 YmplY3QgbWF0dGVyIGZvciBzdXJlLgoKCnllcywgZXhjZXB0IGl0IGRvZXNuJ3QgaGF2ZSB0byBi
67 ZS4gIHRoZSBhY3R1YWwKaHR0cHM6Ly9lbi53aWtpcGVkaWEub3JnL3dpa2kvTGV2ZW5zaHRlaW5f
68 ZGlzdGFuY2UgYmV0d2VlbiBUb21hc3VsbyBhbmQKNjYwMCByZWFsbHkgaXMgbm90IHRoYXQgZ3Jl
69 YXQuCgppIHRob3VnaHQgaXQgd291bGQgYmUgZnVuIHRvIHVzZSBhIG5ldyB1bnByb25vdW5jZWFi
70 bGUgd29yZCBpIGxlYXJuZWQKeWVzdGVyZGF5IDopCgoKPiBBdCBzb21lIHBvaW50LCBpdCBiZSBn
71 cmVhdCB0byByZWFsbHkgYnJlYWsgdGhpbmdzIGRvd24gYW5kIG1ha2UgdGhlbSBtb3JlCj4gYWNj
72 ZXNzaWJsZS4KCgp5ZXMuIGl0IGNvbWVzIGRvd24gdG8gdGltZS4KCnN0YXJ0IHdpdGggdGhpcy4K
73 CjEuIEJlZ2luIGZyb20gVG9tYXN1bG8uICBuZWl0aGVyIFRTIG5vciBvcmlnaW5hbCA2NjAwIGhh
74 dmUgcHJlY2lzZQpleGNlcHRpb25zIHNvIHdlIGxlYXZlIHRoYXQgb3V0IGZvciBub3cuCgoyLiBT
75 dGFydCBieSBvbmx5IGFsbG93aW5nIG9uZSByb3cgcGVyIFJlc2VydmF0aW9uIFN0YXRpb24uCgoz
76 LiBFeHBhbmQgdGhlIG51bWJlciBvZiBSU2VzIHNvIHRoYXQgaWYgeW91IHdlcmUgdG8gY291bnQg
77 dGhlIHRvdGFsIG51bWJlcgpvZiBwbGFjZXMgb3BlcmFuZHMgYXJlIHN0b3JlZCwgdGhleSBhcmUg
78 dGhlIHNhbWUuCgooYW5vdGhlciB3YXkgdG8gcHV0IHRoaXMgaXMsICJmbGF0dGVuIGFsbCAyRCBS
79 U2VzIGludG8gMUQiKQoKNC4gd2hlcmUgcGlwZWxpbmVzIHdlcmUgZm9ybWVybHkgY29ubmVjdGVk
80 IGV4Y2x1c2l2ZWx5IHRvIG9uZSBSUywKKnByZXNlcnZlKiB0aG9zZSBjb25uZWN0aW9ucyBldmVu
81 IHRob3VnaCB0aGUgcm93cyBhcmUgbm93IDFEIGZsYXR0ZW5lZC4KCihhbm90aGVyIHdheSB0byBw
82 dXQgdGhpcyBpczogd2UgaGF2ZSBhIGdsb2JhbCAxRCBuYW1pbmcgc2NoZW1lIHRvIHJlZmVyZW5j
83 ZQp0aGUgKm9wZXJhbmQgbGF0Y2hlcyogcmF0aGVyIHRoYW4gYSAyRCBzY2hlbWUgaW52b2x2aW5n
84 IFJTIG51bWJlciBpbiAxCmRpbWVuc2lvbiBhbmQgdGhlIHJvdyBudW1iZXIgaW4gdGhlIDJuZCkK
85 CjUuIGdpdmUgdGhpcyAxRCBmbGF0dGVuaW5nIGFuIFVOQVJZIG51bWJlcmluZyBzY2hlbWUuCgo2
86 LiBtYWtlIHRoZSBzaXplIG9mIHRoZSBSZW9yZGVyIEJ1ZmZlciBFWEFDVExZIGVxdWFsIHRvIHRo
87 ZSBudW1iZXIgb2YgMUQKZmxhdHRlbmVkIFJTZXMuCgo3LiByZW5hbWUgUlNlcyB0byAiRnVuY3Rp
88 b24gVW5pdHMiIChhY3R1YWxseSBpbiBUaG9ybnRvbidzIGJvb2sgdGhlIHBocmFzZQoiQ29tcHV0
89 YXRpb24gVW5pdHMiIGlzIHVzZWQpCgp0aHVzLCBhdCB0aGlzIHBvaW50IGluIHRoZSB0cmFuc2Zv
90 cm1hdGlvbiwgdGhlIFJPQiByb3cgbnVtYmVyICpJUyogdGhlCkZ1bmN0aW9uIFVuaXQgTnVtYmVy
91 LCB0aGUgbmVlZCB0byBhY3R1YWxseSBzdG9yZSB0aGUgUk9CICMgaW4gdGhlClJlc2VydmF0aW9u
92 IFN0YXRpb24gUm93IGlzIFJFTU9WRUQsIGFuZCBjb25zZXF1ZW50bHkgdGhlIFJlc2VydmF0aW9u
93 ClN0YXRpb25zIGFyZSBOTyBMT05HRVIgQSBDQU0uCgo4LiBnaXZlIGFsbCByZWdpc3RlciBmaWxl
94 IG51bWJlcnMgKElOVCBGUCkgYW4gVU5BUlkgbnVtYmVyaW5nLgoKdGhpcyBtZWFucyB0aGF0IGlu
95 IHRoZSBST0IsIHRoZSBDQU0sIHdoaWNoIGhhcyB0byBsb29rIHVwIHRoZSByZWdpc3RlcgpudW1i
96 ZXIgYnkgaGl0dGluZyB0aGUgQ0FNIG9uIGV2ZXJ5IGN5Y2xlLCBub3cgb25seSBoYXMgdG8gbWF0
97 Y2ggYSBzaW5nbGUKQU5EIGdhdGUuCgpiaXR2ZWN0b3JzIHRoZXJlZm9yZSByZXBsYWNlIENBTXMu
98 Cgp3aXRoIHRoZSBST0Igbm93IGhhdmluZyByb3dzIG9mIGJpdHZlY3RvcnMsIGl0IGlzIG5vdyB0
99 ZXJtZWQgYSAiTWF0cml4Ii4KCnRoZSBsZWZ0IHNpZGUgb2YgdGhlIFJPQiwgd2hpY2ggdXNlZCB0
100 byBjb250YWluIHRoZSBSUyBOdW1iZXIgaW4gdW5hcnksIG5vdwpjb250YWlucyBhICpiaXR2ZWN0
101 b3IqIERpcmVjdGVkIEFjeWNsaWMgR3JhcGggb2YgdGhlIEZVIHRvIEZVIGRlcGVuZGVuY2llcywK
102 YW5kIGlzIHNwbGl0IG91dCBpbnRvIGl0cyBvd24gTWF0cml4LgoKdGhpcyB3ZSBjYWxsIHRoZSBG
103 VS1GVSBEZXBlbmRlbmN5IE1hdHJpeC4KCnRoZSByZW1haW5kZXIgb2YgdGhlICJST0IiIGNvbnRh
104 aW5zIHRoZSByZWdpc3RlciBudW1iZXJzIGluIHVuYXJ5IE1hdHJpeApmb3JtLCBhbmQgd2l0aCBl
105 YWNoIHJvdyBiZWluZyBkaXJlY3RseSBhc3NvY2lhdGVkIHdpdGggYSBGdW5jdGlvbiBVbml0LCB3
106 ZQpub3cgaGF2ZSBhbiBhc3NvY2lhdGlvbiBiZXR3ZWVuIEZVIGFuZCBSZWdzIHdoaWNoIHByZXNl
107 cnZlcyB0aGUga25vd2xlZGdlCm9mIHdoYXQgaW5zdHJ1Y3Rpb24gcmVxdWlyZWQgd2hpY2ggcmVn
108 aXN0ZXJzLCAqYW5kKiB3aG8gd2lsbCBwcm9kdWNlIHRoZQpyZXN1bHQuCgp0aGlzIHdlIGNhbGwg
109 dGhlIEZVLVJlZ3MgRGVwZW5kZW5jeSBNYXRyaXguCgp0aGF0ICpyZWFsbHkgaXMgaXQqLgoKdGFr
110 ZSBzb21lIHRpbWUgdG8gYWJzb3JiIHRoZSB0cmFuc2Zvcm1hdGlvbiB3aGljaCBub3Qgb25seSBw
111 cmVzZXJ2ZXMKYWJzb2x1dGVseSBldmVyeSBmdW5jdGlvbmFsIGFzcGVjdCBvZiB0aGUgVG9tYXN1
112 bG8gQWxnb3JpdGhtLCBpdApkcmFzdGljYWxseSBzaW1wbGlmaWVzIHRoZSBpbXBsZW1lbnRhdGlv
113 biwgcmVkdWNlcyBnYXRlIGNvdW50LCByZWR1Y2VzCnBvd2VyIGNvbnN1bXB0aW9uICphbmQqIHBy
114 b3ZpZGVzIGEgc3Ryb25nIGZvdW5kYXRpb24gZm9yIGRvaW5nIGFyYml0cmFyeQptdWx0aS1pc3N1
115 ZSBleGVjdXRpb24gd2l0aCBvbmx5IGFuIE8oTikgbGluZWFyIGluY3JlYXNlIGluIGdhdGUgY291
116 bnQgdG8gZG8Kc28uCgoKZnVydGhlciBoaWxhcmlvdXNseSBzaW1wbGUgYWRkaXRpb25hbCB0cmFu
117 c2Zvcm1hdGlvbnMgb2NjdXIgdG8gcmVwbGFjZQpmb3JtZXIgbWFzc2l2ZSByZXNvdXJjZSBjb25z
118 dHJhaW5lZCBib3R0bGVuZWNrcywgZHVlIHRvIHRoZSBiaW5hcnkKbnVtYmVyaW5nIG9uIGJvdGgg
119 Uk9CIG51bWJlcnMgYW5kIFJlZyBudW1iZXJzLCB3aXRoIHNpbXBsZSBsYXJnZSB1bmFyeSBOT1IK
120 Z2F0ZXM6CgoqIHRoZSBkZXRlcm1pbmF0aW9uIG9mIHdoZW4gaGF6YXJkcyBhcmUgY2xlYXIsIG9u
121 IGEgcGVyIHJlZ2lzdGVyIGJhc2lzLCBpcwphIGxhdWdoYWJseSB0cml2aWFsIE5PUiBnYXRlIGFj
122 cm9zcyBhbGwgY29sdW1ucyBvZiB0aGUgRlUtUkVHcyBtYXRyaXgsCnByb2R1Y2luZyBhIHJvdyBi
123 aXR2ZWN0b3IgZm9yIGVhY2ggcmVhZCByZWdpc3RlciBhbmQgZWFjaCB3cml0ZSByZWdpc3Rlci4K
124 CiogdGhlIGRldGVybWluYXRpb24gb2Ygd2hlbiBhIEZ1bmN0aW9uIFVuaXQgbWF5IHByb2NlZWQg
125 aXMgYSBsYXVnaGFibHkKdHJpdmlhbCBOT1IgZ2F0ZSBhY3Jvc3MgYWxsICpyb3dzKiBvZiB0aGUg
126 KkZVLUZVKiBNYXRyaXgsIHByb2R1Y2luZyBhCnJvdy1iYXNlZCB2ZWN0b3IsIGRldGVybWluaW5n
127 IHRoYXQgaXQgaXMgInJlYWRhYmxlIiBpZiB0aGVyZSBleGlzdHMgbm8Kd3JpdGUgaGF6YXJkIGFu
128 ZCAid3JpdGFibGUiIGlmIHRoZXJlIGV4aXN0cyBubyByZWFkIGhhemFyZC4KCiogdGhlIFRvbWFz
129 dWxvIENvbW1vbiBEYXRhIEJ1cywgZm9ybWVybHkgYmVpbmcgYSBzaW5nbGUgY2hva2Vwb2ludApi
130 aW5hcnktYWRkcmVzc2luZyBnbG9iYWwgQnVzLCBtYXkgbm93IGJlIHVwZ3JhZGVkIHRvICpNVUxU
131 SVBMRSogQ29tbW9uIERhdGEKQnVzZXMgdGhhdCwgYmVjYXVzZSB0aGUgYWRkcmVzc2luZyBpbmZv
132 cm1hdGlvbiBhYm91dCByZWdpc3RlcnMgaXMgbm93IGluCnVuYXJ5LCBpcyBsaWtld2lzZSBsYXVn
133 aGFibHkgdHJpdmlhbCB0byB1c2UgY2FzY2FkaW5nIFByaW9yaXR5IFBpY2tlcnMgKGEKbm1pZ2Vu
134 IFByaW9yaXR5RW5jb2RlciBhbmQgRGVjb2RlciwgYmFjay10by1iYWNrKSB0byBkZXRlcm1pbmUg
135 d2hpY2gKRnVuY3Rpb24gVW5pdCBzaGFsbCBiZSBncmFudGVkIGFjY2VzcyB0byB3aGljaCBDREIg
136 aW4gb3JkZXIgdG8gcmVjZWl2ZSAob3IKc2VuZCkgaXRzIG9wZXJhbmQgKG9yIHJlc3VsdCkuCgoq
137 IG11bHRpLWlzc3VlIGFzIGkgbWVudGlvbmVkIGEgZmV3IHRpbWVzIGlzIGFuIGVxdWFsbHkgbGF1
138 Z2hhYmx5IHRyaXZpYWwKbWF0dGVyIG9mIHRyYW5zaXRpdmVseSBjYXNjYWRpbmcgdGhlIFJlZ2lz
139 dGVyIERlcGVuZGVuY3kgSGF6YXJkcyAoYm90aCByZWFkCmFuZCB3cml0ZSkgYWNyb3NzIGZ1dHVy
140 ZSBpbnN0cnVjdGlvbnMgaW4gdGhlIHNhbWUgbXVsdGkgaXNzdWUgZXhlY3V0aW9uCndpbmRvdy4g
141 aW5zdHIyIGhhcyBpbnN0cjEgQU5EIGluc3RyMidzIGhhemFyZHMuICBpbnN0cjMgaGFzIGluc3Ry
142 MSBBTkQKaW5zdHIyIEFORCBpbnN0cjMncyBoYXphcmRzIGFuZCBzbyBvbi4gIHRoaXMganVzdCBs
143 ZWF2ZXMgdGhlIG5lY2Vzc2l0eSBvZgppbmNyZWFzaW5nIHJlZ2lzdGVyIHBvcnQgbnVtYmVycywg
144 bnVtYmVyIG9mIENEQnMsIGFuZCBMRC9TVCBtZW1vcnkKYmFuZHdpZHRoIHRvIGNvbXBlbnNhdGUg
145 YW5kIGNvcGUgd2l0aCB0aGUgYWRkaXRpb25hbCByZXNvdXJjZSBkZW1hbmRzIHRoYXQKd2lsbCBu
146 b3cgb2NjdXIuCgp0aGUgbGF0dGVyIGlzIHBhcnRpY3VsYXJseSB3aHkgd2UgaGF2ZSBhIGRlc2ln
147 biB0aGF0LCB1bHRpbWF0ZWx5LCB3ZSBjb3VsZAp0YWtlIG9uIEFSTSwgSW50ZWwsIGFuZCBBTUQu
148 Cgp0aGVyZSBpcyBubyByZWFzb24gdGVjaG5pY2FsbHkgd2h5IHdlIGNvdWxkIG5vdCBkbyBhIDQs
149 IDYgb3IgOCBtdWx0aSBpc3N1ZQpzeXN0ZW0sIGFuZCB3aXRoIGVub3VnaCBGdW5jdGlvbiBVbml0
150 cyBhbmQgdGhlIGN5Y2xpYyBidWZmZXIgc3lzdGVtIChzbyBhcwpub3QgdG8gcmVxdWlyZSBhIGZ1
151 bGwgY3Jvc3NiYXIgYXQgdGhlIENvbW1vbiBEYXRhIEJ1c2VzKSwgYW5kIHByb3BlcgpzdHJhdGlm
152 aWNhdGlvbiBhbmQgZGVzaWduIG9mIHRoZSByZWdpc3RlciBmaWxlcywgbWFzc2l2ZSBWZWN0b3Ig
153 cGFyYWxsZWxpc20KYXQgdGhlIHBpcGVsaW5lcyB3b3VsZCBiZSBrZXB0IGZ1bGx5IG9jY3VwaWVk
154 IHdpdGhvdXQgYW4gb3ZlcndoZWxtaW5nCmluY3JlYXNlIGluIGdhdGVzIG9yIHBvd2VyIGNvbnN1
155 bXB0aW9uIHRoYXQgd291bGQgbm9ybWFsbHkgYmUgZXhwZWN0ZWQsIGFuZApzY2FsYXIgcGVyZm9y
156 bWFuY2Ugd291bGQgYmUgc2ltaWxhcmx5IGhpZ2ggYXMgd2VsbC4KCmwuCgoKCgotLSAKLS0tCmNy
157 b3dkLWZ1bmRlZCBlY28tY29uc2Npb3VzIGhhcmR3YXJlOiBodHRwczovL3d3dy5jcm93ZHN1cHBs
158 eS5jb20vZW9tYTY4Cl9fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f
159 X19fCmxpYnJlLXJpc2N2LWRldiBtYWlsaW5nIGxpc3QKbGlicmUtcmlzY3YtZGV2QGxpc3RzLmxp
160 YnJlLXJpc2N2Lm9yZwpodHRwOi8vbGlzdHMubGlicmUtcmlzY3Yub3JnL21haWxtYW4vbGlzdGlu
161 Zm8vbGlicmUtcmlzY3YtZGV2Cg==
162