[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / 34 / d2d5ed61f57a5a0f0c821f9ee26495618f68ca
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 19:19:00 +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 1jW29j-0005aZ-CY; Tue, 05 May 2020 19:18:59 +0100
8 Received: from mail-co1nam11on2101.outbound.protection.outlook.com
9 ([40.107.220.101] helo=NAM11-CO1-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 1jW29i-0005Yh-65
13 for libre-riscv-dev@lists.libre-riscv.org; Tue, 05 May 2020 19:18:58 +0100
14 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none;
15 b=iAW1aN7U/smvhyAQTRA+eD/+AjwW4uBFsNGi5V9UxVqY6mBT5YLJ4AH9zrKgV6Pgru/E9JxYwGtX7sV3j8kiJUogauIInCHspOt9HXIsLykdf5Snzpyi+UzTEtxGCkQrvld8i6nep6N6g8NqTHMSA+1ZVFmfoW/1y76le6awFYLVbC2DsQ3kVpFU/GRVRuSTqsU62dkEYcl2pleILpVuiRlREbHNmt+3fC/OtQ2+uyFZTkhRC1JT7jBMzE7pVhNuAcwj7FuCOxYsdXOp0TpivWaWm3rdLsqf8psH4a+IvzD8cgYTy01Sfs1nS2yC7BhnQVDWMtCdsN6k5UWNWcQaRg==
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=S3p6ysiLVxORHfGgb/Dtew6MZpA/UIU/mtYsoB+oD2U=;
20 b=F/+Qwc2dqNPIvdufbUSj7PBTxMXykWG/ADBEHWIu44hb21hlyPRSq7nZvs4XoXH1V9G6l9H4vxAlnn1Ibttd3oBgpInR2ca+ZgVRa/VHomCPxfwJk4egqogNBIzCshq/LteLB2b178Aj9LMY8R48QHwDvijQ6rGxWVX3Uxr9p63MQJ+HX6fxbYWfZnvUcbxine1P7jHJ2FKZDRFhLlhjPMKOagamOPDYEtd+Qbxh6fxFEkbDP7kIwesSxIGY8+aMr6bsp2nTG4OCL7Nfv2kUeGER6czCDAppkA4xarcARMwzjGbp48zkt8GLJeE+byogL93o58uGclFSD5hhqSzqfQ==
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=S3p6ysiLVxORHfGgb/Dtew6MZpA/UIU/mtYsoB+oD2U=;
28 b=wgaMCdUVDby2RyWyhtGnx9Gng5VvvJJvTL1eB2JMsIV2voxTiL+IYbLtyviPD5QCot1iyQPa5+jZtQgUmwh4RJO85D/Gi4hDpjmBNlSb2vHWc5OTBEoVrnACPpKmsFBIF90/i8ql8yZuT4G0y+JcgMa6BPmKYSbAVCMfK50kUC0=
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 BL0PR07MB5012.namprd07.prod.outlook.com (2603:10b6:208:4d::15)
34 with Microsoft SMTP Server (version=TLS1_2,
35 cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2958.20; Tue, 5 May
36 2020 18:18:52 +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 18:18:52 +0000
41 From: Yehowshua <yimmanuel3@gatech.edu>
42 Date: Tue, 5 May 2020 14:18:51 -0400
43 In-Reply-To: <CAPweEDxJ1HYkOYcn58jUtuUjz6q2jossMdRw54xhN4aANkW0mQ@mail.gmail.com>
44 Cc: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
45 References: <74E24B62-C4E6-4F95-88AC-DE45C5117D88@gatech.edu>
46 <CAPweEDxJ1HYkOYcn58jUtuUjz6q2jossMdRw54xhN4aANkW0mQ@mail.gmail.com>
47 Message-Id: <690DF9FB-783E-49DB-9D86-0233D34F57B8@gatech.edu>
48 X-Mailer: Apple Mail (2.3608.80.23.2.2)
49 X-ClientProxiedBy: BN3PR03CA0087.namprd03.prod.outlook.com
50 (2a01:111:e400:7a4d::47) To BL0PR07MB3908.namprd07.prod.outlook.com
51 (2603:10b6:207:3f::14)
52 MIME-Version: 1.0
53 X-MS-Exchange-MessageSentRepresentingType: 1
54 Received: from yehowshuas-mbp.hsd1.ga.comcast.net (73.43.100.116) by
55 BN3PR03CA0087.namprd03.prod.outlook.com (2a01:111:e400:7a4d::47) with
56 Microsoft SMTP Server (version=TLS1_2,
57 cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2958.20 via Frontend
58 Transport; Tue, 5 May 2020 18:18:52 +0000
59 X-Mailer: Apple Mail (2.3608.80.23.2.2)
60 X-Originating-IP: [73.43.100.116]
61 X-MS-PublicTrafficType: Email
62 X-MS-Office365-Filtering-Correlation-Id: 809587cc-a7d0-494c-27f9-08d7f120c3d0
63 X-MS-TrafficTypeDiagnostic: BL0PR07MB5012:
64 X-Microsoft-Antispam-PRVS: <BL0PR07MB50127C2C2A4AB9FAA8BF8897ECA70@BL0PR07MB5012.namprd07.prod.outlook.com>
65 X-GT-Tenant: 042d12d7-75fe-4547-b5b6-0573f80f829d
66 X-MS-Oob-TLC-OOBClassifiers: OLM:8273;
67 X-Forefront-PRVS: 0394259C80
68 X-MS-Exchange-SenderADCheck: 1
69 X-Microsoft-Antispam: BCL:0;
70 X-Microsoft-Antispam-Message-Info: p7vfYO8KCe2IG66AEqnrxcQ7tTI7sY3rAYZac/2NBmQZIbzL/Wlwhugz8EF/wLrcwkP69ELCesyCRxWZbNjrEE/Wu4k6OjtWm0MpNm92zrxj7kW22/1zIilnGbedotOJC4lTESyE2FLn1l3hFpFrzQNJrlt/rKfFpe0+Q9DEqS4kD8t+/aUWPCqlYwBqWqUBnjl7lywx3VefS4K4NNduI4W26psNGAMaDdoVfj/Mxp/FE2xlPCO3OTCEoVg8U6Ted4SjnMG4QuaakNXd8m8QKdkKFNR1FHx2PDTFXsqg+R2YMTlk68qF6fTDCKF3668Ko0yP55SDnn67BbpapmbOOlUNsHLYvRzkuiy/NGQAZqAKBGKwmBi5faD0UGYqmYzRqPdaOnH0c3qVMKugwb8nLTlv2w93ihlEozYy6twVXdTlL/Qs2fhs4nW2nLlU2kv6zF+Kpq/dCVHBVz5MWVC+BXqyn2Aj7MKL9d5qThfsNt+PH55nAyahScSG1fJVLseiXeTvoke443CDIdScKGf4cg==
71 X-Forefront-Antispam-Report: CIP:255.255.255.255; CTRY:; LANG:en; SCL:1; SRV:;
72 IPV:NLI; SFV:NSPM; H:BL0PR07MB3908.namprd07.prod.outlook.com; PTR:; CAT:NONE;
73 SFTY:;
74 SFS:(4636009)(39860400002)(396003)(366004)(376002)(346002)(136003)(33430700001)(6486002)(4326008)(86362001)(66946007)(66556008)(66476007)(316002)(6506007)(36756003)(786003)(8676002)(2906002)(4744005)(2616005)(956004)(8936002)(52116002)(5660300002)(478600001)(186003)(3480700007)(75432002)(16526019)(33656002)(7116003)(109986005)(33440700001)(26005)(6512007);
75 DIR:OUT; SFP:1102;
76 X-MS-Exchange-AntiSpam-MessageData: y4NUPgQ8HWT7rn9Ey3zpy2a2nd+fGM6/jQeTU63jaFHW5VOrdm8c0q0lgyjQeCKloLiVMNvllOmGVh+hzuhg9DVg1BHp/FwleVS30nbENeI6N3NBE42SbcwceTVSBzmM9SyYD1wiMOqUUFQPUUmj0RtWCvTFlMy6HFKZBR6VGozdaYaof8/l58/acnX6tuntNT8iZOvtVAbe3V8AFhS7JDRqmwl2zjf0qmfuNxos/dSAHZI9HSpqK6jfq8nmsBcGbCmVPZp1WoqIFypphggKcy7GczceikM7veZw6NvfFlic9Gwcu0OC0lvaJutXbgaROx8vO0nY9h5HhaC1lw8KTvEQAhFctMTM1sxDqMivcQTXopNyuOey0wAQ++UPZQO3R6vjsoDc91HZafn0YqH8wiy3PmH+oq8XIwXJHeNdCY/m0bmJzvzB1o6mzeZ6s+V4NMVE3MMPVrm935OzYYaDiMkgeNJjcM3X4ERNEfyBh5LBlJCfHBJElRI7m/Dsrpc3Dqhw06DjK8q9jOqf4X7nYA1eQ29BDOwMYV/4SGjGCmxylGEkdN5Vdqe/cyWM7EovxZwCyBC7kCJjn6fN/TEolqvqPU8YTY9QVqx9irIsUQskLX1xuJCdeizp5WEUUKH0AXZYi6iLHKyCRyu1xEJqgtRpQeYsay87d7Lf6qyfLUwLR8oJtRZI5tHxDleC5AiTDrfa+loZCEAU899jKKwMocIonR8rwNNkQjX3M0FzFNkl5zrv2SvJCLJktkBemPFxlBx8hxx7f3fzCOycbDLr3e0vrHYMrtXKT3AaQAtVeBg=
77 X-OriginatorOrg: gatech.edu
78 X-MS-Exchange-CrossTenant-Network-Message-Id: 809587cc-a7d0-494c-27f9-08d7f120c3d0
79 X-MS-Exchange-CrossTenant-OriginalArrivalTime: 05 May 2020 18:18:52.4779 (UTC)
80 X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted
81 X-MS-Exchange-CrossTenant-Id: 482198bb-ae7b-4b25-8b7a-6d7f32faa083
82 X-MS-Exchange-CrossTenant-MailboxType: HOSTED
83 X-MS-Exchange-CrossTenant-UserPrincipalName: 4/svJHDaRGVuilzkbF6HhUJD/S2eYNlTuUFpA4t5dPtNxT101SycDBkaApJYEaraUSo8G28AcbpHh8MD459MVg==
84 X-MS-Exchange-Transport-CrossTenantHeadersStamped: BL0PR07MB5012
85 Subject: Re: [libre-riscv-dev] Finished Scoreboard
86 X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
87 X-Mailman-Version: 2.1.23
88 Precedence: list
89 List-Id: Libre-RISCV General Development
90 <libre-riscv-dev.lists.libre-riscv.org>
91 List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>,
92 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
93 List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
94 List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
95 List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
96 List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>,
97 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
98 Reply-To: Libre-RISCV General Development
99 <libre-riscv-dev@lists.libre-riscv.org>
100 Content-Type: text/plain; charset="utf-8"
101 Content-Transfer-Encoding: base64
102 Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
103 Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
104
105 V2VsbCBJ4oCZZCBsaWtlIHRvIGJlIHJlYWxpc3RpYy4gSeKAmXZlIGRvbmUgbGFyZ2UgUlRMIHBy
106 b2plY3RzIGJlZm9yZSAtIGlmIHRoZSBzY29yZWJvYXJkIGlzbuKAmXQgcmVhZHkgdG8gZG8gYnkg
107 SnVuZSwgd2UgbWF5IGhhdmUgdG8gbG9vayBpbnRvIHRoZSBtaW5pbXVtIHZpYWJsZSBwcm9kdWN0
108 IGZvciBPY3RvYmVyLiBIYXZpbmcgYSBtdWx0aSBjeWNsZSBub24tcGlwZWxpbmVkIENQVSBpcyB3
109 YXkgYmV0dGVyIHRoYW4gbm8gQ1BVLgoKTHVrZSwgZ2l2ZW4gb25seSB5b3UgaGF2ZSB0aGUga25v
110 d2xlZGdlIHRvIGRvIHRoZSBTY29yZWJvYXJkIGF0IHRoZSBtb21lbnQsIGl04oCZZCBiZSB3aXNl
111 IHRvIHB1dCBlZ2dzIGluIG1vcmUgdGhhbiBvbmUgYmFza2V0LiBBbHNvLCBpdCB0YWtlcyBhdCBs
112 ZWFzdCBhIHNlbWVzdGVyIHRvIGZ1bGx5IGNvbXByZWhlbmQgdGhlIHNjb3JlYm9hcmQgYXJjaGl0
113 ZWN0dXJlLCBzbyB3ZSBjYW7igJl0IGp1c3QgYWRkIHBlb3BsZSB0byBoZWxwIHlvdS4KCkp1c3Qg
114 c29tZSB0aGluZ3MgdG8ga2VlcCBpbiBtaW5kLgoKWWVob3dzaHVhCl9fX19fX19fX19fX19fX19f
115 X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fCmxpYnJlLXJpc2N2LWRldiBtYWlsaW5nIGxp
116 c3QKbGlicmUtcmlzY3YtZGV2QGxpc3RzLmxpYnJlLXJpc2N2Lm9yZwpodHRwOi8vbGlzdHMubGli
117 cmUtcmlzY3Yub3JnL21haWxtYW4vbGlzdGluZm8vbGlicmUtcmlzY3YtZGV2Cg==
118