[libre-riscv-dev] [Bug 335] New: Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / 40 / 9df2467aeb7ccc6896834693bdce0551e5c298
1 Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
2 Envelope-to: publicinbox@libre-riscv.org
3 Delivery-date: Fri, 08 May 2020 16:10:54 +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 1jX4eL-0006ha-VP; Fri, 08 May 2020 16:10:53 +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 1jX4eK-0006hS-CK
11 for libre-riscv-dev@lists.libre-riscv.org; Fri, 08 May 2020 16:10:52 +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=zuU1Qxm0f50MXSRH9/1/jzoEN3qi9vX4Qj2MMgRsMko=;
16 b=XygeiNJ7qRUWe1dHTPLvT+3qYthomEOtltkVGupd3JSJEnI4eixYSPtR4ZBrkjoc4CvLO1zGhL2odIT+4de2t6Uzz9mi6OJ987x1xOiklZvEAKFSP3DsvxpCZ74oAzcU9gpqZoUD1ULmkoJfOaoooPf71sfA1GSkUjAM7VLJY/M=;
17 Received: from mail-lj1-f172.google.com ([209.85.208.172])
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 1jX4eJ-0006TB-WC
20 for libre-riscv-dev@lists.libre-riscv.org; Fri, 08 May 2020 15:10:52 +0000
21 Received: by mail-lj1-f172.google.com with SMTP id e25so2031565ljg.5
22 for <libre-riscv-dev@lists.libre-riscv.org>;
23 Fri, 08 May 2020 08:10:36 -0700 (PDT)
24 X-Gm-Message-State: AOAM533xMxVoIkk3hcWniwXcBdegTOgRL2cri0zN538wf99tbRBXGBly
25 RscIUe/4mU0bBvBxQdB7TjJfplPzY/sZ7ka+4Jk=
26 X-Google-Smtp-Source: ABdhPJzbolNCa4PpP7oDOZg0tEOia+mjuZvtBBid3n5EwdjhzShZPKX6BPplppvQiHtDoPH+EReVGB2D+EmuwfSKyEU=
27 X-Received: by 2002:a2e:8056:: with SMTP id p22mr2082842ljg.266.1588950631048;
28 Fri, 08 May 2020 08:10:31 -0700 (PDT)
29 MIME-Version: 1.0
30 References: <CAPweEDw-nM8HiGuMaSZPsvf0HBJCCpAfRQjJJOpUZce7uiBOrQ@mail.gmail.com>
31 <70a36b10-a95d-c956-03a0-c0c4dfda6f0d@gmail.com>
32 In-Reply-To: <70a36b10-a95d-c956-03a0-c0c4dfda6f0d@gmail.com>
33 From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
34 Date: Fri, 8 May 2020 16:10:19 +0100
35 X-Gmail-Original-Message-ID: <CAPweEDwaffb9wvD7-Vg3ODfRdocVyLjf_qzBted-i_ZefL0wXA@mail.gmail.com>
36 Message-ID: <CAPweEDwaffb9wvD7-Vg3ODfRdocVyLjf_qzBted-i_ZefL0wXA@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 08mar2020
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 T24gRnJpLCBNYXkgOCwgMjAyMCBhdCAyOjI4IFBNIE1pY2hhZWwgTm9sYW4gPG10bm9sYW4yNjQw
59 QGdtYWlsLmNvbT4gd3JvdGU6Cj4KPiBOb3cgdGhhdCBJIGhhdmUgYnJhbmNoZXMgd29ya2luZyBp
60 biB0aGUgc2ltdWxhdG9yLCBJIHdhcyB0aGlua2luZyBvZgo+IHN0YXJ0aW5nIHdvcmsgb24gdGhl
61 IGludGVnZXIgQUxVLiBUYWtpbmcgYSBsb29rIGF0IGFsdV9oaWVyLnB5LCBJIHRoaW5rCj4gSSds
62 bCBrZWVwIHRoZSBpbnRlcmZhY2UgYnV0IHJlcGxhY2UgdGhlIGltcGxlbWVudGF0aW9uIHdpdGgg
63 YSBwaXBlbGluZWQKPiBvbmUuCgp5ZXMgcGxlYXNlLiAgcGxlYXNlIHJhaXNlIGEgYnVncmVwb3J0
64 IGFib3V0IGl0LCBhc3NpZ24gaXQgdG8geW91cnNlbGYsCmFuZCBtYWtlIGNlcnRhaW4gdG8gdXNl
65 IHRoZSBSZXNlcnZhdGlvblN0YXRpb25zIGJhc2UgY2xhc3MgYW5kIHRlc3QKaW5mcmFzdHJ1Y3R1
66 cmUgKHJ1bmZwKSBleGFjdGx5IGFzIGkgZGVzY3JpYmVkIGluIGhlcmU6CgpodHRwczovL2J1Z3Mu
67 bGlicmUtc29jLm9yZy9zaG93X2J1Zy5jZ2k/aWQ9MjA4I2M1NQoKKmFsbCogQUxVcyBuZWVkIHRv
68 IGhhdmUgdGhhdCBjb21tb24gaW50ZXJmYWNlIChtdWx0aXBsZQppbnB1dHMtb3V0cHV0cykuICBp
69 ZiB5b3UgY2FuLCB1c2UgcnVuZnAgLSBpZiB0aGVyZSdzIGFueSBhc3N1bXB0aW9ucwphYm91dCB0
70 aGUgZm9ybWF0IGJlaW5nIEZQIG51bWJlcnMsIGFkZCBhbiBleHRyYSBwYXJhbWV0ZXIgd2hpY2gg
71 ZG9lcwpkZWJ1ZyBwcmludGluZyBhcyBoZXhhZGVjaW1hbC4gIGkgKnRoaW5rKiBpdCBzaG91bGQg
72 ZG8gdGhhdCBhbnl3YXkKYmVjYXVzZSBpIHVzZWQgdGhlIHNhbWUgcnVuZnAgdGVzdCBjb2RlIGZv
73 ciBGUC10by1JTlQgYW5kIElOVC10by1GUAoKbC4KCl9fX19fX19fX19fX19fX19fX19fX19fX19f
74 X19fX19fX19fX19fX19fX19fX19fCmxpYnJlLXJpc2N2LWRldiBtYWlsaW5nIGxpc3QKbGlicmUt
75 cmlzY3YtZGV2QGxpc3RzLmxpYnJlLXJpc2N2Lm9yZwpodHRwOi8vbGlzdHMubGlicmUtcmlzY3Yu
76 b3JnL21haWxtYW4vbGlzdGluZm8vbGlicmUtcmlzY3YtZGV2Cg==
77