Skip to content

Commit b00ade6

Browse files
committed
fix for netlist conversion
This fixes the case where the netlist conversion fails when there is an operand with natural or integer type. Fixes #674.
1 parent 3847085 commit b00ade6

File tree

3 files changed

+20
-0
lines changed

3 files changed

+20
-0
lines changed
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
CORE
2+
netlist-conversion1.v
3+
--bound 1 --aig
4+
^EXIT=10$
5+
^SIGNAL=0$
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 [0:0] q;
4+
5+
always @(posedge clk)
6+
q[0] <= q[0];
7+
8+
always assert p1: q[0];
9+
10+
endmodule

src/trans-netlist/trans_to_netlist.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -593,6 +593,11 @@ void convert_trans_to_netlistt::convert_lhs_rec(
593593
// default
594594
forall_operands(it, expr)
595595
{
596+
// natural/integer-typed expressions do not contain symbols, and hence,
597+
// do not need to be recursed into.
598+
if(it->type().id() == ID_natural || it->type().id() == ID_integer)
599+
continue;
600+
596601
std::size_t width=boolbv_width(it->type());
597602

598603
if(width==0)

0 commit comments

Comments
 (0)