Merge pull request #2 from google-research/setup-ci

Setup CI

.github/scripts/generate_checks.sh

@@ -0,0 +1,13 @@
+#!/bin/bash
+set -exuo pipefail
+IFS=$'\n\t'
+HERE=$(dirname "$0")
+ROOT=$(git rev-parse --show-toplevel)
+
+cd "${ROOT}"
+cp -r riscv-formal-config riscv-formal/cores/contranomy
+sed -i 's/const rand/rand const/g' riscv-formal/checks/rvfi_macros.*
+cd riscv-formal/cores/contranomy
+cp "${ROOT}"/contranomy/verilog/Contranomy.contranomyRVFITE/*.inc .
+cp "${ROOT}"/contranomy/verilog/Contranomy.contranomyRVFITE/*.v .
+python3 "${ROOT}"/riscv-formal/checks/genchecks.py

.github/scripts/get_formal_checks.sh

@@ -0,0 +1,17 @@
+#!/bin/bash
+set -exuo pipefail
+IFS=$'\n\t'
+HERE=$(dirname "$0")
+ROOT=$(git rev-parse --show-toplevel)
+
+cd "${HERE}"
+./generate_checks.sh
+
+cd "${ROOT}"
+
+# This is all.. a bit hacky. The alternative would be to fork riscv-formal and
+# modify genchecks.py such that it also yield a JSON. I'm not super thrilled
+# about that either.
+makefile=riscv-formal/cores/contranomy/checks/makefile
+checks=$(grep -oP '^all: \K.*' "$makefile")
+python3 -c "import json; print(json.dumps('${checks}'.split()))" > checks.json

.github/scripts/run_riscv_formal_check.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+set -exuo pipefail
+IFS=$'\n\t'
+HERE=$(dirname "$0")
+ROOT=$(git rev-parse --show-toplevel)
+
+cd "${HERE}"
+./generate_checks.sh
+
+cd "${ROOT}"/riscv-formal/cores/contranomy
+make -C checks "$1"
+[[ -f checks/"$1"/PASS ]]

.github/workflows/ci.yml

@@ -0,0 +1,118 @@
+name: CI
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    types:
+      - opened
+      - synchronize
+
+concurrency:
+ group: ${{ github.head_ref || github.run_id }}
+ cancel-in-progress: true
+
+jobs:
+  build-contranomy:
+    name: Build Contranomy using Clash
+    runs-on: ubuntu-latest
+
+    container:
+      image: docker.pkg.github.com/clash-lang/clash-compiler/clash-ci-8.10.2:2022-01-06
+
+      credentials:
+        username: ${{ github.actor }}
+        password: ${{ secrets.GITHUB_TOKEN }}
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v1
+
+      - name: Install nodejs
+        run: |
+          apt-get update
+          apt-get install -y nodejs
+
+      - name: Update Cabal index info
+        run: |
+          cd contranomy
+          cabal update
+          cabal freeze
+
+      - name: Cache
+        uses: actions/cache@v2
+        with:
+          path: |
+            ~/.cabal/packages
+            ~/.cabal/store
+            contranomy/dist-newstyle
+            contranomy/verilog
+
+          key: contranomy-${{ hashFiles('contranomy/cabal.project.freeze') }}
+          restore-keys: contranomy-
+
+      - name: Build Contranomy
+        run: |
+          cd contranomy
+          cabal run clash -- --version
+
+      - name: Generate HDL
+        run: |
+          cd contranomy
+          cabal run -- clash --verilog -main-is contranomyRVFITE Contranomy
+
+      - name: Archive HDL
+        run: |
+          tar -c -f contranomy-hdl.tar contranomy/verilog
+
+      - name: Upload Contranomy HDL
+        uses: actions/upload-artifact@v2
+        with:
+          name: contranomy-hdl
+          path: contranomy-hdl.tar
+
+      - name: Get test matrix
+        run: |
+          .github/scripts/get_formal_checks.sh
+
+      - name: Set test matrix
+        id: set-matrix
+        run: |
+          echo "::set-output name=check_matrix::$(cat checks.json)"
+
+    outputs:
+      check_matrix: ${{ steps.set-matrix.outputs.check_matrix }}
+
+  verify-contranomy:
+    name: RISC-V Formal checks
+    needs: build-contranomy
+    runs-on: ubuntu-latest
+
+    container:
+      image: docker.pkg.github.com/clash-lang/clash-compiler/clash-ci-8.10.2:2022-01-06
+
+      credentials:
+        username: ${{ github.actor }}
+        password: ${{ secrets.GITHUB_TOKEN }}
+
+    strategy:
+      matrix:
+        check: ${{ fromJson(needs.build-contranomy.outputs.check_matrix) }}
+      fail-fast: false
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v1
+
+      - name: Download Contranomy HDL
+        uses: actions/download-artifact@v2
+        with:
+          name: contranomy-hdl
+
+      - name: Extract HDL
+        run: |
+          tar -x -f contranomy-hdl.tar
+
+      - name: Verify ${{ matrix.check }}
+        run: |
+          .github/scripts/run_riscv_formal_check.sh ${{ matrix.check }}

riscv-formal-config/checks.cfg

@@ -0,0 +1,32 @@
+[options]
+isa rv32ic
+
+[depth]
+insn            20
+reg       15    25
+pc_fwd    10    30
+pc_bwd    10    30
+liveness  1  10 30
+unique    1  10 30
+causal    10    30
+csrw            30
+cover     1     15
+
+[csrs]
+misa
+
+[defines]
+`define RISCV_FORMAL_ALIGNED_MEM
+`define RISCV_FORMAL_ALTOPS
+`define RISCV_FORMAL_COMPRESSED
+
+[defines liveness]
+`define CONTRANOMY_FAIRNESS
+
+[script-sources]
+read_verilog -sv @basedir@/cores/@core@/wrapper.sv
+read_verilog -sv @basedir@/cores/@core@/ContranomyCoreMachineStateDirect.inc
+read_verilog -sv @basedir@/cores/@core@/contranomyRVFITE.v
+
+[cover]
+always @* if (!reset) cover (channel[0].cnt_insns == 2);

riscv-formal-config/wrapper.sv

@@ -0,0 +1,98 @@
+module rvfi_wrapper (
+  input clock,
+  input reset,
+  `RVFI_OUTPUTS
+);
+
+(* keep *) `rvformal_rand_reg [31:0] iBusWishbone_DAT_MISO;
+(* keep *) `rvformal_rand_reg iBusWishbone_ACK;
+(* keep *) `rvformal_rand_reg [31:0] dBusWishbone_DAT_MISO;
+(* keep *) `rvformal_rand_reg dBusWishbone_ACK;
+
+(* keep *) wire [29:0] iBusWishbone_ADR;
+(* keep *) wire [31:0] iBusWishbone_DAT_MOSI;
+(* keep *) wire [3:0] iBusWishbone_SEL;
+(* keep *) wire  iBusWishbone_CYC;
+(* keep *) wire  iBusWishbone_STB;
+(* keep *) wire  iBusWishbone_WE;
+(* keep *) wire [2:0] iBusWishbone_CTI;
+(* keep *) wire [1:0] iBusWishbone_BTE;
+(* keep *) wire [29:0] dBusWishbone_ADR;
+(* keep *) wire [31:0] dBusWishbone_DAT_MOSI;
+(* keep *) wire [3:0] dBusWishbone_SEL;
+(* keep *) wire  dBusWishbone_CYC;
+(* keep *) wire  dBusWishbone_STB;
+(* keep *) wire  dBusWishbone_WE;
+
+contranomyRVFITE uut (
+  .clk (clock),
+  .reset (reset),
+
+  .iBusWishbone_DAT_MISO (iBusWishbone_DAT_MISO),
+  .iBusWishbone_ACK (iBusWishbone_ACK),
+  .iBusWishbone_ERR (1'b0),
+  .dBusWishbone_DAT_MISO (dBusWishbone_DAT_MISO),
+  .dBusWishbone_ACK (dBusWishbone_ACK),
+  .dBusWishbone_ERR (1'b0),
+  .timerInterrupt (1'b0),
+  .softwareInterrupt (1'b0),
+  .externalInterrupt (32'd0),
+
+  .iBusWishbone_ADR(iBusWishbone_ADR),
+  .iBusWishbone_DAT_MOSI(iBusWishbone_DAT_MOSI),
+  .iBusWishbone_SEL(iBusWishbone_SEL),
+  .iBusWishbone_CYC(iBusWishbone_CYC),
+  .iBusWishbone_STB(iBusWishbone_STB),
+  .iBusWishbone_WE(iBusWishbone_WE),
+  .iBusWishbone_CTI(iBusWishbone_CTI),
+  .iBusWishbone_BTE(iBusWishbone_BTE),
+  .dBusWishbone_ADR(dBusWishbone_ADR),
+  .dBusWishbone_DAT_MOSI(dBusWishbone_DAT_MOSI),
+  .dBusWishbone_SEL(dBusWishbone_SEL),
+  .dBusWishbone_CYC(dBusWishbone_CYC),
+  .dBusWishbone_STB(dBusWishbone_STB),
+  .dBusWishbone_WE(dBusWishbone_WE),
+
+  `RVFI_CONN
+);
+
+  // I-MEM
+  always @(posedge clock) begin
+    if (reset) begin
+      assume (!iBusWishbone_ACK);
+    end
+    if (!iBusWishbone_CYC) begin
+      assume (!iBusWishbone_ACK);
+    end
+  end
+
+  // D-MEM
+  always @(posedge clock) begin
+    if (reset) begin
+      assume (!dBusWishbone_ACK);
+    end
+    if (!dBusWishbone_CYC) begin
+      assume (!dBusWishbone_ACK);
+    end
+  end
+
+`ifdef CONTRANOMY_FAIRNESS
+  reg [2:0] timeout_ibus = 0;
+  reg [2:0] timeout_dbus = 0;
+
+  always @(posedge clock) begin
+    timeout_ibus <= 0;
+    timeout_dbus <= 0;
+
+    if (iBusWishbone_CYC && !iBusWishbone_ACK)
+      timeout_ibus <= timeout_ibus + 1;
+
+    if (dBusWishbone_CYC && !dBusWishbone_ACK)
+      timeout_dbus <= timeout_dbus + 1;
+
+    assume (!timeout_ibus[2]);
+    assume (!timeout_dbus[2]);
+  end
+`endif
+
+endmodule

riscv-formal/.gitignore

@@ -0,0 +1 @@
+/cores/.gitignore

riscv-formal/COPYING

@@ -0,0 +1,13 @@
+Copyright (C) 2017  Clifford Wolf <[email protected]>
+
+Permission to use, copy, modify, and/or distribute this software for any
+purpose with or without fee is hereby granted, provided that the above
+copyright notice and this permission notice appear in all copies.
+
+THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.

riscv-formal/CodeOfConduct

@@ -0,0 +1,73 @@
+Contributor Covenant Code of Conduct
+
+Our Pledge
+
+In the interest of fostering an open and welcoming environment, we as
+contributors and maintainers pledge to making participation in our project and
+our community a harassment-free experience for everyone, regardless of age, body
+size, disability, ethnicity, gender identity and expression, level of experience,
+nationality, personal appearance, race, religion, or sexual identity and
+orientation.
+
+Our Standards
+
+Examples of behavior that contributes to creating a positive environment
+include:
+
+* Using welcoming and inclusive language
+* Being respectful of differing viewpoints and experiences
+* Gracefully accepting constructive criticism
+* Focusing on what is best for the community
+* Showing empathy towards other community members
+
+Examples of unacceptable behavior by participants include:
+
+* The use of sexualized language or imagery and unwelcome sexual attention or
+  advances
+* Trolling, insulting/derogatory comments, and personal or political attacks
+* Public or private harassment
+* Publishing others' private information, such as a physical or electronic
+  address, without explicit permission
+* Other conduct which could reasonably be considered inappropriate in a
+  professional setting
+
+Our Responsibilities
+
+Project maintainers are responsible for clarifying the standards of acceptable
+behavior and are expected to take appropriate and fair corrective action in
+response to any instances of unacceptable behavior.
+
+Project maintainers have the right and responsibility to remove, edit, or
+reject comments, commits, code, wiki edits, issues, and other contributions
+that are not aligned to this Code of Conduct, or to ban temporarily or
+permanently any contributor for other behaviors that they deem inappropriate,
+threatening, offensive, or harmful.
+
+Scope
+
+This Code of Conduct applies both within project spaces and in public spaces
+when an individual is representing the project or its community. Examples of
+representing a project or community include using an official project e-mail
+address, posting via an official social media account, or acting as an appointed
+representative at an online or offline event. Representation of a project may be
+further defined and clarified by project maintainers.
+
+Enforcement
+
+Instances of abusive, harassing, or otherwise unacceptable behavior may be
+reported by contacting the project team at [email protected] (and/or
+[email protected] if you think your mail to the other address got
+stuck in the spam filter). All complaints will be reviewed and investigated and
+will result in a response that is deemed necessary and appropriate to the
+circumstances. The project team is obligated to maintain confidentiality with
+regard to the reporter of an incident.  Further details of specific enforcement
+policies may be posted separately.
+
+Project maintainers who do not follow or enforce the Code of Conduct in good
+faith may face temporary or permanent repercussions as determined by other
+members of the project's leadership.
+
+Attribution
+
+This Code of Conduct is adapted from the Contributor Covenant, version 1.4,
+available at http://contributor-covenant.org/version/1/4/