Skip to content

Commit 2d3f15a

Browse files
kroeningkroening
committed
extract code for outputting netlists as SMV
This extracts the code for outputting netlists as SMV files from the class, and into a separate file.
1 parent 8c5ac32 commit 2d3f15a

File tree

6 files changed

+313
-329
lines changed

6 files changed

+313
-329
lines changed

‎src/ebmc/ebmc_parse_options.cpp‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
1313
#include <util/help_formatter.h>
1414
#include <util/string2int.h>
1515

16+
#include <trans-netlist/smv_netlist.h>
17+
1618
#include "diatest.h"
1719
#include "ebmc_base.h"
1820
#include "ebmc_error.h"
@@ -288,7 +290,7 @@ int ebmc_parse_optionst::doit()
288290
outfile.stream() << "-- Generated from "
289291
<< transition_system.main_symbol->name << '\n';
290292
outfile.stream() << '\n';
291-
netlist.output_smv(outfile.stream());
293+
smv_netlist(netlist, outfile.stream());
292294
return 0;
293295
}
294296

‎src/trans-netlist/Makefile‎

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,21 @@
11
SRC = aig.cpp \
2-
aig_terminals.cpp \
32
aig_prop.cpp \
3+
aig_terminals.cpp \
44
bmc_map.cpp \
5+
bv_varid.cpp \
6+
compute_ct.cpp \
57
counterexample_netlist.cpp \
68
instantiate_netlist.cpp \
9+
ldg.cpp \
10+
map_aigs.cpp \
711
netlist.cpp \
12+
smv_netlist.cpp \
13+
trans_to_netlist.cpp \
14+
trans_trace.cpp \
815
trans_trace_netlist.cpp \
9-
var_map.cpp \
1016
unwind_netlist.cpp \
11-
ldg.cpp \
12-
compute_ct.cpp \
13-
trans_trace.cpp \
14-
trans_to_netlist.cpp \
15-
map_aigs.cpp \
16-
bv_varid.cpp
17+
var_map.cpp \
18+
# last line
1719

1820
include ../config.inc
1921
include ../common

‎src/trans-netlist/netlist.cpp‎

Lines changed: 0 additions & 314 deletions
Original file line numberDiff line numberDiff line change
@@ -8,14 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
88

99
#include "netlist.h"
1010

11-
#include <util/namespace.h>
12-
#include <util/symbol_table.h>
13-
14-
#include <smvlang/expr2smv.h>
1511
#include <solvers/flattening/boolbv_width.h>
16-
#include <solvers/prop/literal_expr.h>
17-
#include <temporal-logic/temporal_logic.h>
18-
#include <verilog/sva_expr.h>
1912

2013
#include <ctype.h>
2114
#include <sstream>
@@ -225,310 +218,3 @@ void netlistt::output_dot(std::ostream &out) const
225218
}
226219
}
227220
}
228-
229-
/*******************************************************************\
230-
231-
Function: netlistt::output_smv
232-
233-
Inputs:
234-
235-
Outputs:
236-
237-
Purpose:
238-
239-
\*******************************************************************/
240-
241-
void netlistt::output_smv(std::ostream &out) const
242-
{
243-
out << "MODULE main" << '\n';
244-
245-
out << '\n';
246-
out << "-- Variables" << '\n';
247-
out << '\n';
248-
249-
for(var_mapt::mapt::const_iterator
250-
it=var_map.map.begin();
251-
it!=var_map.map.end();
252-
it++)
253-
{
254-
const var_mapt::vart &var=it->second;
255-
256-
for(unsigned i=0; i<var.bits.size(); i++)
257-
{
258-
if(var.is_latch())
259-
{
260-
out << "VAR " << id2smv(it->first);
261-
if(var.bits.size()!=1) out << "[" << i << "]";
262-
out << ": boolean;" << '\n';
263-
}
264-
}
265-
}
266-
267-
out << '\n';
268-
out << "-- Inputs" << '\n';
269-
out << '\n';
270-
271-
for(var_mapt::mapt::const_iterator
272-
it=var_map.map.begin();
273-
it!=var_map.map.end();
274-
it++)
275-
{
276-
const var_mapt::vart &var=it->second;
277-
278-
for(unsigned i=0; i<var.bits.size(); i++)
279-
{
280-
if(var.is_input())
281-
{
282-
out << "VAR " << id2smv(it->first);
283-
if(var.bits.size()!=1) out << "[" << i << "]";
284-
out << ": boolean;" << '\n';
285-
}
286-
}
287-
}
288-
289-
out << '\n';
290-
out << "-- AND Nodes" << '\n';
291-
out << '\n';
292-
293-
for(unsigned node_nr=0; node_nr<nodes.size(); node_nr++)
294-
{
295-
const aig_nodet &node=nodes[node_nr];
296-
297-
if(node.is_and())
298-
{
299-
out << "DEFINE node" << node_nr << ":=";
300-
print_smv(out, node.a);
301-
out << " & ";
302-
print_smv(out, node.b);
303-
out << ";" << '\n';
304-
}
305-
}
306-
307-
out << '\n';
308-
out << "-- Next state functions" << '\n';
309-
out << '\n';
310-
311-
for(var_mapt::mapt::const_iterator
312-
it=var_map.map.begin();
313-
it!=var_map.map.end();
314-
it++)
315-
{
316-
const var_mapt::vart &var=it->second;
317-
318-
for(unsigned i=0; i<var.bits.size(); i++)
319-
{
320-
if(var.is_latch())
321-
{
322-
out << "ASSIGN next(" << id2smv(it->first);
323-
if(var.bits.size()!=1) out << "[" << i << "]";
324-
out << "):=";
325-
print_smv(out, var.bits[i].next);
326-
out << ";" << '\n';
327-
}
328-
}
329-
}
330-
331-
out << '\n';
332-
out << "-- Initial state" << '\n';
333-
out << '\n';
334-
335-
for(auto &initial_l : initial)
336-
{
337-
if(!initial_l.is_true())
338-
{
339-
out << "INIT ";
340-
print_smv(out, initial_l);
341-
out << '\n';
342-
}
343-
}
344-
345-
out << '\n';
346-
out << "-- TRANS" << '\n';
347-
out << '\n';
348-
349-
for(auto &trans_l : transition)
350-
{
351-
if(!trans_l.is_true())
352-
{
353-
out << "TRANS ";
354-
print_smv(out, trans_l);
355-
out << '\n';
356-
}
357-
}
358-
359-
out << '\n';
360-
out << "-- Properties" << '\n';
361-
out << '\n';
362-
363-
for(auto &[id, netlist_expr] : properties)
364-
{
365-
if(is_CTL(netlist_expr))
366-
{
367-
out << "-- " << id << '\n';
368-
out << "CTLSPEC ";
369-
print_smv(out, netlist_expr);
370-
out << '\n';
371-
}
372-
else if(is_LTL(netlist_expr))
373-
{
374-
out << "-- " << id << '\n';
375-
out << "LTLSPEC ";
376-
print_smv(out, netlist_expr);
377-
out << '\n';
378-
}
379-
else if(is_SVA(netlist_expr))
380-
{
381-
if(is_SVA_always_p(netlist_expr))
382-
{
383-
out << "-- " << id << '\n';
384-
out << "CTLSPEC AG ";
385-
print_smv(out, to_sva_always_expr(netlist_expr).op());
386-
out << '\n';
387-
}
388-
else if(is_SVA_always_s_eventually_p(netlist_expr))
389-
{
390-
out << "-- " << id << '\n';
391-
out << "CTLSPEC AG AF ";
392-
print_smv(
393-
out,
394-
to_sva_s_eventually_expr(to_sva_always_expr(netlist_expr).op()).op());
395-
out << '\n';
396-
}
397-
else
398-
{
399-
out << "-- " << id << '\n';
400-
out << "-- not translated\n";
401-
out << '\n';
402-
}
403-
}
404-
else
405-
{
406-
// neither LTL nor CTL nor SVA
407-
out << "-- " << id << '\n';
408-
out << "-- not translated\n";
409-
out << '\n';
410-
}
411-
}
412-
}
413-
414-
/*******************************************************************\
415-
416-
Function: netlistt::id2smv
417-
418-
Inputs:
419-
420-
Outputs:
421-
422-
Purpose:
423-
424-
\*******************************************************************/
425-
426-
std::string netlistt::id2smv(const irep_idt &id)
427-
{
428-
std::string result;
429-
430-
for(unsigned i=0; i<id.size(); i++)
431-
{
432-
const bool first = i == 0;
433-
char ch=id[i];
434-
if(
435-
isalnum(ch) || ch == '_' || (ch == '.' && !first) ||
436-
(ch == '#' && !first) || (ch == '-' && !first))
437-
{
438-
result+=ch;
439-
}
440-
else if(ch==':')
441-
{
442-
result+='.';
443-
if((i-1)<id.size() && id[i+1]==':') i++;
444-
}
445-
else
446-
{
447-
result+='$';
448-
result+=std::to_string(ch);
449-
result+='$';
450-
}
451-
}
452-
453-
return result;
454-
}
455-
456-
/*******************************************************************\
457-
458-
Function: netlistt::print_smv
459-
460-
Inputs:
461-
462-
Outputs:
463-
464-
Purpose:
465-
466-
\*******************************************************************/
467-
468-
void netlistt::print_smv(
469-
std::ostream& out,
470-
literalt a) const
471-
{
472-
if(a==const_literal(false))
473-
{
474-
out << "0";
475-
return;
476-
}
477-
else if(a==const_literal(true))
478-
{
479-
out << "1";
480-
return;
481-
}
482-
483-
unsigned node_nr=a.var_no();
484-
DATA_INVARIANT(node_nr < number_of_nodes(), "node_nr in range");
485-
486-
if(a.sign()) out << "!";
487-
488-
if(nodes[node_nr].is_and())
489-
out << "node" << node_nr;
490-
else if(nodes[node_nr].is_var())
491-
{
492-
const bv_varidt &varid=var_map.reverse(node_nr);
493-
out << id2smv(varid.id);
494-
const var_mapt::mapt::const_iterator v_it=var_map.map.find(varid.id);
495-
if(v_it!=var_map.map.end() && v_it->second.bits.size()!=1)
496-
out << '[' << varid.bit_nr << ']';
497-
}
498-
else
499-
out << "unknown";
500-
}
501-
502-
/*******************************************************************\
503-
504-
Function: netlistt::print_smv
505-
506-
Inputs:
507-
508-
Outputs:
509-
510-
Purpose:
511-
512-
\*******************************************************************/
513-
514-
void netlistt::print_smv(std::ostream &out, const exprt &expr) const
515-
{
516-
symbol_tablet symbol_table;
517-
namespacet ns{symbol_table};
518-
519-
// replace literal expressions by symbols
520-
521-
exprt replaced = expr;
522-
replaced.visit_pre(
523-
[this](exprt &node)
524-
{
525-
if(node.id() == ID_literal)
526-
{
527-
std::ostringstream buffer;
528-
print_smv(buffer, to_literal_expr(node).get_literal());
529-
node = symbol_exprt{buffer.str(), node.type()};
530-
}
531-
});
532-
533-
out << expr2smv(replaced, ns);
534-
}

‎src/trans-netlist/netlist.h‎

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,6 @@ class netlistt:public aig_plus_constraintst
3838
using aigt::print;
3939
virtual void print(std::ostream &out) const;
4040
virtual void output_dot(std::ostream &out) const;
41-
virtual void output_smv(std::ostream &out) const;
4241
virtual std::string label(unsigned n) const;
4342
virtual std::string dot_label(unsigned n) const;
4443

@@ -59,11 +58,6 @@ class netlistt:public aig_plus_constraintst
5958
// which uses literal_exprt.
6059
using propertiest = std::map<irep_idt, exprt>;
6160
propertiest properties;
62-
63-
protected:
64-
static std::string id2smv(const irep_idt &id);
65-
void print_smv(std::ostream &, literalt) const;
66-
void print_smv(std::ostream &, const exprt &) const;
6761
};
6862

6963
#endif

0 commit comments

Comments
 (0)