Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit a0df895

Browse files
authoredJul 10, 2024··
Merge pull request #586 from diffblue/netlist-trace2
AIG engine: fix for new symbols for fresh inputs
2 parents f1f38b9 + a5bd0e7 commit a0df895

File tree

3 files changed

+17
-4
lines changed

3 files changed

+17
-4
lines changed
 
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
CORE
2+
netlist-trace2.sv
3+
--bound 0 --numbered-trace --aig
4+
^EXIT=10$
5+
^SIGNAL=0$
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
module main;
2+
3+
wire [7:0] unconnected;
4+
5+
p1: assert property (unconnected == 10);
6+
7+
endmodule

‎src/trans-netlist/trans_to_netlist.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,8 @@ class convert_trans_to_netlistt:public messaget
5959
netlistt &dest;
6060

6161
literalt new_input();
62+
std::size_t input_counter = 0;
63+
irep_idt mode;
6264

6365
class rhs_entryt
6466
{
@@ -159,13 +161,11 @@ Function: convert_trans_to_netlistt::new_input
159161

160162
literalt convert_trans_to_netlistt::new_input()
161163
{
162-
irep_idt id="convert::input";
164+
irep_idt id = "convert::input" + std::to_string(input_counter++);
163165

164166
if(symbol_table.symbols.find(id)==symbol_table.symbols.end())
165167
{
166-
symbolt symbol;
167-
symbol.name=id;
168-
symbol.type=bool_typet();
168+
symbolt symbol{id, bool_typet(), mode};
169169
symbol.is_input=true;
170170
symbol.base_name="input";
171171
symbol_table.add(symbol);
@@ -286,6 +286,7 @@ void convert_trans_to_netlistt::operator()(
286286

287287
const symbolt &module_symbol=ns.lookup(module);
288288
const transt &trans=to_trans_expr(module_symbol.value);
289+
mode = module_symbol.mode;
289290

290291
// build the net-list
291292
aig_prop_constraintt aig_prop(dest, get_message_handler());

0 commit comments

Comments
 (0)
Please sign in to comment.