From mboxrd@z Thu Jan 1 00:00:00 1970 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" Archived-At: List-Archive: 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==