nuterm using libtorch

.github/workflows/pull-request-checks.yaml

@@ -191,3 +191,52 @@ jobs:
         run: make -C regression/verilog test-z3
       - name: Print ccache stats
         run: ccache -s
+
+  # This job takes approximately 1 minute
+  check-ubuntu-22_04-nuterm:
+    runs-on: ubuntu-22.04
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq gcc g++ ccache cmake
+      - name: Prepare ccache
+        uses: actions/cache@v3
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-22.04-nuterm-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-22.04-nuterm-${{ github.ref }}
+            ${{ runner.os }}-22.04-nuterm
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Get pytorch
+        run: |
+          cd src/nuterm
+          wget -q https://download.pytorch.org/libtorch/cpu/libtorch-cxx11-abi-shared-with-deps-2.1.2%2Bcpu.zip
+          unzip -q *.zip
+      - name: Build with cmake
+        run: |
+          cd src/nuterm
+          LIBTORCH=`pwd`/libtorch
+          mkdir build
+          cd build
+          cmake -DCMAKE_PREFIX_PATH=$LIBTORCH -DCMAKE_CXX_COMPILER_LAUNCHER=ccache ..
+          cmake --build . --config Release
+      - name: Run the unit tests
+        run: src/nuterm/build/pytorch_tests
+      - name: Run the system tests
+        run: make -C regression/nuterm
+      - name: Print ccache stats
+        run: ccache -s

regression/nuterm/Makefile

@@ -0,0 +1,7 @@
+default: test
+
+TEST_PL = ../../lib/cbmc/regression/test.pl
+
+test:
+	@$(TEST_PL) -c ../../../src/nuterm/build/nuterm
+

regression/nuterm/counters/counter1.desc

@@ -0,0 +1,9 @@
+CORE
+counter1
+
+^weight main.clk = 0 .*$
+^weight main.counter = 1 .*$
+^RESULT: main.counter-1$
+^bias: -1 .*$
+^EXIT=0$
+^SIGNAL=0$

regression/nuterm/counters/counter1.v

@@ -0,0 +1,9 @@
+module main(input clk);
+
+  reg [31:0] counter;
+
+  always @(posedge clk)
+    if(counter != 0)
+      counter = counter - 1;
+
+endmodule

regression/nuterm/counters/counter1/trace.1

@@ -0,0 +1,37 @@
+$date
+  Sun Jan  7 16:33:39 2024
+$end
+$timescale
+  1ns
+$end
+$scope module main $end
+  $var reg 32 main.counter main.counter [31:0] $end
+  $var wire 1 main.clk main.clk $end
+$upscope $end
+$enddefinitions $end
+#0
+b00010000000000000000000000000000 main.counter
+0main.clk
+#1
+b00001111111111111111111111111111 main.counter
+1main.clk
+#2
+b00001111111111111111111111111110 main.counter
+#3
+b00001111111111111111111111111101 main.counter
+0main.clk
+#4
+b00001111111111111111111111111100 main.counter
+1main.clk
+#5
+b00001111111111111111111111111011 main.counter
+#6
+b00001111111111111111111111111010 main.counter
+#7
+b00001111111111111111111111111001 main.counter
+#8
+b00001111111111111111111111111000 main.counter
+#9
+b00001111111111111111111111110111 main.counter
+#10
+b00001111111111111111111111110110 main.counter

regression/nuterm/counters/counter1/trace.10

@@ -0,0 +1,40 @@
+$date
+  Sun Jan  7 16:33:39 2024
+$end
+$timescale
+  1ns
+$end
+$scope module main $end
+  $var reg 32 main.counter main.counter [31:0] $end
+  $var wire 1 main.clk main.clk $end
+$upscope $end
+$enddefinitions $end
+#0
+b00010000000000000000000000000000 main.counter
+0main.clk
+#1
+b00001111111111111111111111111111 main.counter
+1main.clk
+#2
+b00001111111111111111111111111110 main.counter
+0main.clk
+#3
+b00001111111111111111111111111101 main.counter
+#4
+b00001111111111111111111111111100 main.counter
+1main.clk
+#5
+b00001111111111111111111111111011 main.counter
+0main.clk
+#6
+b00001111111111111111111111111010 main.counter
+#7
+b00001111111111111111111111111001 main.counter
+#8
+b00001111111111111111111111111000 main.counter
+1main.clk
+#9
+b00001111111111111111111111110111 main.counter
+#10
+b00001111111111111111111111110110 main.counter
+0main.clk

regression/nuterm/counters/counter1/trace.2

@@ -0,0 +1,39 @@
+$date
+  Sun Jan  7 16:33:39 2024
+$end
+$timescale
+  1ns
+$end
+$scope module main $end
+  $var reg 32 main.counter main.counter [31:0] $end
+  $var wire 1 main.clk main.clk $end
+$upscope $end
+$enddefinitions $end
+#0
+b00010000000000000000000000000000 main.counter
+0main.clk
+#1
+b00001111111111111111111111111111 main.counter
+#2
+b00001111111111111111111111111110 main.counter
+1main.clk
+#3
+b00001111111111111111111111111101 main.counter
+0main.clk
+#4
+b00001111111111111111111111111100 main.counter
+#5
+b00001111111111111111111111111011 main.counter
+#6
+b00001111111111111111111111111010 main.counter
+#7
+b00001111111111111111111111111001 main.counter
+#8
+b00001111111111111111111111111000 main.counter
+1main.clk
+#9
+b00001111111111111111111111110111 main.counter
+0main.clk
+#10
+b00001111111111111111111111110110 main.counter
+1main.clk

regression/nuterm/counters/counter1/trace.3

@@ -0,0 +1,40 @@
+$date
+  Sun Jan  7 16:33:39 2024
+$end
+$timescale
+  1ns
+$end
+$scope module main $end
+  $var reg 32 main.counter main.counter [31:0] $end
+  $var wire 1 main.clk main.clk $end
+$upscope $end
+$enddefinitions $end
+#0
+b00010000000000000000000000000000 main.counter
+1main.clk
+#1
+b00001111111111111111111111111111 main.counter
+0main.clk
+#2
+b00001111111111111111111111111110 main.counter
+#3
+b00001111111111111111111111111101 main.counter
+1main.clk
+#4
+b00001111111111111111111111111100 main.counter
+#5
+b00001111111111111111111111111011 main.counter
+#6
+b00001111111111111111111111111010 main.counter
+#7
+b00001111111111111111111111111001 main.counter
+0main.clk
+#8
+b00001111111111111111111111111000 main.counter
+1main.clk
+#9
+b00001111111111111111111111110111 main.counter
+0main.clk
+#10
+b00001111111111111111111111110110 main.counter
+1main.clk

regression/nuterm/counters/counter1/trace.4

@@ -0,0 +1,41 @@
+$date
+  Sun Jan  7 16:33:39 2024
+$end
+$timescale
+  1ns
+$end
+$scope module main $end
+  $var reg 32 main.counter main.counter [31:0] $end
+  $var wire 1 main.clk main.clk $end
+$upscope $end
+$enddefinitions $end
+#0
+b00010000000000000000000000000000 main.counter
+0main.clk
+#1
+b00001111111111111111111111111111 main.counter
+1main.clk
+#2
+b00001111111111111111111111111110 main.counter
+#3
+b00001111111111111111111111111101 main.counter
+0main.clk
+#4
+b00001111111111111111111111111100 main.counter
+1main.clk
+#5
+b00001111111111111111111111111011 main.counter
+#6
+b00001111111111111111111111111010 main.counter
+0main.clk
+#7
+b00001111111111111111111111111001 main.counter
+#8
+b00001111111111111111111111111000 main.counter
+1main.clk
+#9
+b00001111111111111111111111110111 main.counter
+0main.clk
+#10
+b00001111111111111111111111110110 main.counter
+1main.clk

regression/nuterm/counters/counter1/trace.5

@@ -0,0 +1,38 @@
+$date
+  Sun Jan  7 16:33:39 2024
+$end
+$timescale
+  1ns
+$end
+$scope module main $end
+  $var reg 32 main.counter main.counter [31:0] $end
+  $var wire 1 main.clk main.clk $end
+$upscope $end
+$enddefinitions $end
+#0
+b00010000000000000000000000000000 main.counter
+1main.clk
+#1
+b00001111111111111111111111111111 main.counter
+#2
+b00001111111111111111111111111110 main.counter
+#3
+b00001111111111111111111111111101 main.counter
+#4
+b00001111111111111111111111111100 main.counter
+0main.clk
+#5
+b00001111111111111111111111111011 main.counter
+1main.clk
+#6
+b00001111111111111111111111111010 main.counter
+0main.clk
+#7
+b00001111111111111111111111111001 main.counter
+1main.clk
+#8
+b00001111111111111111111111111000 main.counter
+#9
+b00001111111111111111111111110111 main.counter
+#10
+b00001111111111111111111111110110 main.counter

regression/nuterm/counters/counter1/trace.6

@@ -0,0 +1,42 @@
+$date
+  Sun Jan  7 16:33:39 2024
+$end
+$timescale
+  1ns
+$end
+$scope module main $end
+  $var reg 32 main.counter main.counter [31:0] $end
+  $var wire 1 main.clk main.clk $end
+$upscope $end
+$enddefinitions $end
+#0
+b00010000000000000000000000000000 main.counter
+0main.clk
+#1
+b00001111111111111111111111111111 main.counter
+1main.clk
+#2
+b00001111111111111111111111111110 main.counter
+0main.clk
+#3
+b00001111111111111111111111111101 main.counter
+#4
+b00001111111111111111111111111100 main.counter
+1main.clk
+#5
+b00001111111111111111111111111011 main.counter
+#6
+b00001111111111111111111111111010 main.counter
+0main.clk
+#7
+b00001111111111111111111111111001 main.counter
+1main.clk
+#8
+b00001111111111111111111111111000 main.counter
+0main.clk
+#9
+b00001111111111111111111111110111 main.counter
+1main.clk
+#10
+b00001111111111111111111111110110 main.counter
+0main.clk