[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / b7 / 66d3eec7783c698c93de4c057cc26c2e92e6bc
1 Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
2 Envelope-to: publicinbox@libre-riscv.org
3 Delivery-date: Fri, 15 May 2020 22:56:17 +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 1jZiJV-0002nF-3f; Fri, 15 May 2020 22:56:17 +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 1jZiJU-0002n9-Dq
11 for libre-riscv-dev@lists.libre-riscv.org; Fri, 15 May 2020 22:56:16 +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=q1AO8qwwD7iTORbBbXcXsczte0ozRAXMaruULmCc5LQ=;
16 b=Wyo6nljCtaxvAv0UZmAojJQExvocdc/whMPMIiCKXcuh3UaB/GAqAZy1qLoQEY7Y8LCpq9gAIidXUx27Tj1nwvnaLQH65Z3PW4r4Ia9lKP4Er28ri+9Iaw9xaJlXl70AJGhsBL2bKYPFuipw3OxBc5LJvWQz9Hm3ryfTJfLO+a4=;
17 Received: from mail-lj1-f173.google.com ([209.85.208.173])
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 1jZiJU-0004z5-4I
20 for libre-riscv-dev@lists.libre-riscv.org; Fri, 15 May 2020 21:56:16 +0000
21 Received: by mail-lj1-f173.google.com with SMTP id b6so3842668ljj.1
22 for <libre-riscv-dev@lists.libre-riscv.org>;
23 Fri, 15 May 2020 14:56:00 -0700 (PDT)
24 X-Gm-Message-State: AOAM5316aeCJN/1in0TEUqb+V0hYarlzllzriCi6728kJj2C2Xv37sBP
25 0TXxMpKnHiXiUxIuWebHirrsjBGgOOipy3/7JCw=
26 X-Google-Smtp-Source: ABdhPJwCRRwP627cHNowg7YUgRUemZVWzrdqgOjA/KRFsy/5epjqPxJMEHDaEwTWeTDYCiFQD9+Oo0oKqjKyo0habjc=
27 X-Received: by 2002:a2e:9081:: with SMTP id l1mr3276016ljg.81.1589579755140;
28 Fri, 15 May 2020 14:55:55 -0700 (PDT)
29 MIME-Version: 1.0
30 References: <CAEoCstQz36UuDJ+ZUgLRJNeQkA=pTfYuzCr+XgF-FJY9+yJsvA@mail.gmail.com>
31 <747F8870-06C6-46A0-AFD9-D55289D4C41A@gatech.edu>
32 <CAEoCstRUXkB_LxXXubx4A0dhLGvFqq6EPL+GzukDQORpHopaiw@mail.gmail.com>
33 <4BDA96A5-9063-42A6-9548-CAE3CBEBEBAC@gatech.edu>
34 <CAPweEDyZQEBsh8uZ4VkzzALPcoiTgs0AvTmTwS6B0Dc+jy+mfw@mail.gmail.com>
35 <CAEoCstTERH=Z84je148ffL7_yiBYFj_Zet2VfOzkbe86MVmyQQ@mail.gmail.com>
36 <CAC2bXD4udi-tytQQACjZXsq=HURLEJVtianh+BGv0qJp+AVfFQ@mail.gmail.com>
37 In-Reply-To: <CAC2bXD4udi-tytQQACjZXsq=HURLEJVtianh+BGv0qJp+AVfFQ@mail.gmail.com>
38 From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
39 Date: Fri, 15 May 2020 22:55:43 +0100
40 X-Gmail-Original-Message-ID: <CAPweEDy75hwhXiXrUOzXugWLU1m0739YT6gf4WxCdtMFj91LWQ@mail.gmail.com>
41 Message-ID: <CAPweEDy75hwhXiXrUOzXugWLU1m0739YT6gf4WxCdtMFj91LWQ@mail.gmail.com>
42 To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
43 Subject: Re: [libre-riscv-dev] Introduction and Questions
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 T24gRnJpLCBNYXkgMTUsIDIwMjAgYXQgMTA6MjAgUE0gSmFjb2IgTGlmc2hheSA8cHJvZ3JhbW1l
64 cmpha2VAZ21haWwuY29tPiB3cm90ZToKCj4gV2Ugd2lsbCBkZWZpbml0ZWx5IG5lZWQgbW9yZSBz
65 dGFnZXMgaW4gdGhlIGZldGNoIHBpcGVsaW5lIGZvciBicmFuY2gKPiBwcmVkaWN0aW9uLCBUTEIs
66 IGFuZCBjYWNoZSBoYW5kbGluZywgSSdtIGd1ZXNzaW5nIDIgb3IgMyBmZXRjaCBzdGFnZXMuCgpv
67 aCwgeWVzLiAgZ29vZCBjYXRjaC4gIGFoLi4uIG9rIFRMQiBpcyBkZWxpYmVyYXRlbHkga2VwdCB0
68 byB2ZXJ5IHNtYWxsCnNpemVzICg4IGVudHJpZXMgbWF4KQpzbyB0aGF0IGl0IGNhbiByZXNwb25k
69 IGluIDEgY3ljbGUgKG9yLCBzYW1lLWN5Y2xlKS4gIGJyYW5jaCBwcmVkaWN0aW9uIGFuZApjYWNo
70 ZSBtaXNzZXMsIGkgbGVmdCBvdXQgYmVjYXVzZSB0aGV5J3JlICJleHRyYSIgKGJ1dCBvbmx5IG9u
71 IG1pc3NlcykuCgpob3dldmVyIGZvciBoaWdoZXIgc3BlZWRzLCBUTEJzIGFyZSBvZnRlbiBjYXNj
72 YWRlZCBhbmQgYWdhaW4gZW5kIHVwIHdpdGgKZXh0cmEgbWlzc2VzLiAgdGhhdCdzIGFjY29yZGlu
73 ZyB0byB0aGUgd2lraXBlZGlhIHBhZ2Ugb24gVExCIDopCgpsLgoKX19fX19fX19fX19fX19fX19f
74 X19fX19fX19fX19fX19fX19fX19fX19fX19fX18KbGlicmUtcmlzY3YtZGV2IG1haWxpbmcgbGlz
75 dApsaWJyZS1yaXNjdi1kZXZAbGlzdHMubGlicmUtcmlzY3Yub3JnCmh0dHA6Ly9saXN0cy5saWJy
76 ZS1yaXNjdi5vcmcvbWFpbG1hbi9saXN0aW5mby9saWJyZS1yaXNjdi1kZXYK
77