SAT-based neural ranking engine

kroening · kroening · commit 426127f79589 · 2024-05-28T12:33:14.000-07:00
This adds a variant of neural ranking that uses a SAT solver to compute the
weights and biases in the neural network.
diff --git a/examples/Benchmarks/run_solver_nuterm b/examples/Benchmarks/run_solver_nuterm
@@ -0,0 +1,154 @@
+#!/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
+ebmc delay_1.sv --solver-neural-liveness "750-cnt"
+ebmc delay_2.sv --solver-neural-liveness "1250-cnt"
+ebmc delay_3.sv --solver-neural-liveness "2500-cnt"
+ebmc delay_4.sv --solver-neural-liveness "5000-cnt"
+ebmc delay_5.sv --solver-neural-liveness "7500-cnt"
+ebmc delay_6.sv --solver-neural-liveness "10000-cnt"
+ebmc delay_7.sv --solver-neural-liveness "12500-cnt"
+ebmc delay_8.sv --solver-neural-liveness "15000-cnt"
+ebmc delay_9.sv --solver-neural-liveness "17500-cnt"
+ebmc delay_10.sv --solver-neural-liveness "20000-cnt"
+ebmc delay_11.sv --solver-neural-liveness "22500-cnt"
+ebmc delay_12.sv --solver-neural-liveness "25000-cnt"
+ebmc delay_13.sv --solver-neural-liveness "50000-cnt"
+ebmc delay_14.sv --solver-neural-liveness "100000-cnt"
+ebmc delay_15.sv --solver-neural-liveness "200000-cnt"
+ebmc delay_16.sv --solver-neural-liveness "400000-cnt"
+fi
+
+if false ; then
+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 "2**9-cnt"
+ebmc i2c_2.sv --solver-neural-liveness "2**10-cnt"
+ebmc i2c_3.sv --solver-neural-liveness "2**11-cnt"
+ebmc i2c_4.sv --solver-neural-liveness "2**12-cnt"
+ebmc i2c_5.sv --solver-neural-liveness "2**13-cnt"
+ebmc i2c_6.sv --solver-neural-liveness "2**14-cnt"
+ebmc i2c_7.sv --solver-neural-liveness "2**15-cnt"
+ebmc i2c_8.sv --solver-neural-liveness "2**16-cnt"
+ebmc i2c_9.sv --solver-neural-liveness "2**17-cnt"
+ebmc i2c_10.sv --solver-neural-liveness "2**18-cnt"
+ebmc i2c_11.sv --solver-neural-liveness "2**19-cnt"
+ebmc i2c_12.sv --solver-neural-liveness "2**10-cnt"
+ebmc i2c_13.sv --solver-neural-liveness "2**10-cnt"
+ebmc i2c_14.sv --solver-neural-liveness "2**10-cnt"
+ebmc i2c_15.sv --solver-neural-liveness "2**10-cnt"
+ebmc i2c_16.sv --solver-neural-liveness "2**10-cnt"
+ebmc i2c_17.sv --solver-neural-liveness "2**10-cnt"
+ebmc i2c_18.sv --solver-neural-liveness "2**10-cnt"
+ebmc i2c_19.sv --solver-neural-liveness "2**10-cnt"
+ebmc i2c_20.sv --solver-neural-liveness "2**19-cnt"
+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
+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
+ebmc uart_transmit_1.sv --solver-neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_2.sv --solver-neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_3.sv --solver-neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_4.sv --solver-neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_5.sv --solver-neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_6.sv --solver-neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_7.sv --solver-neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_8.sv --solver-neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_9.sv --solver-neural-liveness --trace-steps 100 --traces 20
+ebmc uart_transmit_10.sv --solver-neural-liveness --trace-steps 200 --traces 20
+ebmc uart_transmit_11.sv --solver-neural-liveness --trace-steps 200 --traces 20
+ebmc uart_transmit_12.sv --solver-neural-liveness --trace-steps 200 --traces 20
+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
diff --git a/regression/ebmc/solver-neural-liveness/counter1.desc b/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$
+--
diff --git a/regression/ebmc/solver-neural-liveness/counter1.sv b/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
diff --git a/regression/ebmc/solver-neural-liveness/wrap_around1.desc b/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$
+--
diff --git a/regression/ebmc/solver-neural-liveness/wrap_around1.sv b/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
diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
@@ -23,10 +23,12 @@ SRC = \
       output_verilog.cpp \
       random_traces.cpp \
       ranking_function.cpp \
+      ranking_net.cpp \
       report_results.cpp \
       show_formula_solver.cpp \
       show_properties.cpp \
       show_trans.cpp \
+      solver_neural_liveness.cpp \
       transition_system.cpp \
       waveform.cpp \
       #empty line
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
@@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "random_traces.h"
 #include "ranking_function.h"
 #include "show_trans.h"
+#include "solver_neural_liveness.h"
 
 #include <iostream>
 
@@ -162,6 +163,9 @@ int ebmc_parse_optionst::doit()
     if(cmdline.isset("neural-liveness"))
       return do_neural_liveness(cmdline, ui_message_handler);
 
+    if(cmdline.isset("solver-neural-liveness"))
+      return do_solver_neural_liveness(cmdline, ui_message_handler);
+
     if(cmdline.isset("ranking-function"))
       return do_ranking_function(cmdline, ui_message_handler);
 
diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h
@@ -34,6 +34,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(po)(cegar)(k-induction)(2pi)(bound2):"
         "(outfile):(xml-ui)(verbosity):(gui)(json-result):"
         "(neural-liveness)(neural-engine):"
+        "(solver-neural-liveness)"
         "(reset):"
         "(version)(verilog-rtl)(verilog-netlist)"
         "(compute-interpolant)(interpolation)(interpolation-vmcai)"
diff --git a/src/ebmc/ebmc_solver_factory.h b/src/ebmc/ebmc_solver_factory.h
@@ -16,7 +16,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <solvers/decision_procedure.h>
 #include <solvers/prop/prop.h>
 
-#include <iosfwd>
+#include <fstream>
 #include <memory>
 
 class ebmc_solvert final
diff --git a/src/ebmc/ranking_net.cpp b/src/ebmc/ranking_net.cpp
@@ -0,0 +1,106 @@
+/*******************************************************************\
+
+Module: Ranking Neural Net
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "ranking_net.h"
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/std_expr.h>
+
+exprt wrap_around(exprt expr)
+{
+  // map negative values to positive ones, wrap around:
+  // -1 --> int_max-1, -2 --> int_max-2, etc.
+  auto int_max = to_signedbv_type(expr.type()).largest_expr();
+  return if_exprt{sign_exprt{expr}, plus_exprt{int_max, expr}, expr};
+}
+
+tuple_exprt wrap_around_tuple(tuple_exprt expr)
+{
+  // map negative values to positive ones, wrap around:
+  // -1 --> int_max-1, -2 --> int_max-2, etc.
+  for(auto &op : expr.operands())
+    op = wrap_around(op);
+
+  return expr;
+}
+
+tuple_exprt ranking_nett::forward(const tuple_exprt &inputs) const
+{
+  auto fc1_out = fc1.forward(inputs);
+  auto w_out = wrap_around_tuple(fc1_out);
+  return w_out;
+}
+
+ranking_nett::lineart::lineart(
+  const irep_idt &__name,
+  std::size_t in,
+  std::size_t out,
+  const typet &type)
+  : name(__name)
+{
+  neurons.reserve(out);
+
+  for(std::size_t i = 0; i < out; i++)
+  {
+    irep_idt identifier = id2string(__name) + ".n" + std::to_string(i);
+    neurons.emplace_back(identifier, in, type);
+  }
+}
+
+ranking_nett::lineart::neuront::neuront(
+  const irep_idt &__name,
+  std::size_t in,
+  const typet &type)
+  : name(__name)
+{
+  {
+    irep_idt identifier = id2string(__name) + ".b";
+    bias = symbol_exprt(identifier, type);
+  }
+
+  weights.reserve(in);
+
+  for(std::size_t i = 0; i < in; i++)
+  {
+    irep_idt identifier = id2string(__name) + ".w" + std::to_string(i);
+    weights.emplace_back(symbol_exprt{identifier, type});
+  }
+}
+
+exprt ranking_nett::lineart::neuront::forward(const tuple_exprt &input) const
+{
+  exprt::operandst result;
+  result.reserve(weights.size() + 1); // one more for bias
+
+  result.push_back(bias);
+
+  PRECONDITION(weights.size() == input.operands().size());
+
+  for(std::size_t i = 0; i < weights.size(); i++)
+    result.push_back(mult_exprt{weights[i], input.operands()[i]});
+
+  return plus_exprt{std::move(result), bias.type()};
+}
+
+exprt relu(exprt expr)
+{
+  auto zero = from_integer(0, expr.type());
+  return if_exprt{greater_than_or_equal_exprt{expr, zero}, expr, zero};
+}
+
+tuple_exprt ranking_nett::lineart::forward(const tuple_exprt &input) const
+{
+  tuple_exprt::operandst result;
+  result.reserve(neurons.size());
+
+  for(auto &neuron : neurons)
+    result.push_back(neuron.forward(input));
+
+  return tuple_exprt{std::move(result)};
+}
diff --git a/src/ebmc/ranking_net.h b/src/ebmc/ranking_net.h
diff --git a/src/ebmc/solver_neural_liveness.cpp b/src/ebmc/solver_neural_liveness.cpp
diff --git a/src/ebmc/solver_neural_liveness.h b/src/ebmc/solver_neural_liveness.h
