[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / e1 / 0eb8a21dffdef289abd1746b9ea82d762b19fd
1 Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
2 Envelope-to: publicinbox@libre-riscv.org
3 Delivery-date: Wed, 13 May 2020 15:34:29 +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 1jYsSq-0004Lb-Ms; Wed, 13 May 2020 15:34:28 +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 1jYsSo-0004LV-FU
11 for libre-riscv-dev@lists.libre-riscv.org; Wed, 13 May 2020 15:34:26 +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:In-Reply-To:References:MIME-Version;
15 bh=IneZByqed1s5uWJ7j20c/RmeRlpivYtGsaQSABese1Q=;
16 b=AdoAyaMvtUXpwm93ccUlaowc/5sRd4b9OKvUOegYpAUwrtUzueX6TNWYXPAP/SkKJUk0vx6cW2Zarvo+PjJh1BWEV8m97A0Ph74MhfwCjdKGGTuEU7TBTS6JSBuIa9V9v6ronUmZ8nPkw8iNSpqnUKjgsyB/mM/+jKJwccC0H7c=;
17 Received: from mail-lf1-f53.google.com ([209.85.167.53])
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 1jYsSo-0007RS-0p
20 for libre-riscv-dev@lists.libre-riscv.org; Wed, 13 May 2020 14:34:26 +0000
21 Received: by mail-lf1-f53.google.com with SMTP id z22so13868825lfd.0
22 for <libre-riscv-dev@lists.libre-riscv.org>;
23 Wed, 13 May 2020 07:34:10 -0700 (PDT)
24 X-Gm-Message-State: AOAM533ffHAt8rZ1PGoQHvtYLGYGr9WPXQb1tJ4owoWlPY4aKcABW3N3
25 Ed5owFgwrMtUjM0a/2YTU6ZHrmJ3jNHvs3q0czM=
26 X-Google-Smtp-Source: ABdhPJx1VdYdwyaaS92C5gfbtiXUDp93DswGaxipdflSvrU8CB3HxedW6L6HhzGqSDdbYrA8gXlxAu9Js8I7NgS41yA=
27 X-Received: by 2002:ac2:5dd5:: with SMTP id x21mr18216164lfq.107.1589380444982;
28 Wed, 13 May 2020 07:34:04 -0700 (PDT)
29 MIME-Version: 1.0
30 References: <CAPweEDz8rcJ7ENbJS5tk3pCs7TDSPx11=7cOPFwxRaTBbtW_wg@mail.gmail.com>
31 <20200513155647.d30fe7986374bed381ba8360@platen-software.de>
32 In-Reply-To: <20200513155647.d30fe7986374bed381ba8360@platen-software.de>
33 From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
34 Date: Wed, 13 May 2020 15:33:53 +0100
35 X-Gmail-Original-Message-ID: <CAPweEDw+JVQPF6f=MXK-PTcFpqTk8z_j0p4ZFYgG0qBK9raX7A@mail.gmail.com>
36 Message-ID: <CAPweEDw+JVQPF6f=MXK-PTcFpqTk8z_j0p4ZFYgG0qBK9raX7A@mail.gmail.com>
37 To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
38 Subject: Re: [libre-riscv-dev] daily kan-ban update 13may2020
39 X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
40 X-Mailman-Version: 2.1.23
41 Precedence: list
42 List-Id: Libre-RISCV General Development
43 <libre-riscv-dev.lists.libre-riscv.org>
44 List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>,
45 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
46 List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
47 List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
48 List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
49 List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>,
50 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
51 Reply-To: Libre-RISCV General Development
52 <libre-riscv-dev@lists.libre-riscv.org>
53 Content-Type: text/plain; charset="utf-8"
54 Content-Transfer-Encoding: base64
55 Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
56 Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
57
58 LS0tCmNyb3dkLWZ1bmRlZCBlY28tY29uc2Npb3VzIGhhcmR3YXJlOiBodHRwczovL3d3dy5jcm93
59 ZHN1cHBseS5jb20vZW9tYTY4CgpPbiBXZWQsIE1heSAxMywgMjAyMCBhdCAyOjU2IFBNIFRvYmlh
60 cyBQbGF0ZW4KPGxpYnJlLXNvY0BwbGF0ZW4tc29mdHdhcmUuZGU+IHdyb3RlOgo+Cj4gT24gV2Vk
61 LCAxMyBNYXkgMjAyMCAxMToyODoyNSArMDEwMAo+IEx1a2UgS2VubmV0aCBDYXNzb24gTGVpZ2h0
62 b24gPGxrY2xAbGtjbC5uZXQ+IHdyb3RlOgo+Cj4gPiB5ZXN0ZXJkYXkgaSBzdGFydGVkIG9uIGlu
63 dGVncmF0aW5nIHRoZSBMRFNUQ29tcFVuaXQgaW50byB0aGUKPiA+IHNjb3JlYm9hcmQgYW5kIGlt
64 bWVkaWF0ZWx5IHJhbiBpbnRvIGEgYnJpY2sgd2FsbCBpbiB0aGUgZm9ybSBvZiB0aGUKPiA+IGFk
65 ZHJlc3MtcmVxdWVzdC9yZWxlYXNlIHNpZ25hbGxpbmcuICB3aGVuIGdvX2FkZHIgaXMgcmFpc2Vk
66 IChpbgo+ID4gcmVzcG9uc2UgdG8gcmVxX2FkZHIpLCB0aGUgTERTVENvbXBVbml0IGlzIHN1cHBv
67 c2VkIHRvIGRyb3AgcmVxX2FkZHIKPiA+IG9uZSBjeWNsZSBsYXRlcjogaW5zdGVhZCBpdCBzdGF5
68 cyBoaWdoLgo+ID4KPiA+IGkgYWxzbyBpbnZlc3RpZ2F0ZWQgbWljcm93YXR0IHRvIGZpbmQgb3V0
69 IHdoYXQgdGhlIGhlY2sgaXMgZ29pbmcgb24KPiA+IHdpdGggdGhlIHJlZ2lzdGVyLW9yZGVyLXN3
70 YXBwaW5nLiAgdHVybnMgb3V0IHRoYXQgZGlmZmVyZW50IGNsYXNzZXMgb2YKPiA+IG9wZXJhdGlv
71 bnMgKGxvZ2ljYWwsIHJvdGF0ZSwgYXJpdGgpIGhhdmUgZGlmZmVyZW50IG9yZGVyaW5nLiAgd2h5
72 PyB3aG8KPiA+IGtub3dzLgo+ID4KPiA+IHRvZGF5IGkgd2lsbCBjb250aW51ZSB3b3JraW5nIHRo
73 cm91Z2ggdGhlIGFkZHJlc3MtbmVnb3RpYXRpb24gaW4gTERTVENvbXBVbml0Lgo+ID4KPiA+IGwu
74 Cj4gPgo+ID4gX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18K
75 PiA+IGxpYnJlLXJpc2N2LWRldiBtYWlsaW5nIGxpc3QKPiA+IGxpYnJlLXJpc2N2LWRldkBsaXN0
76 cy5saWJyZS1yaXNjdi5vcmcKPiA+IGh0dHA6Ly9saXN0cy5saWJyZS1yaXNjdi5vcmcvbWFpbG1h
77 bi9saXN0aW5mby9saWJyZS1yaXNjdi1kZXYKPgo+IEkndmUgbG9va2VkIGludG8gdGhlIHNvYy9z
78 cmMvc29jL2RlY29kZXIvaXNhIGFuZCBzcmMvc29jL2FsdS8gZGlyZWN0b3JpZXMuCj4gVGhlcmUg
79 aXMgYSBUT0RPIHRoYXQgcmVmZXJlbmNlcyB0aGUgUG93ZXJJU0EgUERGLCBzbyBJIHdpbGwgZmly
80 c3QgcmVhZCB0aGUKPiBmb2xsb3dpbmcgc2VjdGlvbnMsIGJlZm9yZSB3cml0aW5nIGFueXRoaW5n
81 LgoKYSByZWFsbHkgdXNlZnVsIHNlbGYtY29udGFpbmVkIHN1Yi10YXNrIHdvdWxkIGJlIHRvIGNv
82 bnZlcnQgdGhpcyB0byBubWlnZW46Cmh0dHBzOi8vZ2l0aHViLmNvbS9hbnRvbmJsYW5jaGFyZC9t
83 aWNyb3dhdHQvYmxvYi9tYXN0ZXIvY291bnR6ZXJvLnZoZGwKCmZvY3Vzc2luZyBvbiB0aGF0IHdv
84 dWxkIGFsbG93IHlvdSB0byBkbyBzb21ldGhpbmcgaW1tZWRpYXRlbHkgdGhhdCBkaWQKbm90IHJl
85 cXVpcmUgYSBsb3Qgb2YgYmFja2dyb3VuZCByZWFkaW5nIG9yIHByZXBhcmF0aW9uLCBhbmQgeWV0
86 IGlzIHJlYWxseQppbXBvcnRhbnQgYW5kIHZhbHVhYmxlLCBhbmQgY2FuIGJlIGRvbmUgZmFzdC4K
87 CnlvdSBjYW4gc2VlIHdoYXQgaSBkaWQgd2l0aCByb3RhdG9yLnB5IHRvIGdldCBhIGZlZWwgZm9y
88 IGhvdyB0aGF0J3MgZG9uZS4KdGhlc2UgYXJlIHR3byByZWFsbHkgaW1wb3J0YW50IGdvdGNoYXMg
89 dG8gd2F0Y2ggb3V0IGZvcjoKCiogc2lnbmFsKEhJIGRvd250byBMTykgbXVzdCBiZSBjb252ZXJ0
90 ZWQgdG8gc2lnbmFsW0xPOkhJKzFdICAqKk5PVEUKVEhFIEFERCBPTkUqKgoqIEEgJiBCICYgQyBt
91 dXN0IGJlIGNvbnZlcnRlZCB0byBDYXQoQywgQiwgQSkKCmFzIHRoaXMgaXMgb25seSAxNDAgbGlu
92 ZXMgb2YgY29kZSwgaWYgeW91IHBsYW4gdG8gLSBvciBpbWFnaW5lIHRoYXQgLQp0aGUgdGltZSB0
93 YWtlbgppcyBncmVhdGVyIHRoYW4gNjAgdG8gOTAgbWludXRlcyB0byBjb21wbGV0ZSBhIGZpcnN0
94 IGN1dCAod2hpY2ggc2hvdWxkIGJlCmNvbW1pdHRlZCBpbW1lZGlhdGVseSksIHRoZW4gc29tZXRo
95 aW5nIGlzIHdyb25nLiAgdGhpcyBpcyBhIGhhbGYgdG8gb25lIGRheQp0YXNrLCBhYnNvbHV0ZSBt
96 YXguCgpnb2luZyBvbiBmcm9tIHRoZXJlIC0gYmV5b25kIHRoYXQgaGFsZi1kYXk6CgppZiB5b3Ug
97 Y2FuIGFsc28gd3JpdGUgYSBmb3JtYWwgcHJvb2YsIHRoZXNlIHdlIGNhbiBkb25hdGUgbW9yZSwg
98 d2hlcmUgZm9yCnRoZSAibWFpbiBjb3JlIiAtIGp1c3QgdGhlIGNvdW50emVybyAtIHdlIGFyZSBy
99 dW5uaW5nIGxvdyBmcm9tIHRoYXQgYnVkZ2V0Lgpmb3JtYWwgcHJvb2ZzIGFyZSBiYXNpY2FsbHkg
100 ImEgYnVuY2ggb2YgYXNzZXJ0cyIgZXhhY3RseSBhcyB5b3Ugd291bGQgaGF2ZQppbiBjKysgY29k
101 ZSBvciBhbnkgb3RoZXIgbGFuZ3VhZ2Ugd2l0aCAiYXNzZXJ0IGlmIHRoaXMgaXMgdHJ1ZSBvciBu
102 b3QiLgoKPiAgICAgICAgICMgNC4yLjIgcDEyNCBGUFNDUiAoZGVmaW5pdGVseSAic2VwYXJhdGUi
103 IC0gbm90IGluIFNQUikKPiAgICAgICAgICMgICAgICAgICAgICBub3RlIHRoYXQgbWZmcywgbWNy
104 ZnMsIG10ZnNmICJtYW5hZ2UiIHRoaXMgRlBTQ1IKPiAgICAgICAgICMgMi4zLjEgQ1IgKGFuZCBz
105 dWItZmllbGRzIENSMC4uQ1I2IC0gQ1IwIFNPIGNvbWVzIGZyb20gWEVSLlNPKQo+ICAgICAgICAg
106 IyAgICAgICAgIG5vdGUgdGhhdCBtZm9jcmYsIG1mY3IsIG10Y3IsIG10b2NyZiwgbWNyeHJ4ICJt
107 YW5hZ2UiIENScwo+ICAgICAgICAgIyAyLjMuMiBMUiAgIChhY3R1YWxseSBTUFIgIzgpCj4gICAg
108 ICAgICAjIDIuMy4zIENUUiAgKGFjdHVhbGx5IFNQUiAjOSkKPiAgICAgICAgICMgMi4zLjQgVEFS
109 ICAoYWN0dWFsbHkgU1BSICM4MTUpCj4gICAgICAgICAjIDMuMi4yIHA0NSBYRVIgIChhY3R1YWxs
110 eSBTUFIgIzApCj4gICAgICAgICAjIDMuMi4zIHA0NiBwMjMyIFZSU0FWRSAoYWN0dWFsbHkgU1BS
111 ICMyNTYpCj4gSSBhc3N1bWUgdGhhdCB0aGF0IHRoZSB2ZXJzaW9uIG9mIHRoZSBwZGYgcmVmZXJl
112 bmNlZCBpcyBzdGlsbCAzLjAgb25lIGFuZCBub3QgMy4xIHJlY2VudGx5IHJlbGVhc2VkLgoKY29y
113 cmVjdC4KCmwuCgpfX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f
114 XwpsaWJyZS1yaXNjdi1kZXYgbWFpbGluZyBsaXN0CmxpYnJlLXJpc2N2LWRldkBsaXN0cy5saWJy
115 ZS1yaXNjdi5vcmcKaHR0cDovL2xpc3RzLmxpYnJlLXJpc2N2Lm9yZy9tYWlsbWFuL2xpc3RpbmZv
116 L2xpYnJlLXJpc2N2LWRldgo=
117