From b197032925861d62ce0c1d4501010aa115ac4c12 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Mon, 8 Jun 2020 10:40:27 +0100 Subject: [PATCH] Re: [libre-riscv-dev] Using formal to expose bugs in scoreboard --- 4a/59d8d434a6dc73976563490a8d9aa8bddd95fa | 120 ++++++++++++++++++++++ 1 file changed, 120 insertions(+) create mode 100644 4a/59d8d434a6dc73976563490a8d9aa8bddd95fa diff --git a/4a/59d8d434a6dc73976563490a8d9aa8bddd95fa b/4a/59d8d434a6dc73976563490a8d9aa8bddd95fa new file mode 100644 index 0000000..06a9ed5 --- /dev/null +++ b/4a/59d8d434a6dc73976563490a8d9aa8bddd95fa @@ -0,0 +1,120 @@ +Return-path: +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 ) + 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 ) 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 ) 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 ; + 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: +In-Reply-To: +From: Luke Kenneth Casson Leighton +Date: Mon, 8 Jun 2020 10:40:27 +0100 +X-Gmail-Original-Message-ID: +Message-ID: +To: Libre-RISCV General Development +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 + +List-Unsubscribe: , + +List-Archive: +List-Post: +List-Help: +List-Subscribe: , + +Reply-To: Libre-RISCV General Development + +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" + +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== + -- 2.30.2