From 03dad39f67c5185287199ea4c87bda2adf7d1937 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 8 Apr 2025 09:55:09 -0400 Subject: [PATCH 1/2] smv_netlist: cleanup This replaces iterators by ranged for, and unsigned by std::size_t when iterating over vector indices. --- src/trans-netlist/smv_netlist.cpp | 36 +++++++++++++------------------ 1 file changed, 15 insertions(+), 21 deletions(-) diff --git a/src/trans-netlist/smv_netlist.cpp b/src/trans-netlist/smv_netlist.cpp index 35c459bed..8c04e1c5e 100644 --- a/src/trans-netlist/smv_netlist.cpp +++ b/src/trans-netlist/smv_netlist.cpp @@ -20,7 +20,7 @@ std::string id2smv(const irep_idt &id) { std::string result; - for(unsigned i = 0; i < id.size(); i++) + for(std::size_t i = 0; i < id.size(); i++) { const bool first = i == 0; char ch = id[i]; @@ -60,7 +60,7 @@ void print_smv(const netlistt &netlist, std::ostream &out, literalt a) return; } - unsigned node_nr = a.var_no(); + std::size_t node_nr = a.var_no(); DATA_INVARIANT(node_nr < netlist.number_of_nodes(), "node_nr in range"); if(a.sign()) @@ -115,17 +115,15 @@ void smv_netlist(const netlistt &netlist, std::ostream &out) auto &var_map = netlist.var_map; - for(var_mapt::mapt::const_iterator it = var_map.map.begin(); - it != var_map.map.end(); - it++) + for(auto &var_it : var_map.map) { - const var_mapt::vart &var = it->second; + const var_mapt::vart &var = var_it.second; - for(unsigned i = 0; i < var.bits.size(); i++) + for(std::size_t i = 0; i < var.bits.size(); i++) { if(var.is_latch()) { - out << "VAR " << id2smv(it->first); + out << "VAR " << id2smv(var_it.first); if(var.bits.size() != 1) out << "[" << i << "]"; out << ": boolean;" << '\n'; @@ -137,17 +135,15 @@ void smv_netlist(const netlistt &netlist, std::ostream &out) out << "-- Inputs" << '\n'; out << '\n'; - for(var_mapt::mapt::const_iterator it = var_map.map.begin(); - it != var_map.map.end(); - it++) + for(auto &var_it : var_map.map) { - const var_mapt::vart &var = it->second; + const var_mapt::vart &var = var_it.second; - for(unsigned i = 0; i < var.bits.size(); i++) + for(std::size_t i = 0; i < var.bits.size(); i++) { if(var.is_input()) { - out << "VAR " << id2smv(it->first); + out << "VAR " << id2smv(var_it.first); if(var.bits.size() != 1) out << "[" << i << "]"; out << ": boolean;" << '\n'; @@ -161,7 +157,7 @@ void smv_netlist(const netlistt &netlist, std::ostream &out) auto &nodes = netlist.nodes; - for(unsigned node_nr = 0; node_nr < nodes.size(); node_nr++) + for(std::size_t node_nr = 0; node_nr < nodes.size(); node_nr++) { const aig_nodet &node = nodes[node_nr]; @@ -179,17 +175,15 @@ void smv_netlist(const netlistt &netlist, std::ostream &out) out << "-- Next state functions" << '\n'; out << '\n'; - for(var_mapt::mapt::const_iterator it = var_map.map.begin(); - it != var_map.map.end(); - it++) + for(auto &var_it : var_map.map) { - const var_mapt::vart &var = it->second; + const var_mapt::vart &var = var_it.second; - for(unsigned i = 0; i < var.bits.size(); i++) + for(std::size_t i = 0; i < var.bits.size(); i++) { if(var.is_latch()) { - out << "ASSIGN next(" << id2smv(it->first); + out << "ASSIGN next(" << id2smv(var_it.first); if(var.bits.size() != 1) out << "[" << i << "]"; out << "):="; From 9d6b2bef15e8b43ebd7622a47e0213348237a868 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 8 Apr 2025 10:12:55 -0400 Subject: [PATCH 2/2] smv-netlist: use expr2smv for property The SMV to netlist conversion now uses expr2smv for outputting the property, which enables outputting full LTL or CTL. --- regression/ebmc/smv-netlist/smv1.desc | 10 ++++ regression/ebmc/smv-netlist/smv1.smv | 9 ++++ regression/ebmc/smv-netlist/verilog1.desc | 11 +++++ regression/ebmc/smv-netlist/verilog1.sv | 12 +++++ src/ebmc/bdd_engine.cpp | 8 ++-- src/trans-netlist/instantiate_netlist.cpp | 18 ++----- src/trans-netlist/smv_netlist.cpp | 57 ++++++++++------------- 7 files changed, 74 insertions(+), 51 deletions(-) create mode 100644 regression/ebmc/smv-netlist/smv1.desc create mode 100644 regression/ebmc/smv-netlist/smv1.smv create mode 100644 regression/ebmc/smv-netlist/verilog1.desc create mode 100644 regression/ebmc/smv-netlist/verilog1.sv diff --git a/regression/ebmc/smv-netlist/smv1.desc b/regression/ebmc/smv-netlist/smv1.desc new file mode 100644 index 000000000..caaa7e348 --- /dev/null +++ b/regression/ebmc/smv-netlist/smv1.desc @@ -0,0 +1,10 @@ +CORE +smv1.smv +--smv-netlist +^MODULE main$ +^VAR smv\.main\.var\.x: boolean;$ +^ASSIGN next\(smv\.main\.var\.x\):=\!smv\.main\.var\.x;$ +^INIT !smv\.main\.var\.x$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/smv-netlist/smv1.smv b/regression/ebmc/smv-netlist/smv1.smv new file mode 100644 index 000000000..de6109f2e --- /dev/null +++ b/regression/ebmc/smv-netlist/smv1.smv @@ -0,0 +1,9 @@ +MODULE main + +VAR x: boolean; + +ASSIGN next(x):=!x; +ASSIGN init(x):=FALSE; + +LTLSPEC G F x + diff --git a/regression/ebmc/smv-netlist/verilog1.desc b/regression/ebmc/smv-netlist/verilog1.desc new file mode 100644 index 000000000..f7edf9db5 --- /dev/null +++ b/regression/ebmc/smv-netlist/verilog1.desc @@ -0,0 +1,11 @@ +CORE +verilog1.sv +--smv-netlist +^MODULE main$ +^VAR Verilog\.main\.x: boolean;$ +^ASSIGN next\(Verilog\.main\.x\):=\!Verilog\.main\.x;$ +^INIT !Verilog\.main\.x$ +^LTLSPEC G F Verilog\.main\.x$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/smv-netlist/verilog1.sv b/regression/ebmc/smv-netlist/verilog1.sv new file mode 100644 index 000000000..f8fc58a0e --- /dev/null +++ b/regression/ebmc/smv-netlist/verilog1.sv @@ -0,0 +1,12 @@ +module main(input clk); + + reg x; + + initial x = 0; + + always @(posedge clk) + x = !x; + + always assert property (always s_eventually x); + +endmodule diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp index 86010535d..772deb078 100644 --- a/src/ebmc/bdd_engine.cpp +++ b/src/ebmc/bdd_engine.cpp @@ -1054,12 +1054,10 @@ void bdd_enginet::build_BDDs() auto netlist_property = netlist.properties.find(property.identifier); CHECK_RETURN(netlist_property != netlist.properties.end()); DATA_INVARIANT( - netlist_property->second.id() == ID_sva_always, - "assumed property must be sva_always"); - auto &p = to_sva_always_expr(netlist_property->second).op(); + netlist_property->second.id() == ID_G, "assumed property must be G"); + auto &p = to_G_expr(netlist_property->second).op(); DATA_INVARIANT( - p.id() == ID_literal, - "assumed property must be sva_assume sva_assert literal"); + p.id() == ID_literal, "assumed property must be G literal"); auto l = to_literal_expr(p).get_literal(); constraints_BDDs.push_back(aig2bdd(l, BDDs)); } diff --git a/src/trans-netlist/instantiate_netlist.cpp b/src/trans-netlist/instantiate_netlist.cpp index b33c853b2..2543080f8 100644 --- a/src/trans-netlist/instantiate_netlist.cpp +++ b/src/trans-netlist/instantiate_netlist.cpp @@ -311,20 +311,10 @@ std::optional netlist_property( } else if(is_SVA_operator(expr)) { - if(expr.id() == ID_sva_always || expr.id() == ID_sva_assume) - { - auto copy = expr; - auto &op = to_unary_expr(copy).op(); - auto op_opt = - netlist_property(solver, var_map, op, ns, message_handler); - if(op_opt.has_value()) - { - op = op_opt.value(); - return copy; - } - else - return {}; - } + // Try to turn into LTL + auto LTL_opt = SVA_to_LTL(expr); + if(LTL_opt.has_value()) + return netlist_property(solver, var_map, *LTL_opt, ns, message_handler); else return {}; } diff --git a/src/trans-netlist/smv_netlist.cpp b/src/trans-netlist/smv_netlist.cpp index 8c04e1c5e..072685132 100644 --- a/src/trans-netlist/smv_netlist.cpp +++ b/src/trans-netlist/smv_netlist.cpp @@ -88,21 +88,35 @@ void print_smv(const netlistt &netlist, std::ostream &out, const exprt &expr) symbol_tablet symbol_table; namespacet ns{symbol_table}; - // replace literal expressions by symbols + class expr2smv_netlistt : public expr2smvt + { + public: + expr2smv_netlistt(const namespacet &ns, const netlistt &__netlist) + : expr2smvt(ns), netlist(__netlist) + { + } + + protected: + const netlistt &netlist; - exprt replaced = expr; - replaced.visit_pre( - [&netlist](exprt &node) + resultt convert_rec(const exprt &expr) override { - if(node.id() == ID_literal) + if(expr.id() == ID_literal) { std::ostringstream buffer; - print_smv(netlist, buffer, to_literal_expr(node).get_literal()); - node = symbol_exprt{buffer.str(), node.type()}; + auto l = to_literal_expr(expr).get_literal(); + print_smv(netlist, buffer, l); + if(l.sign()) + return {precedencet::NOT, buffer.str()}; + else + return {precedencet::MAX, buffer.str()}; } - }); + else + return expr2smvt::convert_rec(expr); + } + }; - out << expr2smv(replaced, ns); + out << expr2smv_netlistt{ns, netlist}.convert(expr); } void smv_netlist(const netlistt &netlist, std::ostream &out) @@ -243,29 +257,8 @@ void smv_netlist(const netlistt &netlist, std::ostream &out) } else if(is_SVA(netlist_expr)) { - if(is_SVA_always_p(netlist_expr)) - { - out << "-- " << id << '\n'; - out << "CTLSPEC AG "; - print_smv(netlist, out, to_sva_always_expr(netlist_expr).op()); - out << '\n'; - } - else if(is_SVA_always_s_eventually_p(netlist_expr)) - { - out << "-- " << id << '\n'; - out << "CTLSPEC AG AF "; - print_smv( - netlist, - out, - to_sva_s_eventually_expr(to_sva_always_expr(netlist_expr).op()).op()); - out << '\n'; - } - else - { - out << "-- " << id << '\n'; - out << "-- not translated\n"; - out << '\n'; - } + // Should have been mapped to LTL + DATA_INVARIANT(false, "smv_netlist got SVA"); } else {