SAT-based neural ranking engine

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

@@ -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

src/ebmc/ebmc_parse_options.cpp

@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
 #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);
 

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)"

src/ebmc/ebmc_solver_factory.h

@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/decision_procedure.h>
 #include <solvers/prop/prop.h>
 
-#include <iosfwd>
+#include <fstream>
 #include <memory>
 
 class ebmc_solvert final

src/ebmc/liveness_to_safety.cpp

@@ -120,23 +120,10 @@ void liveness_to_safetyt::operator()()
   if(!properties.requires_lasso_constraints())
     return; // no
 
-  irep_idt module_identifier = transition_system.main_symbol->name;
-
   // gather the state variables
-  const namespacet ns(transition_system.symbol_table);
+  state_vars = transition_system.state_variables();
 
-  const auto &symbol_module_map =
-    transition_system.symbol_table.symbol_module_map;
-  auto lower = symbol_module_map.lower_bound(module_identifier);
-  auto upper = symbol_module_map.upper_bound(module_identifier);
-
-  for(auto it = lower; it != upper; it++)
-  {
-    const symbolt &symbol = ns.lookup(it->second);
-
-    if(symbol.is_state_var)
-      state_vars.push_back(symbol.symbol_expr());
-  }
+  const namespacet ns(transition_system.symbol_table);
 
   // create 'loop' shadow symbols for the state variables
   for(auto &symbol_expr : state_vars)

src/ebmc/random_traces.cpp

@@ -84,8 +84,6 @@ class random_tracest
 
   constant_exprt random_value(const typet &);
 
-  symbolst inputs() const;
-  symbolst state_variables() const;
   symbolst remove_constrained(const symbolst &) const;
 
   void
@@ -440,80 +438,6 @@ constant_exprt random_tracest::random_value(const typet &type)
 
 /*******************************************************************\
 
-Function: random_tracest::inputs
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-random_tracest::symbolst random_tracest::inputs() const
-{
-  symbolst inputs;
-
-  const auto &module_symbol = *transition_system.main_symbol;
-
-  if(module_symbol.type.id() != ID_module)
-    throw ebmc_errort() << "expected a module but got "
-                        << module_symbol.type.id();
-
-  const auto &ports = module_symbol.type.find(ID_ports);
-
-  // filter out the inputs
-  for(auto &port : static_cast<const exprt &>(ports).operands())
-  {
-    DATA_INVARIANT(port.id() == ID_symbol, "port must be a symbol");
-    if(port.get_bool(ID_input) && !port.get_bool(ID_output))
-    {
-      symbol_exprt input_symbol(port.get(ID_identifier), port.type());
-      input_symbol.add_source_location() = port.source_location();
-      inputs.push_back(std::move(input_symbol));
-    }
-  }
-
-  return inputs;
-}
-
-/*******************************************************************\
-
-Function: random_tracest::state_variables
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-random_tracest::symbolst random_tracest::state_variables() const
-{
-  symbolst state_variables;
-
-  const auto &module_symbol = *transition_system.main_symbol;
-  const namespacet ns(transition_system.symbol_table);
-
-  const auto &symbol_module_map =
-    transition_system.symbol_table.symbol_module_map;
-  auto lower = symbol_module_map.lower_bound(module_symbol.name);
-  auto upper = symbol_module_map.upper_bound(module_symbol.name);
-
-  for(auto it = lower; it != upper; it++)
-  {
-    const symbolt &symbol = ns.lookup(it->second);
-
-    if(symbol.is_state_var)
-      state_variables.push_back(symbol.symbol_expr());
-  }
-
-  return state_variables;
-}
-
-/*******************************************************************\
-
 Function: random_tracest::remove_constrained
 
   Inputs:
@@ -665,12 +589,12 @@ void random_tracest::operator()(
     ns,
     true);
 
-  auto inputs = this->inputs();
+  auto inputs = transition_system.inputs();
 
   if(inputs.empty())
     throw ebmc_errort() << "module does not have inputs";
 
-  auto state_variables = this->state_variables();
+  auto state_variables = transition_system.state_variables();
 
   message.statistics() << "Found " << inputs.size() << " input(s) and "
                        << state_variables.size() << " state variable(s)"