[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / b7 / 7da2025398426f576f13a61f3b76dd10e9f93d
1 Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
2 Envelope-to: publicinbox@libre-riscv.org
3 Delivery-date: Tue, 05 May 2020 14:07:56 +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 1jVxIh-0001Hw-VP; Tue, 05 May 2020 14:07:55 +0100
8 Received: from mail-dm6nam11on2111.outbound.protection.outlook.com
9 ([40.107.223.111] helo=NAM11-DM6-obe.outbound.protection.outlook.com)
10 by libre-soc.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
11 (Exim 4.89) (envelope-from <yimmanuel3@gatech.edu>)
12 id 1jVxIg-0001Hq-2x
13 for libre-riscv-dev@lists.libre-riscv.org; Tue, 05 May 2020 14:07:54 +0100
14 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none;
15 b=HCjnLyjfK02XeQwFGAVvlaMsOe5kpvlGkyKBKyI/vpEC105jgheug61ZD5w4nZvxJEv6U3k85EQAXm64J5AdfI8tzANFTyTydrN/2aVw/tMbIvCaLTBIUNZUYRTiRBjnJfR0bEqGAI9lczH9g26P2JwssNGSiEyDe0BPids/4FsDWD7evuV8S01ux0wIG7TzcQ0mS8wlZYbZASQDN3fRKkZut1g6890DS+/fJrDDCY0pM+4rLNqL6r4hxcdJbjTbgLzhK6d8iJFuBTi1cTswUbmHvHyS1cW39D4FAM2EAS6274ysWRXYzl15XCZUrlKUqbAMdxIkvw6vZCH9k7y1wQ==
16 ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com;
17 s=arcselector9901;
18 h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck;
19 bh=7DFsNrDtadDAIkuokLPFk3ri6PmcYDfVHMD6+Fmtleo=;
20 b=MZf7d8OLiv1LLPoGouvT2AyqYpV2CUQHaKzd0noCUuD3EeoQeEO+A1xkOtklEoh79VqtjgXONi0ewFqstekhQjy+etmK7LUOeLF6JIwMA+Q9/QnG542uT67fmTvVaEvPvSVGaG3v8HLURyKm3WX+gcv12myf+tayxOTakLomi+k0WyaTTG8+aWVs9x5e9g4KPqGRwG9aAKCw4isFoFTymn1flsFcZ1dGPkm8ZUXZhjFM/LGEL4+GkEBrdC4V/NNJyqPW5xjGbrWVBiB+7fSOlZ+hFN7Bz5WuwonPnA66UyfPmS3/rCXbF3O0DCaBhmse0RWY3zo67rtH96myp9Inww==
21 ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass
22 smtp.mailfrom=gatech.edu; dmarc=pass action=none header.from=gatech.edu;
23 dkim=pass header.d=gatech.edu; arc=none
24 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gatech.edu;
25 s=selector1;
26 h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck;
27 bh=7DFsNrDtadDAIkuokLPFk3ri6PmcYDfVHMD6+Fmtleo=;
28 b=lMrEcresH5fdNeuRzdpxe/Yw9jxCBVih99Xr6y5ZsCJbg5n0VGuk10hp+5Hh3z1j/lQnibRQbHMYQvzFUCmuobYun39O98673qJgCzgar/48K6wXOc5fA9GHhcPrex6wtEMK26lsH86xTQwwXE5Zd5/KEfNtW4P3Q2MiCEb3Rik=
29 Authentication-Results: lists.libre-riscv.org; dkim=none (message not signed)
30 header.d=none; lists.libre-riscv.org;
31 dmarc=none action=none header.from=gatech.edu;
32 Received: from BL0PR07MB3908.namprd07.prod.outlook.com (2603:10b6:207:3f::14)
33 by BL0PR07MB5396.namprd07.prod.outlook.com (2603:10b6:208:47::22)
34 with Microsoft SMTP Server (version=TLS1_2,
35 cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2958.19; Tue, 5 May
36 2020 13:07:51 +0000
37 Received: from BL0PR07MB3908.namprd07.prod.outlook.com
38 ([fe80::bc9c:c809:95a2:527c]) by BL0PR07MB3908.namprd07.prod.outlook.com
39 ([fe80::bc9c:c809:95a2:527c%7]) with mapi id 15.20.2958.027; Tue, 5 May 2020
40 13:07:51 +0000
41 From: Yehowshua <yimmanuel3@gatech.edu>
42 Date: Tue, 5 May 2020 09:07:50 -0400
43 References: <CAPweEDwbe8bVrqR9OpBYR-Xfp-K7XGi=YStbuF-s8jwU2z1O6w@mail.gmail.com>
44 To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
45 In-Reply-To: <CAPweEDwbe8bVrqR9OpBYR-Xfp-K7XGi=YStbuF-s8jwU2z1O6w@mail.gmail.com>
46 Message-Id: <A96607D2-362B-4720-B1FE-2C2BBACD472D@gatech.edu>
47 X-Mailer: Apple Mail (2.3608.80.23.2.2)
48 X-ClientProxiedBy: BN8PR12CA0028.namprd12.prod.outlook.com
49 (2603:10b6:408:60::41) To BL0PR07MB3908.namprd07.prod.outlook.com
50 (2603:10b6:207:3f::14)
51 MIME-Version: 1.0
52 X-MS-Exchange-MessageSentRepresentingType: 1
53 Received: from yehowshuas-mbp.hsd1.ga.comcast.net (73.43.100.116) by
54 BN8PR12CA0028.namprd12.prod.outlook.com (2603:10b6:408:60::41) with Microsoft
55 SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id
56 15.20.2958.20 via Frontend Transport; Tue, 5 May 2020 13:07:51 +0000
57 X-Mailer: Apple Mail (2.3608.80.23.2.2)
58 X-Originating-IP: [73.43.100.116]
59 X-MS-PublicTrafficType: Email
60 X-MS-Office365-Filtering-Correlation-Id: 7a825a22-f05c-4497-eda5-08d7f0f55132
61 X-MS-TrafficTypeDiagnostic: BL0PR07MB5396:
62 X-Microsoft-Antispam-PRVS: <BL0PR07MB539607ED68A16A264175197CECA70@BL0PR07MB5396.namprd07.prod.outlook.com>
63 X-GT-Tenant: 042d12d7-75fe-4547-b5b6-0573f80f829d
64 X-MS-Oob-TLC-OOBClassifiers: OLM:8882;
65 X-Forefront-PRVS: 0394259C80
66 X-MS-Exchange-SenderADCheck: 1
67 X-Microsoft-Antispam: BCL:0;
68 X-Microsoft-Antispam-Message-Info: 6VJtPe9l9tgRKVEo5zXV87DNQFBQUu62OZd5ctcn9HAWVxGUwdXuSsm+onMGljPvskPU0lMlhm4mmIZTc7LuMVV9JGssQwQGrVR09ap86pJlIE4QsApx3IKUiOX7pUF0bcp92WHZjecpVZka7IkW7zp1AGFM+GaAA/945a5sUxf7J+FYFTkeFFO4Nz8Rcmi4Q0KOECfkQnWZJ0lQ/PjMmbBtENnONfRxknL+QMc7oArfnfR4XmcrWhtRWaxT9/hp/u0Mdck5H4pfzTVvamLCgnICHS2ywudFUbQF463I09DGZb3c0A+hs0W5bDID6yf3bLGn5uR15k2GgK8IyZ7gilaf0tTbhO636aH/TXbmVVYbpYV3GFvQ4mbB8soeMFsmVIJxomvD3mLMQOEXC9xyLPbuET+SmbaKAi1mf7dJZLu5c+ILATNm+4gPqTIu3J3M3v5TYaAskATk2Prn2A9Q9MCKaYcGXIob0g+ZClqPuaSBMtWYBRUO4ENeYNMfy8vHnJqp4a0yu+JJ26tJcFjgtE/uhpNJRJSGgFRa/okGu6bvG8NJJjeV6IZcI0bXhgu0
69 X-Forefront-Antispam-Report: CIP:255.255.255.255; CTRY:; LANG:en; SCL:1; SRV:;
70 IPV:NLI; SFV:NSPM; H:BL0PR07MB3908.namprd07.prod.outlook.com; PTR:; CAT:NONE;
71 SFTY:;
72 SFS:(4636009)(39860400002)(396003)(346002)(136003)(366004)(376002)(33430700001)(956004)(786003)(8676002)(316002)(8936002)(6486002)(6512007)(16526019)(26005)(186003)(478600001)(33964004)(52116002)(53546011)(36756003)(6506007)(66946007)(6916009)(66556008)(66476007)(33656002)(86362001)(2616005)(5660300002)(75432002)(2906002)(33440700001)(82953001);
73 DIR:OUT; SFP:1102;
74 X-MS-Exchange-AntiSpam-MessageData: OR8zO6/xR76i4jQMgoxR/Jl6yL1R7bGB+893Hsr86HsN0JeOYh8Bl/TNCXHZWkJ5MLpKWlAHxSy/ndPkKwnywWBaG8MSwT13aAPQ/oSXImMl+IDvLNpCCP/BqyklEfoBGVHl18O8+NqXn6zlyHiq4102lfbBD4PQ2XqYWrg3RtQqSI/4TMPeINGKoXcvI9be/CdcLSIExzuJT3vzDRv2ZzWMkUZoVolPYlgmEeb397fHQ8+A9FfXP5PcSWFRw5Jx8Qy8ZQFQBK2qNzA3jUSXM/iYyG8lNE+JOla/3NT3IvNt3aE23n8X8usabzlS9dKkV1+AqBfyI5Cp4dc20wKWxazXqH3004BBG8pFR64FsDIBJCHtw2MZEHIPZdKIBB9d3FQXOOV3GbLKZMgUXp+nzPF6Tnu+NNEhYTUml6yMGLn50DpCrxnR52M14cGMl5PHcF5ySu2DFmws666lLpEoXU15NJEWENla8ExaNrErafmp6iz1SMLg4aplItF4n5Xk1CiOTukeFxqb3GVoV6tuAuHqElDhByNuZVVb5xCY2HUv5w+51eZ5OweoWDap/c+ftbBdiBA2Os0/0DUlgfb7IofFHdVFDERqX78IJyyqnpbV45N6X3c0OFhBJjasNIyIBj3jmcQ/e9r0QEtAdU3Q2V7lvK9kAB4pbBaLTPFO2TkG+dN83IGaNgkJucVVWzlfqNPFOkn9ikRWM9P0adV1CDHVvPI+Tg6oWYs6uvr4jVLgs+t4a/l3Y256//469BMsg0k2T/y4zDGUD9+quWdkEduSkNPTB2qs0G6eWiRXBPc=
75 X-OriginatorOrg: gatech.edu
76 X-MS-Exchange-CrossTenant-Network-Message-Id: 7a825a22-f05c-4497-eda5-08d7f0f55132
77 X-MS-Exchange-CrossTenant-OriginalArrivalTime: 05 May 2020 13:07:51.7309 (UTC)
78 X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted
79 X-MS-Exchange-CrossTenant-Id: 482198bb-ae7b-4b25-8b7a-6d7f32faa083
80 X-MS-Exchange-CrossTenant-MailboxType: HOSTED
81 X-MS-Exchange-CrossTenant-UserPrincipalName: CRCCDw48ybCMb43IBE05Q84d1UvZXbnbwClvXGIIpRgQ1ySP2HC4lxWKXdyWeeexVdW+UnnwoGFuSIwKT4Y/ow==
82 X-MS-Exchange-Transport-CrossTenantHeadersStamped: BL0PR07MB5396
83 X-Content-Filtered-By: Mailman/MimeDel 2.1.23
84 Subject: Re: [libre-riscv-dev] daily status update 05may2020
85 X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
86 X-Mailman-Version: 2.1.23
87 Precedence: list
88 List-Id: Libre-RISCV General Development
89 <libre-riscv-dev.lists.libre-riscv.org>
90 List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>,
91 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
92 List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
93 List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
94 List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
95 List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>,
96 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
97 Reply-To: Libre-RISCV General Development
98 <libre-riscv-dev@lists.libre-riscv.org>
99 Content-Type: text/plain; charset="utf-8"
100 Content-Transfer-Encoding: base64
101 Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
102 Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
103
104 Cgo+IE9uIE1heSA1LCAyMDIwLCBhdCA2OjQ3IEFNLCBMdWtlIEtlbm5ldGggQ2Fzc29uIExlaWdo
105 dG9uIDxsa2NsQGxrY2wubmV0PiB3cm90ZToKPiAKPiBpdCB3b3VsZCBiZSBnb29kIGlmIGV2ZXJ5
106 b25lIGVsc2UgZGlkIGFzIHdlbGwsIGFzIHdlCj4gY2FuIGtlZXAgaW4gdG91Y2ggYW5kIHNlZSB3
107 aGF0J3MgZ29pbmcgb24uCgpJ4oCZbSB3b3JraW5nIG15IHdheSB0aHJvdWdoIHRoZSBjb2RlYmFz
108 ZSBhbmQgc2xvd2x5IGFkZGluZyBkb2N1bWVudGF0aW9uLgoKSSB3YXMgaGlyZWQgYnkgR2Vvcmdp
109 YSBUZWNoIHRvIHJldmlzZSBjcml0aWNhbCBwYXJ0cyBvZiB0aGUgQ29tcHV0ZXIgQXJjaGl0ZWN0
110 dXJlIGN1cnJpY3VsdW0gYW5kIEkgaGF2ZSB0byB3cml0ZSBteSBUaGVzaXMgdGhpcyBzdW1tZXIg
111 LSBhYm91dCAxNCBob3VycyBhIGRheSAtIHNvIHllYWggLSBzbG93bHkgZG9jdW1lbnRpbmcuCgpU
112 YWxraW5nIHRvIHNvbWUgbGF3eWVycyBhYm91dCBicmluZ2luZyBpbiB0aGUgTGlicmUtU09DIGFu
113 ZCBLYXphbiB0cmFkZW1hcmtzIHVuZGVyIFN5c3TDqG1lcyBMaWJyZXMuCgpBbHNvLCBkaXNjdXNz
114 aW5nIGVxdWl0eS4gSW5kaXZpZHVhbHMgd2hvIG1hZGUgY29udHJpYnV0aW9ucyB0byBMaWJyZS1T
115 T0MgaW4gdGhlIHBhc3QgYW5kIHdobyBjb250aW51ZSB0byBtYWtlIGNvbnRyaWJ1dGlvbnMgdW50
116 aWwgc2VlZC1mdW5kaW5nIG9mIFN5c3TDqG1lcyBMaWJyZXMgYXJlIGVsaWdpYmxlIGZvciBlcXVp
117 dHkgYWNjb3JkaW5nIHRvIHRoZSBTbGljaW5nIFBpZSBtb2RlbC4KClllaG93c2h1YQpfX19fX19f
118 X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fXwpsaWJyZS1yaXNjdi1kZXYg
119 bWFpbGluZyBsaXN0CmxpYnJlLXJpc2N2LWRldkBsaXN0cy5saWJyZS1yaXNjdi5vcmcKaHR0cDov
120 L2xpc3RzLmxpYnJlLXJpc2N2Lm9yZy9tYWlsbWFuL2xpc3RpbmZvL2xpYnJlLXJpc2N2LWRldgo=
121