[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / 21 / dd7a9449fca3b704c811bc3fbfde18d44fd19b
1 Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
2 Envelope-to: publicinbox@libre-riscv.org
3 Delivery-date: Sun, 17 May 2020 23:24:20 +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 1jaRhj-0002Rb-9i; Sun, 17 May 2020 23:24:19 +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 1jaRhh-0002RV-Q6
11 for libre-riscv-dev@lists.libre-riscv.org; Sun, 17 May 2020 23:24:17 +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=Vn1rzBMgdlKVQ4FTJgmS2zCva1+BKNMMdK/BWctRztM=;
16 b=C+d9LxJooeygUzeUMkWpfRN9YXcIKsz5v3vEHy/Mg4UPM5eCwgdU37XOLmPsP2K/4gHNozp6gbszuEY6PHM/yc+szBg7CnTKzv09nYjfnWEoPje86W47tcE9d1Mz0o1/ZgMnx0/RolmnX9eUpWcDGXat6+lXFaOTNRuu/RH/zWs=;
17 Received: from mail-lj1-f178.google.com ([209.85.208.178])
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 1jaRhh-0002Ph-Ev
20 for libre-riscv-dev@lists.libre-riscv.org; Sun, 17 May 2020 22:24:17 +0000
21 Received: by mail-lj1-f178.google.com with SMTP id g1so7810311ljk.7
22 for <libre-riscv-dev@lists.libre-riscv.org>;
23 Sun, 17 May 2020 15:24:02 -0700 (PDT)
24 X-Gm-Message-State: AOAM532/Mw3UTlfiPla3tNzJRRdlcxs6sf4A7/X9diVyKssv+wRXD9eS
25 S2bbnwznhVRtAB8e7I9y4/4FMeJZIXY0WvRoO/U=
26 X-Google-Smtp-Source: ABdhPJwDaCNBIBoXa+P6L552sL1VcWQ+ZZCM4+rtcbWmNEISOZ8kvzc4cHYVDwu+vmeuaWcdZCqM9QYom2ZVsZ0Z1xY=
27 X-Received: by 2002:a2e:2245:: with SMTP id i66mr8787500lji.191.1589754236446;
28 Sun, 17 May 2020 15:23:56 -0700 (PDT)
29 MIME-Version: 1.0
30 References: <13EDF987-9A19-4C96-89C2-6DB784CF2C96@gatech.edu>
31 <CAPweEDyDcmAJbJx+PKkL8MotPMNyHyFOEtuNOKP+V2PmmY5HvA@mail.gmail.com>
32 <CAPweEDyw+LSW2S4sKWk-V24NSHYe2qqWO+KFqikQ34Q1Guhaig@mail.gmail.com>
33 <CAPweEDweXSC5c_ROQ8a3Y4hQMaJYmD_jAriadcZk9PRrkjOXvA@mail.gmail.com>
34 <25AC8A2E-D48F-439F-AF9D-0EB3DC08D7CC@gatech.edu>
35 <CAPweEDx_TMOxQHLrhbdhnXsBE1s-u2mz3xD2DDFCMi6m9BZCZg@mail.gmail.com>
36 <CAEoCstRd+hLfF5YtUbnS2gukPxVAjmheJrZ29QvJD3y4Y928JQ@mail.gmail.com>
37 <CAPweEDxXGedm-4QwmU2UuYvb4G2nNaoAsy_P2eyviQ42pbmyXA@mail.gmail.com>
38 <CAEoCstSGxwV88JUHTQmUp=75kHWxSZNSPu==_pxsUYf29ctd9w@mail.gmail.com>
39 <CAPweEDzp3aSyhi-+UOO5Ce_gdUFGjpGqGVZM+GT0qDTLGtpZ-g@mail.gmail.com>
40 <ec75de0d-6ffb-969f-4250-f8a9ecf120b0@gmail.com>
41 <CAPweEDwZzU904jAo9UUn+x4C7GOvvYG+GooSePwBHw96AwtoLg@mail.gmail.com>
42 <12f9f234-b1f6-3624-5a35-b6fa85e84615@gmail.com>
43 <CAPweEDzTD3rF7cz-36qS5K_-fX6yaWGWd+yo0K17AjQdCOXqcw@mail.gmail.com>
44 In-Reply-To: <CAPweEDzTD3rF7cz-36qS5K_-fX6yaWGWd+yo0K17AjQdCOXqcw@mail.gmail.com>
45 From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
46 Date: Sun, 17 May 2020 23:23:44 +0100
47 X-Gmail-Original-Message-ID: <CAPweEDwWOynkzhFcPJmyFVBHYjWJJf6sRc+YbzNc+ZrV0Q7jQA@mail.gmail.com>
48 Message-ID: <CAPweEDwWOynkzhFcPJmyFVBHYjWJJf6sRc+YbzNc+ZrV0Q7jQA@mail.gmail.com>
49 To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
50 Subject: Re: [libre-riscv-dev] LD/ST Comp Unit FSM (was: Re: Scoreboard vs
51 Tomasulo)
52 X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
53 X-Mailman-Version: 2.1.23
54 Precedence: list
55 List-Id: Libre-RISCV General Development
56 <libre-riscv-dev.lists.libre-riscv.org>
57 List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>,
58 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
59 List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
60 List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
61 List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
62 List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>,
63 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
64 Reply-To: Libre-RISCV General Development
65 <libre-riscv-dev@lists.libre-riscv.org>
66 Content-Type: text/plain; charset="utf-8"
67 Content-Transfer-Encoding: base64
68 Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
69 Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
70
71 YnR3IENlc2FyIHlvdSd2ZSBiZWVuIHRyYWNraW5nIHRoZSBsaXN0IGZvciBhIHdoaWxlLCBzbyB5
72 b3Uga25vdyBvZiB0aGlzOgpodHRwczovL2xpYnJlLXNvYy5vcmcvSERMX3dvcmtmbG93CgpmZWVs
73 IGZyZWUgdG8gc2VuZCBtZSBhbiBzc2ggcHVibGljIGtleS4KCmwuCgpfX19fX19fX19fX19fX19f
74 X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fXwpsaWJyZS1yaXNjdi1kZXYgbWFpbGluZyBs
75 aXN0CmxpYnJlLXJpc2N2LWRldkBsaXN0cy5saWJyZS1yaXNjdi5vcmcKaHR0cDovL2xpc3RzLmxp
76 YnJlLXJpc2N2Lm9yZy9tYWlsbWFuL2xpc3RpbmZvL2xpYnJlLXJpc2N2LWRldgo=
77