Skip to content

Commit 75e0dd1

Browse files
committed
SAT-based neural ranking engine
This adds a variant of neural ranking that uses a SAT solver to compute the weights and biases in the neural network.
1 parent 63ace46 commit 75e0dd1

File tree

10 files changed

+727
-1
lines changed

10 files changed

+727
-1
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
counter1.sv
3+
--traces 1 --solver-neural-liveness
4+
^candidate: 1 \* cast\(Verilog::main\.counter, signedbv\[40\]\)$
5+
^\[main\.property\.p0\] always s_eventually main\.counter == 0: PROVED$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
// count down from 10 to 0
2+
3+
module main(input clk);
4+
5+
reg [7:0] counter;
6+
7+
initial counter = 10;
8+
9+
always @(posedge clk)
10+
if(counter != 0)
11+
counter = counter - 1;
12+
13+
// expected to pass
14+
p0: assert property (s_eventually counter == 0);
15+
16+
endmodule

src/ebmc/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,10 +23,12 @@ SRC = \
2323
output_verilog.cpp \
2424
random_traces.cpp \
2525
ranking_function.cpp \
26+
ranking_net.cpp \
2627
report_results.cpp \
2728
show_formula_solver.cpp \
2829
show_properties.cpp \
2930
show_trans.cpp \
31+
solver_neural_liveness.cpp \
3032
transition_system.cpp \
3133
waveform.cpp \
3234
#empty line

src/ebmc/ebmc_parse_options.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
2525
#include "random_traces.h"
2626
#include "ranking_function.h"
2727
#include "show_trans.h"
28+
#include "solver_neural_liveness.h"
2829

2930
#include <iostream>
3031

@@ -162,6 +163,9 @@ int ebmc_parse_optionst::doit()
162163
if(cmdline.isset("neural-liveness"))
163164
return do_neural_liveness(cmdline, ui_message_handler);
164165

166+
if(cmdline.isset("solver-neural-liveness"))
167+
return do_solver_neural_liveness(cmdline, ui_message_handler);
168+
165169
if(cmdline.isset("ranking-function"))
166170
return do_ranking_function(cmdline, ui_message_handler);
167171

src/ebmc/ebmc_parse_options.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ class ebmc_parse_optionst:public parse_options_baset
3434
"(po)(cegar)(k-induction)(2pi)(bound2):"
3535
"(outfile):(xml-ui)(verbosity):(gui)(json-result):"
3636
"(neural-liveness)(neural-engine):"
37+
"(solver-neural-liveness)"
3738
"(reset):"
3839
"(version)(verilog-rtl)(verilog-netlist)"
3940
"(compute-interpolant)(interpolation)(interpolation-vmcai)"

src/ebmc/ebmc_solver_factory.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
1616
#include <solvers/decision_procedure.h>
1717
#include <solvers/prop/prop.h>
1818

19-
#include <iosfwd>
19+
#include <fstream>
2020
#include <memory>
2121

2222
class ebmc_solvert final

src/ebmc/ranking_net.cpp

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
/*******************************************************************\
2+
3+
Module: Ranking Neural Net
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "ranking_net.h"
10+
11+
#include <util/arith_tools.h>
12+
#include <util/bitvector_types.h>
13+
#include <util/std_expr.h>
14+
15+
ranking_nett::lineart::lineart(
16+
const irep_idt &__name,
17+
std::size_t in,
18+
std::size_t out,
19+
const typet &type)
20+
: name(__name)
21+
{
22+
neurons.reserve(out);
23+
24+
for(std::size_t i = 0; i < out; i++)
25+
{
26+
irep_idt identifier = id2string(__name) + ".n" + std::to_string(i);
27+
neurons.emplace_back(identifier, in, type);
28+
}
29+
}
30+
31+
ranking_nett::lineart::neuront::neuront(
32+
const irep_idt &__name,
33+
std::size_t in,
34+
const typet &type)
35+
: name(__name)
36+
{
37+
{
38+
irep_idt identifier = id2string(__name) + ".b";
39+
bias = symbol_exprt(identifier, type);
40+
}
41+
42+
weights.reserve(in);
43+
44+
for(std::size_t i = 0; i < in; i++)
45+
{
46+
irep_idt identifier = id2string(__name) + ".w" + std::to_string(i);
47+
weights.emplace_back(symbol_exprt{identifier, type});
48+
}
49+
}
50+
51+
exprt ranking_nett::lineart::neuront::forward(const tuple_exprt &input) const
52+
{
53+
exprt::operandst result;
54+
result.reserve(weights.size() + 1); // one more for bias
55+
56+
result.push_back(bias);
57+
58+
PRECONDITION(weights.size() == input.operands().size());
59+
60+
for(std::size_t i = 0; i < weights.size(); i++)
61+
result.push_back(mult_exprt{weights[i], input.operands()[i]});
62+
63+
return plus_exprt{std::move(result), bias.type()};
64+
}
65+
66+
exprt relu(exprt expr)
67+
{
68+
auto zero = from_integer(0, expr.type());
69+
return if_exprt{greater_than_or_equal_exprt{expr, zero}, expr, zero};
70+
}
71+
72+
tuple_exprt ranking_nett::lineart::forward(const tuple_exprt &input) const
73+
{
74+
tuple_exprt::operandst result;
75+
result.reserve(neurons.size());
76+
77+
for(auto &neuron : neurons)
78+
result.push_back(neuron.forward(input));
79+
80+
return tuple_exprt{std::move(result)};
81+
}

src/ebmc/ranking_net.h

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
/*******************************************************************\
2+
3+
Module: Ranking Neural Net
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef EBMC_RANKING_NET_H
10+
#define EBMC_RANKING_NET_H
11+
12+
#include <util/mathematical_expr.h>
13+
14+
class ranking_nett
15+
{
16+
public:
17+
explicit ranking_nett(
18+
std::size_t number_of_state_variables,
19+
const typet &__type)
20+
: fc1("nn::fc1", number_of_state_variables, 1, __type)
21+
{
22+
}
23+
24+
tuple_exprt forward(const tuple_exprt &inputs) const
25+
{
26+
return fc1.forward(inputs);
27+
}
28+
29+
class lineart
30+
{
31+
public:
32+
lineart(
33+
const irep_idt &name,
34+
std::size_t in,
35+
std::size_t out,
36+
const typet &);
37+
38+
irep_idt name;
39+
40+
class neuront
41+
{
42+
public:
43+
std::vector<exprt> weights;
44+
exprt bias;
45+
irep_idt name;
46+
neuront(const irep_idt &name, std::size_t in, const typet &);
47+
exprt forward(const tuple_exprt &) const;
48+
};
49+
50+
std::vector<neuront> neurons;
51+
52+
tuple_exprt forward(const tuple_exprt &) const;
53+
};
54+
55+
lineart fc1;
56+
};
57+
58+
exprt relu(exprt);
59+
60+
#endif // EBMC_RANKING_NET

0 commit comments

Comments
 (0)