Skip to content

Commit 89d1908

Browse files
committed
ebmc: --word-level-smv
1 parent d115585 commit 89d1908

File tree

8 files changed

+210
-1
lines changed

8 files changed

+210
-1
lines changed

CHANGELOG

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
* SystemVerilog: typedefs from package scopes
44
* SystemVerilog: assignment patterns with keys for structs
55
* SMV: LTL V operator, xnor operator
6+
* --smv-word-level outputs the model as word-level SMV
67

78
# EBMC 5.5
89

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
verilog1.v
3+
--smv-word-level
4+
^MODULE main$
5+
^VAR x : unsigned word\[32\];$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
module main(input clk);
2+
3+
reg [31:0] x;
4+
5+
initial x = 0;
6+
7+
always @(posedge clk)
8+
x = x + 1;
9+
10+
endmodule

src/ebmc/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ SRC = \
2424
netlist.cpp \
2525
neural_liveness.cpp \
2626
output_file.cpp \
27+
output_smv_word_level.cpp \
2728
output_verilog.cpp \
2829
property_checker.cpp \
2930
random_traces.cpp \

src/ebmc/ebmc_parse_options.cpp

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
2121
#include "netlist.h"
2222
#include "neural_liveness.h"
2323
#include "output_file.h"
24+
#include "output_smv_word_level.h"
2425
#include "property_checker.h"
2526
#include "random_traces.h"
2627
#include "ranking_function.h"
@@ -215,6 +216,15 @@ int ebmc_parse_optionst::doit()
215216
auto properties = ebmc_propertiest::from_command_line(
216217
cmdline, transition_system, ui_message_handler);
217218

219+
if(cmdline.isset("smv-word-level"))
220+
{
221+
auto filename = cmdline.value_opt("outfile").value_or("-");
222+
output_filet output_file{filename};
223+
output_smv_word_level(
224+
transition_system, properties, output_file.stream());
225+
return 0;
226+
}
227+
218228
if(cmdline.isset("show-properties"))
219229
{
220230
show_properties(properties, ui_message_handler);
@@ -418,6 +428,7 @@ void ebmc_parse_optionst::help()
418428
" {y--smv-netlist} \t show netlist in SMV format\n"
419429
" {y--dot-netlist} \t show netlist in DOT format\n"
420430
" {y--show-trans} \t show transition system\n"
431+
" {y--smv-word-level} \t output word-level SMV\n"
421432
" {y--verbosity} {u#} \t verbosity level, from 0 (silent) to 10 (everything)\n"
422433
// clang-format on
423434
"\n");

src/ebmc/ebmc_parse_options.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,8 @@ class ebmc_parse_optionst:public parse_options_baset
4444
"(smt2)(bitwuzla)(boolector)(cvc3)(cvc4)(cvc5)(mathsat)(yices)(z3)"
4545
"(minisat)(cadical)"
4646
"(aig)(stop-induction)(stop-minimize)(start):(coverage)(naive)"
47-
"(compute-ct)(dot-netlist)(smv-netlist)(vcd):"
47+
"(compute-ct)(dot-netlist)(smv-netlist)(smv-word-level)"
48+
"(vcd):"
4849
"(random-traces)(trace-steps):(random-seed):(traces):"
4950
"(random-trace)(random-waveform)"
5051
"(bmc-with-assumptions)"

src/ebmc/output_smv_word_level.cpp

Lines changed: 154 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
1+
/*******************************************************************\
2+
3+
Module: Word-Level SMV Output
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "output_smv_word_level.h"
10+
11+
#include <util/bitvector_types.h>
12+
13+
#include "ebmc_error.h"
14+
#include "ebmc_properties.h"
15+
#include "transition_system.h"
16+
17+
#include <ostream>
18+
19+
class smv_type_printert
20+
{
21+
public:
22+
explicit smv_type_printert(const typet &__type) : _type(__type)
23+
{
24+
}
25+
26+
const typet &type() const
27+
{
28+
return _type;
29+
}
30+
31+
protected:
32+
const typet &_type;
33+
};
34+
35+
std::ostream &
36+
operator<<(std::ostream &out, const smv_type_printert &type_printer)
37+
{
38+
auto &type = type_printer.type();
39+
40+
if(type.id() == ID_bool)
41+
return out << "boolean";
42+
else if(type.id() == ID_signedbv)
43+
return out << "signed word[" << to_signedbv_type(type).get_width() << "]";
44+
else if(type.id() == ID_unsignedbv)
45+
return out << "unsigned word[" << to_unsignedbv_type(type).get_width()
46+
<< "]";
47+
else
48+
throw ebmc_errort{} << "cannot convert type " << type.id() << " to SMV";
49+
50+
return out;
51+
}
52+
53+
class smv_expr_printert
54+
{
55+
public:
56+
explicit smv_expr_printert(const exprt &__expr) : _expr(__expr)
57+
{
58+
}
59+
60+
const exprt &expr() const
61+
{
62+
return _expr;
63+
}
64+
65+
protected:
66+
const exprt &_expr;
67+
};
68+
69+
std::ostream &
70+
operator<<(std::ostream &out, const smv_expr_printert &expr_printer)
71+
{
72+
return out;
73+
}
74+
75+
static void smv_state_variables(
76+
const transition_systemt &transition_system,
77+
std::ostream &out)
78+
{
79+
bool found = false;
80+
81+
const auto module = transition_system.main_symbol->name;
82+
const auto &symbol_table = transition_system.symbol_table;
83+
84+
for(auto m_it = symbol_table.symbol_module_map.lower_bound(module);
85+
m_it != symbol_table.symbol_module_map.upper_bound(module);
86+
m_it++)
87+
{
88+
const irep_idt &identifier = m_it->second;
89+
90+
symbol_tablet::symbolst::const_iterator s_it =
91+
symbol_table.symbols.find(identifier);
92+
93+
if(s_it == symbol_table.symbols.end())
94+
throw ebmc_errort{} << "failed to find symbol " << identifier;
95+
96+
const symbolt &symbol = s_it->second;
97+
98+
if(symbol.is_state_var)
99+
{
100+
out << "VAR " << symbol.base_name << " : "
101+
<< smv_type_printert{symbol.type} << ";\n";
102+
found = true;
103+
}
104+
}
105+
106+
if(found)
107+
out << '\n';
108+
}
109+
110+
static void smv_transition_relation(
111+
const transition_systemt &transition_system,
112+
std::ostream &out)
113+
{
114+
}
115+
116+
static void
117+
smv_properties(const ebmc_propertiest &properties, std::ostream &out)
118+
{
119+
for(auto &property : properties.properties)
120+
{
121+
if(property.is_disabled() || property.is_assumed())
122+
continue;
123+
124+
if(is_CTL(property.normalized_expr))
125+
{
126+
out << "CTLSPEC " << smv_expr_printert{property.normalized_expr};
127+
}
128+
else if(is_LTL(property.normalized_expr))
129+
{
130+
out << "LTLSPEC " << smv_expr_printert{property.normalized_expr};
131+
}
132+
else
133+
out << "-- " << property.identifier << ": not converted\n";
134+
135+
out << '\n';
136+
}
137+
}
138+
139+
void output_smv_word_level(
140+
const transition_systemt &transition_system,
141+
const ebmc_propertiest &properties,
142+
std::ostream &out)
143+
{
144+
out << "MODULE main\n\n";
145+
146+
// state-holding elements first
147+
smv_state_variables(transition_system, out);
148+
149+
// transition relation
150+
smv_transition_relation(transition_system, out);
151+
152+
// properties
153+
smv_properties(properties, out);
154+
}

src/ebmc/output_smv_word_level.h

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
/*******************************************************************\
2+
3+
Module: Word-Level SMV Output
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef EBMC_OUTPUT_SMV_WORD_LEVEL_H
10+
#define EBMC_OUTPUT_SMV_WORD_LEVEL_H
11+
12+
#include <iosfwd>
13+
14+
class ebmc_propertiest;
15+
class transition_systemt;
16+
17+
/// outputs word-level SMV
18+
void output_smv_word_level(
19+
const transition_systemt &,
20+
const ebmc_propertiest &,
21+
std::ostream &);
22+
23+
#endif // EBMC_OUTPUT_SMV_WORD_LEVEL_H

0 commit comments

Comments
 (0)