nuterm using libtorch

Initial prototype of neural ranking function synthesis for liveness
properties.

Author: kroening

.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

examples/Benchmarks/run_nuterm

@@ -0,0 +1,145 @@
+#!/bin/sh
+
+set -e
+
+ebmc PWM_1.sv --neural-liveness --trace-steps 700 --traces 1
+ebmc PWM_2.sv --neural-liveness --trace-steps 1000 --traces 1
+ebmc PWM_3.sv --neural-liveness --trace-steps 3000 --traces 1
+ebmc PWM_4.sv --neural-liveness --trace-steps 5000 --traces 1
+ebmc PWM_5.sv --neural-liveness --trace-steps 10000 --traces 1
+ebmc PWM_6.sv --neural-liveness --trace-steps 20000 --traces 1
+ebmc PWM_7.sv --neural-liveness --trace-steps 40000 --traces 1
+ebmc PWM_8.sv --neural-liveness --trace-steps 80000 --traces 1
+ebmc PWM_9.sv --neural-liveness --trace-steps 160000 --traces 1
+
+if false ; then
+ebmc delay_1.sv --neural-liveness "750-cnt"
+ebmc delay_2.sv --neural-liveness "1250-cnt"
+ebmc delay_3.sv --neural-liveness "2500-cnt"
+ebmc delay_4.sv --neural-liveness "5000-cnt"
+ebmc delay_5.sv --neural-liveness "7500-cnt"
+ebmc delay_6.sv --neural-liveness "10000-cnt"
+ebmc delay_7.sv --neural-liveness "12500-cnt"
+ebmc delay_8.sv --neural-liveness "15000-cnt"
+ebmc delay_9.sv --neural-liveness "17500-cnt"
+ebmc delay_10.sv --neural-liveness "20000-cnt"
+ebmc delay_11.sv --neural-liveness "22500-cnt"
+ebmc delay_12.sv --neural-liveness "25000-cnt"
+ebmc delay_13.sv --neural-liveness "50000-cnt"
+ebmc delay_14.sv --neural-liveness "100000-cnt"
+ebmc delay_15.sv --neural-liveness "200000-cnt"
+ebmc delay_16.sv --neural-liveness "400000-cnt"
+fi
+
+ebmc gray_1.sv --neural-liveness
+ebmc gray_2.sv --neural-liveness
+ebmc gray_3.sv --neural-liveness
+ebmc gray_4.sv --neural-liveness
+ebmc gray_5.sv --neural-liveness
+ebmc gray_6.sv --neural-liveness
+ebmc gray_7.sv --neural-liveness
+ebmc gray_8.sv --neural-liveness
+ebmc gray_9.sv --neural-liveness
+ebmc gray_10.sv --neural-liveness
+ebmc gray_11.sv --neural-liveness
+
+if false ; then
+ebmc i2c_1.sv --neural-liveness "2**9-cnt"
+ebmc i2c_2.sv --neural-liveness "2**10-cnt"
+ebmc i2c_3.sv --neural-liveness "2**11-cnt"
+ebmc i2c_4.sv --neural-liveness "2**12-cnt"
+ebmc i2c_5.sv --neural-liveness "2**13-cnt"
+ebmc i2c_6.sv --neural-liveness "2**14-cnt"
+ebmc i2c_7.sv --neural-liveness "2**15-cnt"
+ebmc i2c_8.sv --neural-liveness "2**16-cnt"
+ebmc i2c_9.sv --neural-liveness "2**17-cnt"
+ebmc i2c_10.sv --neural-liveness "2**18-cnt"
+ebmc i2c_11.sv --neural-liveness "2**19-cnt"
+ebmc i2c_12.sv --neural-liveness "2**10-cnt"
+ebmc i2c_13.sv --neural-liveness "2**10-cnt"
+ebmc i2c_14.sv --neural-liveness "2**10-cnt"
+ebmc i2c_15.sv --neural-liveness "2**10-cnt"
+ebmc i2c_16.sv --neural-liveness "2**10-cnt"
+ebmc i2c_17.sv --neural-liveness "2**10-cnt"
+ebmc i2c_18.sv --neural-liveness "2**10-cnt"
+ebmc i2c_19.sv --neural-liveness "2**10-cnt"
+ebmc i2c_20.sv --neural-liveness "2**19-cnt"
+fi
+
+if false ; then
+ebmc lcd_1.sv --neural-liveness "{3-state,500-cnt}"
+ebmc lcd_2.sv --neural-liveness "{3-state,1000-cnt}"
+ebmc lcd_3.sv --neural-liveness "{3-state,1500-cnt}"
+ebmc lcd_4.sv --neural-liveness "{3-state,2500-cnt}"
+ebmc lcd_5.sv --neural-liveness "{3-state,5000-cnt}"
+ebmc lcd_6.sv --neural-liveness "{3-state,7500-cnt}"
+ebmc lcd_7.sv --neural-liveness "{3-state,10000-cnt}"
+ebmc lcd_8.sv --neural-liveness "{3-state,12500-cnt}"
+ebmc lcd_9.sv --neural-liveness "{3-state,15000-cnt}"
+ebmc lcd_10.sv --neural-liveness "{3-state,17500-cnt}"
+ebmc lcd_11.sv --neural-liveness "{3-state,20000-cnt}"
+ebmc lcd_12.sv --neural-liveness "{3-state,22500-cnt}"
+ebmc lcd_13.sv --neural-liveness "{3-state,90000-cnt}"
+ebmc lcd_14.sv --neural-liveness "{3-state,180000-cnt}"
+fi
+
+ebmc seven_seg_1.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_2.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_3.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_4.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_5.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_6.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_7.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_8.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_9.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_10.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_11.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_12.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_16.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_17.sv --neural-liveness --property SEVEN.property.p1
+ebmc seven_seg_18.sv --neural-liveness --property SEVEN.property.p1
+
+if false ; then
+ebmc thermocouple_1.sv --neural-liveness "{2-state,2**5-cnt}"
+ebmc thermocouple_2.sv --neural-liveness "{2-state,2**9-cnt}"
+ebmc thermocouple_3.sv --neural-liveness "{2-state,2**10-cnt}"
+ebmc thermocouple_4.sv --neural-liveness "{2-state,2**10-cnt}"
+ebmc thermocouple_5.sv --neural-liveness "{2-state,2**11-cnt}"
+ebmc thermocouple_6.sv --neural-liveness "{2-state,2**11-cnt}"
+ebmc thermocouple_7.sv --neural-liveness "{2-state,2**12-cnt}"
+ebmc thermocouple_8.sv --neural-liveness "{2-state,2**12-cnt}"
+ebmc thermocouple_9.sv --neural-liveness "{2-state,2**13-cnt}"
+ebmc thermocouple_10.sv --neural-liveness "{2-state,2**14-cnt}"
+ebmc thermocouple_11.sv --neural-liveness "{2-state,2**14-cnt}"
+ebmc thermocouple_12.sv --neural-liveness "{2-state,2**14-cnt}"
+ebmc thermocouple_13.sv --neural-liveness "{2-state,2**15-cnt}"
+ebmc thermocouple_14.sv --neural-liveness "{2-state,2**16-cnt}"
+ebmc thermocouple_15.sv --neural-liveness "{2-state,2**17-cnt}"
+ebmc thermocouple_16.sv --neural-liveness "{2-state,2**18-cnt}"
+ebmc thermocouple_17.sv --neural-liveness "{2-state,2**19-cnt}"
+fi
+
+ebmc uart_transmit_1.sv --neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_2.sv --neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_3.sv --neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_4.sv --neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_5.sv --neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_6.sv --neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_7.sv --neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_8.sv --neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_9.sv --neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_10.sv --neural-liveness --trace-steps 200 --traces 20
+ebmc uart_transmit_11.sv --neural-liveness --trace-steps 200 --traces 20
+ebmc uart_transmit_12.sv --neural-liveness --trace-steps 200 --traces 20
+
+if false ; then
+ebmc vga_1.sv --neural-liveness "{2**5-v_cnt,2**7-h_cnt}"
+ebmc vga_2.sv --neural-liveness "{2**6-v_cnt,2**8-h_cnt}"
+ebmc vga_3.sv --neural-liveness "{2**6-v_cnt,2**8-h_cnt}"
+ebmc vga_4.sv --neural-liveness "{2**7-v_cnt,2**9-h_cnt}"
+ebmc vga_5.sv --neural-liveness "{2**8-v_cnt,2**9-h_cnt}"
+ebmc vga_6.sv --neural-liveness "{2**8-v_cnt,2**9-h_cnt}"
+ebmc vga_7.sv --neural-liveness "{2**8-v_cnt,2**10-h_cnt}"
+ebmc vga_8.sv --neural-liveness "{2**9-v_cnt,2**10-h_cnt}"
+ebmc vga_9.sv --neural-liveness "{2**9-v_cnt,2**11-h_cnt}"
+fi

regression/ebmc/neural-liveness/counter1.desc

@@ -1,6 +1,6 @@
 CORE
 counter1.sv
---traces 2 --neural-liveness --neural-engine "echo Candidate: counter\\\\n"
+--traces 2 --neural-liveness --neural-engine "echo RESULT: counter\\\\n"
 ^\[main\.property\.p0\] always s_eventually main.counter == 0: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$

regression/ebmc/neural-liveness/live_signal1.desc

@@ -1,17 +1,17 @@
 CORE
 counter1.sv
 --traces 1 --neural-liveness --show-traces
-^nuterm::live@0 = 0$
-^nuterm::live@1 = 0$
-^nuterm::live@2 = 0$
-^nuterm::live@3 = 0$
-^nuterm::live@4 = 0$
-^nuterm::live@5 = 0$
-^nuterm::live@6 = 0$
-^nuterm::live@7 = 0$
-^nuterm::live@8 = 0$
-^nuterm::live@9 = 0$
-^nuterm::live@10 = 1$
+^Verilog::main\.\$live@0 = 0$
+^Verilog::main\.\$live@1 = 0$
+^Verilog::main\.\$live@2 = 0$
+^Verilog::main\.\$live@3 = 0$
+^Verilog::main\.\$live@4 = 0$
+^Verilog::main\.\$live@5 = 0$
+^Verilog::main\.\$live@6 = 0$
+^Verilog::main\.\$live@7 = 0$
+^Verilog::main\.\$live@8 = 0$
+^Verilog::main\.\$live@9 = 0$
+^Verilog::main\.\$live@10 = 1$
 ^EXIT=0$
 ^SIGNAL=0$
 --

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/README

@@ -0,0 +1,3 @@
+Sample as follows:
+
+ebmc FILE.v --random-traces --vcd FILE/trace 

regression/nuterm/counters/counter1.desc

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

regression/nuterm/counters/counter1.v

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

regression/nuterm/counters/counter1/trace.1

@@ -0,0 +1,39 @@
+$date
+  Mon May 20 17:39:58 2024
+$end
+$timescale
+  1ns
+$end
+$scope module Verilog::main $end
+  $var wire 1 main.clk clk $end
+  $var reg 32 main.counter counter [31:0] $end
+  $var wire 1 main.$live $live $end
+$upscope $end
+$enddefinitions $end
+#0
+0main.clk
+b00010000000000000000000000000000 main.counter
+0main.$live
+#1
+1main.clk
+b00001111111111111111111111111111 main.counter
+#2
+b00001111111111111111111111111110 main.counter
+#3
+0main.clk
+b00001111111111111111111111111101 main.counter
+#4
+1main.clk
+b00001111111111111111111111111100 main.counter
+#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,42 @@
+$date
+  Mon May 20 17:39:58 2024
+$end
+$timescale
+  1ns
+$end
+$scope module Verilog::main $end
+  $var wire 1 main.clk clk $end
+  $var reg 32 main.counter counter [31:0] $end
+  $var wire 1 main.$live $live $end
+$upscope $end
+$enddefinitions $end
+#0
+0main.clk
+b00010000000000000000000000000000 main.counter
+0main.$live
+#1
+1main.clk
+b00001111111111111111111111111111 main.counter
+#2
+0main.clk
+b00001111111111111111111111111110 main.counter
+#3
+b00001111111111111111111111111101 main.counter
+#4
+1main.clk
+b00001111111111111111111111111100 main.counter
+#5
+0main.clk
+b00001111111111111111111111111011 main.counter
+#6
+b00001111111111111111111111111010 main.counter
+#7
+b00001111111111111111111111111001 main.counter
+#8
+1main.clk
+b00001111111111111111111111111000 main.counter
+#9
+b00001111111111111111111111110111 main.counter
+#10
+0main.clk
+b00001111111111111111111111110110 main.counter

regression/nuterm/counters/counter1/trace.2

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