solver-based neural ranking engine

This adds a variant of neural ranking that uses a SAT/SMT solver to compute
the weights and biases in the neural network.

Author: kroening

examples/Benchmarks/run_solver_nuterm

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

regression/ebmc/solver-neural-liveness/counter1.desc

@@ -0,0 +1,9 @@
+CORE
+counter1.sv
+--traces 1 --solver-neural-liveness
+^weight: nn::fc1\.n0\.w0 = 1$
+^bias: nn::fc1\.n0\.b = .*$
+^\[main\.property\.p0\] always s_eventually main\.counter == 0: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/solver-neural-liveness/counter1.sv

@@ -0,0 +1,16 @@
+// count down from 10 to 0
+
+module main(input clk);
+
+  reg [7:0] counter;
+
+  initial counter = 10;
+
+  always @(posedge clk)
+    if(counter != 0)
+      counter = counter - 1;
+
+  // expected to pass
+  p0: assert property (s_eventually counter == 0);
+
+endmodule

regression/ebmc/solver-neural-liveness/wrap_around1.desc

@@ -0,0 +1,9 @@
+CORE
+wrap_around1.sv
+--traces 1 --solver-neural-liveness
+^weight: nn::fc1\.n0\.w0 = -1$
+^bias: nn::fc1\.n0\.b = .*$
+^\[main\.property\.p0\] always s_eventually main\.counter == 10: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/solver-neural-liveness/wrap_around1.sv

@@ -0,0 +1,18 @@
+// count up from 0 to 10
+
+module main(input clk);
+
+  reg [7:0] counter;
+
+  initial counter = 0;
+
+  always @(posedge clk)
+    if(counter == 10)
+      counter = 0;
+    else
+      counter = counter + 1;
+
+  // expected to pass
+  p0: assert property (s_eventually counter == 10);
+
+endmodule

src/ebmc/Makefile

@@ -24,13 +24,14 @@ SRC = \
       live_signal.cpp \
       main.cpp \
       netlist.cpp \
-      neural_liveness.cpp \
+      neural.cpp \
       output_file.cpp \
       output_smv_word_level.cpp \
       output_verilog.cpp \
       property_checker.cpp \
       random_traces.cpp \
       ranking_function.cpp \
+      ranking_net.cpp \
       report_results.cpp \
       show_formula_solver.cpp \
       show_properties.cpp \

src/ebmc/ebmc_parse_options.cpp

@@ -22,7 +22,6 @@ Author: Daniel Kroening, [email protected]
 #include "instrument_buechi.h"
 #include "liveness_to_safety.h"
 #include "netlist.h"
-#include "neural_liveness.h"
 #include "output_file.h"
 #include "output_smv_word_level.h"
 #include "property_checker.h"
@@ -142,9 +141,6 @@ int ebmc_parse_optionst::doit()
     if(cmdline.isset("random-trace") || cmdline.isset("random-waveform"))
       return random_trace(cmdline, ui_message_handler);
 
-    if(cmdline.isset("neural-liveness"))
-      return do_neural_liveness(cmdline, ui_message_handler);
-
     if(cmdline.isset("ranking-function"))
       return do_ranking_function(cmdline, ui_message_handler);
 
@@ -224,7 +220,11 @@ int ebmc_parse_optionst::doit()
 
     // LTL/SVA to Buechi?
     if(cmdline.isset("buechi"))
+    {
+      if(cmdline.isset("neural"))
+        throw ebmc_errort() << "The neural engine does not work with --buechi";
       instrument_buechi(transition_system, properties, ui_message_handler);
+    }
 
     // possibly apply liveness-to-safety
     if(cmdline.isset("liveness-to-safety"))
@@ -412,9 +412,8 @@ void ebmc_parse_optionst::help()
     "    {y--trace-steps} {unumber}  \t set the number of random transitions (default: 10 steps)\n"
     " {y--ranking-function} {uf}     \t prove a liveness property using given ranking funnction (experimental)\n"
     "    {y--property} {uid}         \t the liveness property to prove\n"
-    " {y--neural-liveness}           \t check liveness properties using neural "
+    " {y--neural}                    \t check properties using neural "
                                        "inference (experimental)\n"
-    "    {y--neural-engine} {ucmd}   \t the neural engine to use\n"
 
     //" --interpolation                \t use bit-level interpolants\n"
     //" --interpolation-word           \t use word-level interpolants\n"

src/ebmc/ebmc_parse_options.h

@@ -34,8 +34,9 @@ class ebmc_parse_optionst:public parse_options_baset
         "(po)(cegar)(k-induction)(2pi)(bound2):"
         "(outfile):(xml-ui)(verbosity):(gui)"
         "(json-modules):(json-properties):(json-result):"
-        "(neural-liveness)(neural-engine):"
+        "(neural)"
         "(reset):(ignore-initial)"
+        "(solver-neural-liveness)"
         "(version)(verilog-rtl)(verilog-netlist)"
         "(compute-interpolant)(interpolation)(interpolation-vmcai)"
         "(ic3)(property):(constr)(h)(new-mode)(aiger)"