[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline
[libre-riscv-dev.git] / 47 / ac0d26aef7869c0b15d26b97ef1613dc152f9a
1 Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
2 Envelope-to: publicinbox@libre-riscv.org
3 Delivery-date: Wed, 15 Apr 2020 19:04:15 +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 1jOmOU-0006AU-TG; Wed, 15 Apr 2020 19:04:14 +0100
8 Received: from mail-pg1-f177.google.com ([209.85.215.177])
9 by libre-soc.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
10 (Exim 4.89) (envelope-from <colepoirier@gmail.com>)
11 id 1jOmOS-0006AH-UV
12 for libre-riscv-dev@lists.libre-riscv.org; Wed, 15 Apr 2020 19:04:13 +0100
13 Received: by mail-pg1-f177.google.com with SMTP id p8so290827pgi.5
14 for <libre-riscv-dev@lists.libre-riscv.org>;
15 Wed, 15 Apr 2020 11:04:12 -0700 (PDT)
16 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
17 h=date:from:to:cc:message-id:in-reply-to:references:subject
18 :mime-version:content-transfer-encoding:content-disposition;
19 bh=XWi0vns4iv1Lw0U0Oa42xZK7GVKjEndvVYK47ve+8nE=;
20 b=vOGlAySs4GYIUAPrRNZmk08sVOCbkBEfKMTBq0QDXYzyPyFA8ZcOCxmbxGELtaPTSH
21 Bp1sPB7Z/vBZIwj7mITDcNUcr2ag5PPXYthU0QLgkOQFke81vzzxkFYLG7pLulUPiH9q
22 eqZTjxireNYIGAkjH+H8i5Bji0xa6wT41e7RO2spJdbuu3uvb8j6h9pPvASv5sZYtnTM
23 fYk1iJkpTJjOznC7RbkMN3pzXiIn6rpjdJW+841nw4KD/Yp0zZma9n0GMKdHXsBpu14G
24 4UDYN+Tp+G1lOtPdADXAH5X+rDnxbnaQ3FqKFC4gDEJ+FkdZlxb+v0jDLH6ICqxW6ySD
25 FPkw==
26 X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
27 d=1e100.net; s=20161025;
28 h=x-gm-message-state:date:from:to:cc:message-id:in-reply-to
29 :references:subject:mime-version:content-transfer-encoding
30 :content-disposition;
31 bh=XWi0vns4iv1Lw0U0Oa42xZK7GVKjEndvVYK47ve+8nE=;
32 b=Khrvmca0BIYemnS1K3hc7HcSOfy5/h94aoMF5nwhzXDkL0CFVsib9E15/14tOioy/Y
33 RfWJMj4vJqp5F5x/Svma/B2kGUm5IDIWiZHR+7AWatRQ3hY5ZtC6fzhxUk78QqF7oDgU
34 pnOdsEUT6Q6R6qjTmArZyFsLqEzxWsxz9ox3STX/L/1TJLN2a1nivkmzdMHVRMIog2P0
35 3JF7xoJDNnAr+DW3AqLKoSuPX6omNeg2E+Z1EZpQ9Vp+E3nmcuHOGTRTOFvg1yv9YHGZ
36 THwbOaqXEWTr1vzjJroFkE8yFqOd96ytxnglAxvjwCRvqqsRRHxkU5dpu7zGYN79lC44
37 p6FA==
38 X-Gm-Message-State: AGi0Pua5ipbfjfIs25KwFqaJd8mypwcMa6NHpYhI4d5gOHQFyJdRiVa4
39 q+2yBxpTRxOgI9+WX4R0FVtNgL6FC3UGsQ==
40 X-Google-Smtp-Source: APiQypK28dN3OxawYhwekL60JozV1s3Ii763GC+NlUbWvQrZnJfMyqKCkvNfDSYG8KIiI+czi3gc4A==
41 X-Received: by 2002:a63:ec44:: with SMTP id r4mr26838125pgj.425.1586973850686;
42 Wed, 15 Apr 2020 11:04:10 -0700 (PDT)
43 Received: from cherrytree ([2604:3d08:4680:c200::f2b7])
44 by smtp.gmail.com with ESMTPSA id e135sm9743189pfh.37.2020.04.15.11.04.09
45 for <libre-riscv-dev@lists.libre-riscv.org>
46 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128);
47 Wed, 15 Apr 2020 11:04:09 -0700 (PDT)
48 Date: Wed, 15 Apr 2020 11:04:08 -0700
49 From: Cole Poirier <colepoirier@gmail.com>
50 To: Libre-RISCV General Development
51 <libre-riscv-dev@lists.libre-riscv.org>
52 Cc: "=?utf-8?Q?libre-riscv-dev=40lists.libre-riscv.org?="
53 <libre-riscv-dev@lists.libre-riscv.org>
54 Message-ID: <96A7CF85-69AD-43BA-80D8-C717E61C2FDD@getmailspring.com>
55 In-Reply-To: <bug-208-13-S4waoUKkxV@https.bugs.libre-soc.org/>
56 References: <bug-208-13-S4waoUKkxV@https.bugs.libre-soc.org/>
57 X-Mailer: Mailspring
58 MIME-Version: 1.0
59 Content-Disposition: inline
60 Subject: Re: [libre-riscv-dev] [Bug 208] implement CORDIC in a general way
61 sufficient to do transcendentals
62 X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
63 X-Mailman-Version: 2.1.23
64 Precedence: list
65 List-Id: Libre-RISCV General Development
66 <libre-riscv-dev.lists.libre-riscv.org>
67 List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>,
68 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
69 List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
70 List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
71 List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
72 List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>,
73 <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
74 Reply-To: Libre-RISCV General Development
75 <libre-riscv-dev@lists.libre-riscv.org>
76 Content-Type: text/plain; charset="utf-8"
77 Content-Transfer-Encoding: base64
78 Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
79 Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
80
81 T24gQXByIDE1IDIwMjAsIGF0IDEwOjU0IGFtLCBidWd6aWxsYS1kYWVtb25AbGlicmUtc29jLm9y
82 ZyB3cm90ZToKPiBodHRwczovL2J1Z3MubGlicmUtc29jLm9yZy9zaG93X2J1Zy5jZ2k/aWQ9MjA4
83 Cj4gCj4gLS0tIENvbW1lbnQgIzYgZnJvbSBNaWNoYWVsIE5vbGFuIDxtdG5vbGFuMjY0MEBnbWFp
84 bC5jb20+IC0tLQo+IChJbiByZXBseSB0byBMdWtlIEtlbm5ldGggQ2Fzc29uIExlaWdodG9uIGZy
85 b20gY29tbWVudCAjNSkKPj4gb2sgc28gd291bGQgeW91IGxpa2UgdG8gZG8gdGhlIG5leHQgc3Rl
86 cD8gd2hpY2ggaXMsIHllcCB5b3UgZ3Vlc3NlZCBpdDoKPj4gSUVFRTc1NCBGUCBzaW4gYW5kIGNv
87 cyA6KQo+IAo+IEknbSBub3QgcmVhbGx5IHN1cmUgaG93IHRvIGRvIHRoaXMgdGhvdWdoLiBJIGtu
88 b3cgeW91IGRpZCBhIHNpbWlsYXIKPiB0aGluZyBvbgo+IHRoZSBkaXZpZGVyLCBkaWQgeW91IGhh
89 bmRsZSBpdCBhcyBhIGZsb2F0IHRoZSBlbnRpcmUgd2F5IHRocm91Z2ggb3IKPiBjb252ZXJ0IGl0
90 Cj4gdG8gaW50ZWdlci4uLiBzb21laG93Pwo+IAo+IERvaW5nIGl0IGFzIGEgZmxvYXQgbWVhbnMg
91 dGhhdCB0aGUgYWRkZXJzL3N1YnRyYWN0b3JzIG5lZWQgdG8gYmUgZnVsbCBmbG9hdGluZwo+IHBv
92 aW50IGFkZGVycywgbGlrZSB0aG9zZSBpbiBmcGFkZC8sIHJpZ2h0PyAKPiAKPiBGb3IgY29udmVy
93 dGluZyB0aGUgaW5wdXRzIHRvIGludGVnZXJzLCBpdCBzZWVtcyBsaWtlIHRoZXJlIHdvdWxkIGJl
94 Cj4gaXNzdWVzIGFzCj4gdGhlIGlucHV0IGFuZ2xlIGFwcHJvYWNoZWQgMCAoYmVjYXVzZSBmbG9h
95 dHMgZ2l2ZSBtb3JlIHJlc29sdXRpb24KPiB0aGVyZSkuIENvbGUKPiBlbWFpbGVkIG1lIGEgcGFw
96 ZXIgKHdoaWNoIEkgbGlua2VkIHRvIGluIHRoZSByZXNvdXJjZXMgcGFnZSkgdGhhdAo+IGNvbnRh
97 aW5lZCBhCj4gaHlicmlkIGNvcmRpYyB0aGF0IHN3aXRjaGVkIHRvIGEgdGF5bG9yIHNlcmllcyBh
98 cHByb3hpbWF0aW9uIHdoZW4gdGhlIGlucHV0Cj4gYmVjYW1lIHNtYWxsIGVub3VnaC4gVGhpcyBz
99 ZWVtcyBsaWtlIGl0IG1pZ2h0IHdvcmsgcmVhc29uYWJseSB3ZWxsIGZvciBoYW5kbGluZwo+IHRo
100 ZSBzbWFsbCBpbnB1dCBjYXNlLiAKPiAKPiBUaG91Z2h0cz8KPgo+IE1pY2hhZWwKCkhlcmUncyB0
101 aGUgbGluayB0byB0aGUgcGFwZXIsIHdoaWNoIHlvdSd2ZSBsaW5rZWQgdG8gb24gdGhlIHJlc291
102 cmNlcwpwYWdlLiBJIGp1c3QgdGhvdWdodCBJJ2QgaW5jbHVkZSBpdCBpbiB0aGlzIGJ1Zy9tYWls
103 aW5nIGxpc3QgZm9yIGVhc2Ugb2YKYWNjZXNzOiAiTG93IExhdGVuY3kgYW5kIExvdyBFcnJvciBG
104 bG9hdGluZy1Qb2ludCBTaW5lL0Nvc2luZSBGdW5jdGlvbgpCYXNlZCBUQ09SRElDIEFsZ29yaXRo
105 bSIgKGh0dHBzOi8vaWVlZXhwbG9yZS5pZWVlLm9yZy9kb2N1bWVudC83Nzg0Nzk3KS4KRm9yIHBy
106 b2plY3QgbWVtYmVycyB0aGF0IGRvIG5vdCBoYXZlIElFRUUgZXhwbG9yZSBhY2Nlc3MsIHBsZWFz
107 ZSBlbWFpbApNaWNoYWVsIG9yIG15c2VsZiBvZmYtbGlzdC4KCkkgYWxzbyB0aGluayB0aGF0IHRo
108 aXMgcGFwZXIgbWF5IGJlIHJlbGV2YW50LCBob3dldmVyLCBJIGFtIG5vdCBlbnRpcmVseSBzdXJl
109 LgoiUGlwZWxpbmVkIFJhbmdlIFJlZHVjdGlvbiBCYXNlZCBUcnVuY2F0ZWQgTXVsdGlwbGllciIg
110 KGh0dHBzOi8vaWVlZXhwbG9yZS5pZWVlLm9yZy9kb2N1bWVudC85MDYyNjk3KS4KCkNvbGUKCgpf
111 X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fXwpsaWJyZS1yaXNj
112 di1kZXYgbWFpbGluZyBsaXN0CmxpYnJlLXJpc2N2LWRldkBsaXN0cy5saWJyZS1yaXNjdi5vcmcK
113 aHR0cDovL2xpc3RzLmxpYnJlLXJpc2N2Lm9yZy9tYWlsbWFuL2xpc3RpbmZvL2xpYnJlLXJpc2N2
114 LWRldgo=
115