Re: [libre-riscv-dev] Using formal to expose bugs in scoreboard

diff --git a/4a/59d8d434a6dc73976563490a8d9aa8bddd95fa b/4a/59d8d434a6dc73976563490a8d9aa8bddd95fa
new file mode 100644 (file)
index 0000000..06a9ed5
--- /dev/null
+++ b/4a/59d8d434a6dc73976563490a8d9aa8bddd95fa
@@ -0,0 +1,120 @@
+Return-path: <libre-riscv-dev-bounces@lists.libre-riscv.org>
+Envelope-to: publicinbox@libre-riscv.org
+Delivery-date: Mon, 08 Jun 2020 10:41:02 +0100
+Received: from localhost ([::1] helo=libre-riscv.org)
+       by libre-soc.org with esmtp (Exim 4.89)
+       (envelope-from <libre-riscv-dev-bounces@lists.libre-riscv.org>)
+       id 1jiEH7-0001vA-Ub; Mon, 08 Jun 2020 10:41:01 +0100
+Received: from lkcl.net ([217.147.94.29])
+ by libre-soc.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
+ (Exim 4.89) (envelope-from <lkcl@lkcl.net>) id 1jiEH6-0001v1-FZ
+ for libre-riscv-dev@lists.libre-riscv.org; Mon, 08 Jun 2020 10:41:00 +0100
+DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=lkcl.net;
+ s=201607131; 
+ h=Content-Type:To:Subject:Message-ID:Date:From:In-Reply-To:References:MIME-Version;
+ bh=mXh753WbiVlTmX6p8PuHkkE1nIe+eEExa/3U7bjPh4o=; 
+ b=QRR0peshI+xe/SPawi+UeyGVEY0LowsCw30KL85hkD4gcGS8kEAlznNfDD3yCYH+9uivPJ2DxLKZzOzz52f0xfhRqGbaU2y+TDfRiz5/u474FZc2rDT9+tJAFVDBTWREnRN3+J8gUNtwLrhEwbomiAsa0cQEB4bhyo4snQA+3cE=;
+Received: from mail-lj1-f179.google.com ([209.85.208.179])
+ by lkcl.net with esmtpsa (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
+ (Exim 4.84_2) (envelope-from <lkcl@lkcl.net>) id 1jiEH6-0007jN-36
+ for libre-riscv-dev@lists.libre-riscv.org; Mon, 08 Jun 2020 09:41:00 +0000
+Received: by mail-lj1-f179.google.com with SMTP id 9so19596731ljc.8
+ for <libre-riscv-dev@lists.libre-riscv.org>;
+ Mon, 08 Jun 2020 02:40:44 -0700 (PDT)
+X-Gm-Message-State: AOAM530EF52FH+lQMIsk97V8jYuo6dFFROQuH/Pae2+8urHmE3Wmy4Wq
+ 0b+CjMF281cfKeDKJCdRD+c5wVrYT4OaxKU3uXo=
+X-Google-Smtp-Source: ABdhPJx9L1Rwvx9ujMLHypoPqaU2EP8ATR4t5mf///RSTCK22BZBKuB/OLzuh/SDe+OitypsRJZJskjFb3h0UDWrmvY=
+X-Received: by 2002:a2e:8890:: with SMTP id k16mr678322lji.161.1591609239117; 
+ Mon, 08 Jun 2020 02:40:39 -0700 (PDT)
+MIME-Version: 1.0
+References: <E2E475D2-7421-4970-92BE-146FC5514AA5@gatech.edu>
+In-Reply-To: <E2E475D2-7421-4970-92BE-146FC5514AA5@gatech.edu>
+From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
+Date: Mon, 8 Jun 2020 10:40:27 +0100
+X-Gmail-Original-Message-ID: <CAPweEDzJv5zevxpd_tz1soxMhv+1sPKnCFjKHYPMH36b1VNLEA@mail.gmail.com>
+Message-ID: <CAPweEDzJv5zevxpd_tz1soxMhv+1sPKnCFjKHYPMH36b1VNLEA@mail.gmail.com>
+To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
+Subject: Re: [libre-riscv-dev] Using formal to expose bugs in scoreboard
+X-BeenThere: libre-riscv-dev@lists.libre-riscv.org
+X-Mailman-Version: 2.1.23
+Precedence: list
+List-Id: Libre-RISCV General Development
+ <libre-riscv-dev.lists.libre-riscv.org>
+List-Unsubscribe: <http://lists.libre-riscv.org/mailman/options/libre-riscv-dev>, 
+ <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=unsubscribe>
+List-Archive: <http://lists.libre-riscv.org/pipermail/libre-riscv-dev/>
+List-Post: <mailto:libre-riscv-dev@lists.libre-riscv.org>
+List-Help: <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=help>
+List-Subscribe: <http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev>, 
+ <mailto:libre-riscv-dev-request@lists.libre-riscv.org?subject=subscribe>
+Reply-To: Libre-RISCV General Development
+ <libre-riscv-dev@lists.libre-riscv.org>
+Content-Type: text/plain; charset="utf-8"
+Content-Transfer-Encoding: base64
+Errors-To: libre-riscv-dev-bounces@lists.libre-riscv.org
+Sender: "libre-riscv-dev" <libre-riscv-dev-bounces@lists.libre-riscv.org>
+
+T24gTW9uLCBKdW4gOCwgMjAyMCBhdCA0OjExIEFNIFllaG93c2h1YSA8eWltbWFudWVsM0BnYXRl
+Y2guZWR1PiB3cm90ZToKPgo+IFRoaXMgZXJyb3IgaGlnaGxpZ2h0cyB0aGUgbmVlZCBmb3IgZm9y
+bWFsIG9uIHRoZSBzY29yZWJvYXJkLgoKdGhpcyBleGFjdCBuZWVkIHdhcyB0YWtlbiBpbnRvIGNv
+bnNpZGVyYXRpb24gd2hlbiB0aGUgYXBwbGljYXRpb24gZm9yCk5MTmV0IEZ1bmRpbmcgZm9yIHRo
+ZSBGb3JtYWwgQ29ycmVjdG5lcyBQcm9vZnMgd2FzIG1hZGUsIGEgeWVhciBhZ28uCmh0dHBzOi8v
+YnVncy5saWJyZS1zb2Mub3JnL3Nob3dfYnVnLmNnaT9pZD04MQoKYXMgaXQgaXMgY3JpdGljYWxs
+eSBpbXBvcnRhbnQgYSBidWRnZXQgb2YgRVVSIDUsMDAwIHdhcyBhbGxvY2F0ZWQganVzdAp0byB0
+aGlzICpvbmUqIHRhc2s6Cmh0dHBzOi8vYnVncy5saWJyZS1zb2Mub3JnL3Nob3dfYnVnLmNnaT9p
+ZD0xOTcKCm1pY2hhZWwgYmVnYW4gYSBGb3JtYWwgQ29ycmVjdG5lc3MgUHJvb2YgZm9yIHRoZSBN
+dWx0aUNvbXBVbml0IG9uIHRoZQoyNHRoIG9mIE1heToKaHR0cHM6Ly9idWdzLmxpYnJlLXNvYy5v
+cmcvc2hvd19idWcuY2dpP2lkPTM0MgoKdGhhdCBDb3JyZWN0bmVzcyBQcm9vZiBpcyBkZXNpZ25l
+ZCB0byBjb21wbGVtZW50IHRoZSBidWdyZXBvcnQgdGhhdAp5b3UgcmVmZXJlbmNlZCAoc2VlIGZ1
+cnRoZXIgYmVsb3cpCmh0dHBzOi8vYnVncy5saWJyZS1zb2Mub3JnL3Nob3dfYnVnLmNnaT9pZD0z
+MzYjYzU0CgpTYW11ZWwgRmFsdm8ncyB3b3JrIHdhcyB3aGF0IG9yaWdpbmFsbHkgaW5zcGlyZWQg
+dXMgdG8gdXNlIGEgaHlicmlkCmNvbWJpbmF0aW9uIG9mICJzaW1wbGUsIGNsZWFyLCB3ZWxsLWRv
+Y3VtZW50ZWQiIHVuaXQgdGVzdHMgcGx1cwpleHRlbnNpdmUgRm9ybWFsIENvcnJlY3RuZXNzIFBy
+b29mczoKaHR0cDovL2xpc3RzLmxpYnJlLXJpc2N2Lm9yZy9waXBlcm1haWwvbGlicmUtcmlzY3Yt
+ZGV2LzIwMTktQXVndXN0LzAwMjMxMS5odG1sCgphbHRob3VnaCBpIGNhbm5vdCBmaW5kIHRoZSBv
+cmlnaW5hbCBkaXNjdXNzaW9uLCBpdCBpcyBlbHNld2hlcmUgb24gdGhlCmludGVybmV0IHNldmVy
+YWwgbW9udGhzIHByaW9yIHRvIHRoZSBBdWcgMjAxOSBkaXNjdXNzaW9uLCBTYW11ZWwncwppbnNp
+Z2h0cyBzaG93ZWQgdXMgdGhhdCB3cml0aW5nIGNvbXByZWhlbnNpdmUgVW5pdCBUZXN0cyBzaW1w
+bHkgZG9lcwpub3QgY2F0Y2ggZXZlcnl0aGluZywgYW5kIGV2ZW4gaWYgZWZmb3J0cyBhcmUgbWFk
+ZSB0byB0cnkgdG8gZG8gc28gdGhlCnNoZWVyIHF1YW50aXR5IG9mIGNvZGUgaW52b2x2ZWQgbWFz
+a3MgZXJyb3JzLCBkaXN0cmFjdHMgZnJvbSB0aGUKYWN0dWFsIGNvZGUgYmVpbmcgdGVzdGVkLCBh
+bmQgZG9lc24ndCBjYXRjaCBhbGwgZXJyb3JzIGFueXdheS4KCnRoZSBJRUVFNzU0IEZQVSB0ZXN0
+cyBhcmUgYSBnb29kIGV4YW1wbGUuICB0aGlzIGlzIHRoZSBiYXNpYwppbmZyYXN0cnVjdHVyZSB0
+aGF0IGFsbG93cyBodW5kcmVkcyBvZiB0aG91c2FuZHMgb2YgcmFuZG9tIGFuZApyZWdyZXNzaW9u
+IHRlc3RzIHRvIGJlIGNhbGxlZDoKaHR0cHM6Ly9naXQubGlicmUtc29jLm9yZy8/cD1pZWVlNzU0
+ZnB1LmdpdDthPWJsb2I7Zj1zcmMvaWVlZTc1NC9mcGNvbW1vbi90ZXN0L2Nhc2VfZ2VuLnB5O2hi
+PUhFQUQKaHR0cHM6Ly9naXQubGlicmUtc29jLm9yZy8/cD1pZWVlNzU0ZnB1LmdpdDthPWJsb2I7
+Zj1zcmMvaWVlZTc1NC9mcGNvbW1vbi90ZXN0L2ZwbXV4LnB5O2hiPUhFQUQKCmFuZCBlYWNoIHBp
+cGVsaW5lIHRoZW4gY29udGFpbnMgc29tZXRpbWVzIHVwIHRvIDEwIHNlcGFyYXRlIHVuaXQgdGVz
+dHMKdG8gY292ZXIgZGlmZmVyZW50IGFzcGVjdHM6Cmh0dHBzOi8vZ2l0LmxpYnJlLXNvYy5vcmcv
+P3A9aWVlZTc1NGZwdS5naXQ7YT10cmVlO2Y9c3JjL2llZWU3NTQvZnBkaXYvdGVzdDtoYj1IRUFE
+Cmh0dHBzOi8vZ2l0LmxpYnJlLXNvYy5vcmcvP3A9aWVlZTc1NGZwdS5naXQ7YT1ibG9iO2Y9c3Jj
+L2llZWU3NTQvZnBtYXgvdGVzdC90ZXN0X2ZwbWF4X3BpcGUucHk7aGI9SEVBRApodHRwczovL2dp
+dC5saWJyZS1zb2Mub3JnLz9wPWllZWU3NTRmcHUuZ2l0O2E9dHJlZTtmPXNyYy9pZWVlNzU0L2Zw
+YWRkL3Rlc3Q7aGI9SEVBRApodHRwczovL2dpdC5saWJyZS1zb2Mub3JnLz9wPWllZWU3NTRmcHUu
+Z2l0O2E9dHJlZTtmPXNyYy9pZWVlNzU0L2ZwY21wL3Rlc3Q7aGI9SEVBRAoKbm9uZSBvZiB3aGlj
+aCAqYWN0dWFsbHkqIGdpdmVzIHVzIGZ1bGwgY29uZmlkZW5jZSBpbiB0aGUgY29kZSwgZGVzcGl0
+ZQp0YWtpbmcgYSB3ZWVrIHRvIHJ1biBldmVuIG9uIHRoZSBmYXN0ZXN0IG1vZGVybiBtYWNoaW5l
+cyBhdmFpbGFibGUuCm1hbnkgb2YgdGhlIGVycm9ycyBkdXJpbmcgdGhlIDYrIG1vbnRoIGRldmVs
+b3BtZW50IG9mIHRoZSBJRUVFNzU0IEZQVQpjb2RlIHdlcmUgb25seSBjYXVnaHQgYnkgcnVubmlu
+ZyB3ZWxsIG92ZXIgMTAwLDAwMCByYW5kb20gdGVzdHMgb24gdGhlCmNvZGUgd2hlbiBwYXJhbWV0
+ZXJpc2VkIGRvd24gdG8gRlAxNi4KCndpdGggb25seSA2NTUzNiBwb3NzaWJsZSB2YWx1ZXMgaW4g
+RlAxNiwgdGhpcyBnYXZlIGEgaGlnaCBwcm9iYWJpbGl0eQp0aGF0IGNvcm5lci1jYXNlcyB3b3Vs
+ZCBiZSBjYXVnaHQsIGFuZCBpbiBzb21lIGNhc2VzIChzaW5nbGUgcGFyYW1ldGVyCnJhdGhlciB0
+aGFuIHR3byAyXjE2IHBhcmFtZXRlcnMpIGFsbG93cyBmb3IgZnVsbCBjb3ZlcmFnZS4KCgp0aGVy
+ZWZvcmUsIHllczogdGhlIGlkZWEgaGFzIGFsd2F5cyBiZWVuIHRvIGZvbGxvdyB0aGlzIHN0ZXAt
+Ynktc3RlcApwcm9jZXNzLCBmb3IgKmFsbCogY29kZToKCjEpIHdyaXRlIHRoZSBjb2RlIGFuZCBh
+IGJhc2ljICJ1bmRlcnN0YW5kaW5nIiB1bml0IHRlc3QgaW5mcmFzdHJ1Y3R1cmUKc3VmZmljaWVu
+dCB0byBnZXQgdGhlIGNvZGUgZnVuY3Rpb25hbAoyKSB3cml0ZSBGb3JtYWwgQ29ycmVjdG5lc3Mg
+UHJvb2ZzIHRoYXQgY2F0Y2ggZXJyb3JzCjMpIHdyaXRlICpTSU1QTEUqIHVuaXQgdGVzdHMgdGhh
+dCBpbiBubyB3YXkgY292ZXIgdGhlIGVudGlyZXR5IG9mIHRoZQpjb2RlOiB0aGVpciBwdXJwb3Nl
+IGlzIGFzIGEgKnR1dG9yaWFsKiBhbmQgZXhhbXBsZSBvZiBob3cgdG8gdXNlIHRoZQpjb2RlLgoK
+Z29vZCBleGFtcGxlcyBvZiAoMykgd2hlbiBpdCBjb21lcyB0byB0aGUgcGlwZWxpbmUgQVBJIGFy
+ZSBoZXJlOgpodHRwczovL2dpdC5saWJyZS1zb2Mub3JnLz9wPW5tdXRpbC5naXQ7YT1ibG9iO2Y9
+c3JjL25tdXRpbC90ZXN0L3Rlc3RfYnVmX3BpcGUucHk7aGI9SEVBRApodHRwczovL2dpdC5saWJy
+ZS1zb2Mub3JnLz9wPW5tdXRpbC5naXQ7YT1ibG9iO2Y9c3JjL25tdXRpbC90ZXN0L3Rlc3RfaW5v
+dXRfbXV4X3BpcGUucHk7aGI9SEVBRAoKbC4KCl9fX19fX19fX19fX19fX19fX19fX19fX19fX19f
+X19fX19fX19fX19fX19fX19fCmxpYnJlLXJpc2N2LWRldiBtYWlsaW5nIGxpc3QKbGlicmUtcmlz
+Y3YtZGV2QGxpc3RzLmxpYnJlLXJpc2N2Lm9yZwpodHRwOi8vbGlzdHMubGlicmUtcmlzY3Yub3Jn
+L21haWxtYW4vbGlzdGluZm8vbGlicmUtcmlzY3YtZGV2Cg==
+