[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / 2a / f46de17ad4920bf072739cc816e8f9e255511a
1 Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
2 Envelope-to: publicinbox@libre-riscv.org
3 Delivery-date: Tue, 31 Mar 2020 05:22:14 +0100
4 Received: from localhost ([::1] helo=libre-riscv.org)
5 by libre-riscv.org with esmtp (Exim 4.89)
6 (envelope-from <libre-riscv-dev-bounces@lists.libre-riscv.org>)
7 id 1jJ8Pl-0000a0-RR; Tue, 31 Mar 2020 05:22:13 +0100
8 Received: from mail-mw2nam12on2137.outbound.protection.outlook.com
9 ([40.107.244.137] helo=NAM12-MW2-obe.outbound.protection.outlook.com)
10 by libre-riscv.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
11 (Exim 4.89) (envelope-from <yimmanuel3@gatech.edu>)
12 id 1jJ8Pj-0000Zn-Sv
13 for libre-riscv-dev@lists.libre-riscv.org; Tue, 31 Mar 2020 05:22:12 +0100
14 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none;
15 b=keu86os91TUa2mf1/Z9KpARi8Zb9J+xoJ4VhG3icY24PNBl3EM5K89wIhpIze7Z/dVnfL5rQm8Y6nKMDXsc0FYfO+W8sybzHxWh963bUAusOQKt8a3SYXfK5KCMz1LQ0qkNeOVOaZR2gBms6tRKcQxb6l4KsN9syY3BJwXTh0rG/ymrV/uFxLuYW8Gpy13Ty0SFt0I/GFqbrF51QnsugLaHRIcljcmfEhpRfuIN/1FkLzCra1UvINNOxOlSVf6k9YtgzyRJd1E84QdC9wUHAVrBuxhuC1Wj5EgKrt/3J3owVqB0dvr7bJoDVu4UqkpYIxybAPuAiklz1HPSxXGX2dQ==
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=MvhNseS9zwF8VDxcA8z7jwO2iuuEHw3qeX4ABJn/o5k=;
20 b=kUIhe06ZDALtWv4vyXs1VUjllP3vmBqYp5YiljB/GWCrjBRqLIrrBkvyZ9tERviJnFHWe0M6DC0EEc96tUdWcf84wxEWzprWRm7pE0bofZmMMvdF3CHKLlQPpIsFGAix5SCE0Qs/zlXL5eFrSRs5vandrHyq/l8wwfoU8E2X5WFdGhPuCTStUhIZ7+sxYhDT5Qg7FIt9UUmQn3Bim0h43qtN3MMvEtc+oAxhDg5PSw1/Yq2pXP5pbcY70WnIqNoOE+VDMzXWyeiX8uj+aUxPqBk9dIIQL13+Rx+rn139S/PTJsbEt5Vk+yl4sBEtwFzA4ktY+nUDee5jAs4VV63RVA==
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=MvhNseS9zwF8VDxcA8z7jwO2iuuEHw3qeX4ABJn/o5k=;
28 b=xCf1GlzyfOEJaz8VXje6L2ZLPvz8fOP+lw+MP3vtjbwtcp3MXwuh+lxx14LMdl1c7gCnY9AYvFFUjUCAd7ZBhV3X6ZRKdxxzTn7xs1GfZPUN5gt9sbb3dKjkdTG11cUimi44MWy09F3FQuXE3oyxanuPZqhZwIlBRg19HJxqNnw=
29 Received: from BL0PR07MB3908.namprd07.prod.outlook.com (2603:10b6:207:3f::14)
30 by BL0PR07MB3875.namprd07.prod.outlook.com (2603:10b6:207:49::33)
31 with Microsoft SMTP Server (version=TLS1_2,
32 cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2856.18; Tue, 31 Mar
33 2020 04:21:45 +0000
34 Received: from BL0PR07MB3908.namprd07.prod.outlook.com
35 ([fe80::d040:4516:8c:de63]) by BL0PR07MB3908.namprd07.prod.outlook.com
36 ([fe80::d040:4516:8c:de63%5]) with mapi id 15.20.2856.019; Tue, 31 Mar 2020
37 04:21:45 +0000
38 From: "Immanuel, Yehowshua U" <yimmanuel3@gatech.edu>
39 To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
40 Thread-Topic: [libre-riscv-dev] Public Inbox
41 Thread-Index: AQHWBwW9pFtTZ4zih0WKYIFS3u045KhiDLkAgAALPICAAAEUAIAAALAA
42 Date: Tue, 31 Mar 2020 04:21:45 +0000
43 Message-ID: <09F31DD2-0026-44C7-B702-6E08CE1D5B7C@gatech.edu>
44 References: <C4191A74-A82F-42E8-A1F1-075EF9135D33@gatech.edu>
45 <CAPweEDwLo5gGn5E8mszQEYYBPbUJXgOEQTgXX7Ru1afEpGRVBA@mail.gmail.com>
46 <4C23AC26-6ECC-478D-B93E-A6C501F5AABD@gatech.edu>
47 <829465A0-552A-44CD-AED2-81E976D2191C@gatech.edu>
48 In-Reply-To: <829465A0-552A-44CD-AED2-81E976D2191C@gatech.edu>
49 Accept-Language: en-US
50 Content-Language: en-US
51 X-MS-Has-Attach:
52 X-MS-TNEF-Correlator:
53 x-mailer: Apple Mail (2.3608.60.0.2.5)
54 authentication-results: spf=none (sender IP is )
55 smtp.mailfrom=yimmanuel3@gatech.edu;
56 x-originating-ip: [2601:c9:8000:1266:2011:f22f:3129:866e]
57 x-ms-publictraffictype: Email
58 x-ms-office365-filtering-correlation-id: 27815215-620c-4ac5-101c-08d7d52b05be
59 x-ms-traffictypediagnostic: BL0PR07MB3875:
60 x-microsoft-antispam-prvs: <BL0PR07MB38754D62FDABC83AD812F53DECC80@BL0PR07MB3875.namprd07.prod.outlook.com>
61 x-gt-tenant: 042d12d7-75fe-4547-b5b6-0573f80f829d
62 x-ms-oob-tlc-oobclassifiers: OLM:1332;
63 x-forefront-prvs: 0359162B6D
64 x-forefront-antispam-report: CIP:255.255.255.255; CTRY:; LANG:en; SCL:1; SRV:;
65 IPV:NLI; SFV:NSPM; H:BL0PR07MB3908.namprd07.prod.outlook.com; PTR:; CAT:NONE;
66 SFTY:;
67 SFS:(10019020)(4636009)(396003)(366004)(39860400002)(136003)(376002)(346002)(316002)(186003)(71200400001)(786003)(4270600006)(6916009)(6512007)(33656002)(558084003)(2906002)(86362001)(2616005)(8936002)(478600001)(66446008)(66556008)(66476007)(36756003)(75432002)(81156014)(64756008)(6486002)(81166006)(5660300002)(6506007)(66946007)(76116006)(966005)(91956017)(8676002)(82953001)(584024005)(16725315012)(15302535012);
68 DIR:OUT; SFP:1102;
69 received-spf: None (protection.outlook.com: gatech.edu does not designate
70 permitted sender hosts)
71 x-ms-exchange-senderadcheck: 1
72 x-microsoft-antispam: BCL:0;
73 x-microsoft-antispam-message-info: jrhlFw5IWlQaJgha9tegK4PWwafTkzriyOjr8TYyYgBUFoO6FgCpnXRWaov9J04efuBUd+PD1hs55SVqLO6nW+axevrS3LksgEda2OmCdNY6fnA8WlMonmrLdT+PvJsff39yQK1/0DzQQQdg1ZajxF650l8T0JCtdR6Knxj+G2lPfNDmbWVj97qwAHIGXVhnU+DrJfwAaXHwSPVwdptx9Icy56Ue8uwTFdlHu2r9jPg14qMkTyA/bjqWJZ2rm/2CR2NHNwklJJSQbtE9YIoSuRzKFQ+eQqkyR0hRA2MZTzWJ2y1n/FtRM2kfPE0KATl2fNtEa8y1qtyZmwfQ9B322j+czRUagHZz9XF59EOiaoPtJJbN4LpYaq5ViF7XkeiuXCUqQDQ/UpwpfRAO3K+QdVnXc3+x+THpWmxQ9HbOh060NYTspnQZmEt3sAdfsMT8M31jy8ouiUTVZ9jHW9E/ioSXRRe+sN7xSc6imeNjvmCr2buKXdCWik5slu+qjqhmrxdwxDCrv9efwHXVUiYqBMkPNeGqADftfJEX2zL957zVXtYKyDzgTnlRreqpznyWhOBH5CawXUDCMKXWAvcJRxFHp2+Ou0LyaKHisBDLjQPr84RasldFJh3Pdk+xMKE3QHFBgacTN2mPSX5RyJE5AZqgO7yX5+qXzi0GYVeapZ0=
74 x-ms-exchange-antispam-messagedata: 5DY8pGSlkhBIOntv890Apo8b4PJxbBU+g2zQve2Q9ZgooAz/opcvgEEV4COluL+GcxJk8EUT1XENe1uJyUrAF5zBWd5epeqV5fA2x7DDkwVJ53B9YdV2fnHdMz4OGn4UtARxTT2hkl3SK8gJcYU6aDX20ykBAudvKOksGJBmPtOHiXTXANm+H2DXNdiD2nVcsFrlkEdhhD1NJaiPvvQz9g==
75 x-ms-exchange-transport-forked: True
76 Content-ID: <18B93C2A771F004991485B7FA81BB7FA@namprd07.prod.outlook.com>
77 MIME-Version: 1.0
78 X-OriginatorOrg: gatech.edu
79 X-MS-Exchange-CrossTenant-Network-Message-Id: 27815215-620c-4ac5-101c-08d7d52b05be
80 X-MS-Exchange-CrossTenant-originalarrivaltime: 31 Mar 2020 04:21:45.0407 (UTC)
81 X-MS-Exchange-CrossTenant-fromentityheader: Hosted
82 X-MS-Exchange-CrossTenant-id: 482198bb-ae7b-4b25-8b7a-6d7f32faa083
83 X-MS-Exchange-CrossTenant-mailboxtype: HOSTED
84 X-MS-Exchange-CrossTenant-userprincipalname: 7QrLaPh04gk+CEomUKkVNJs4yOI2o39COd/XdJLGAg8x9wyQ1evUrcCDcTytx1GIEoYVyislfiIF/jrK+slpRA==
85 X-MS-Exchange-Transport-CrossTenantHeadersStamped: BL0PR07MB3875
86 Subject: Re: [libre-riscv-dev] Public Inbox
87 X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
88 X-Mailman-Version: 2.1.23
89 Precedence: list
90 List-Id: Libre-RISCV General Development
91 <libre-riscv-dev.lists.libre-riscv.org>
92 List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>,
93 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
94 List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
95 List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
96 List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
97 List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>,
98 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
99 Reply-To: Libre-RISCV General Development
100 <libre-riscv-dev@lists.libre-riscv.org>
101 Content-Type: text/plain; charset="utf-8"
102 Content-Transfer-Encoding: base64
103 Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
104 Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
105
106 T2guIEkgZm91bmQgaXQuCgpodHRwOi8vaW5ib3gubGlicmUtcmlzY3Yub3JnL2xpYnJlLXJpc2N2
107 LWRldi9uZXcuaHRtbAoKX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f
108 X19fX18KbGlicmUtcmlzY3YtZGV2IG1haWxpbmcgbGlzdApsaWJyZS1yaXNjdi1kZXZAbGlzdHMu
109 bGlicmUtcmlzY3Yub3JnCmh0dHA6Ly9saXN0cy5saWJyZS1yaXNjdi5vcmcvbWFpbG1hbi9saXN0
110 aW5mby9saWJyZS1yaXNjdi1kZXYK
111