diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index cc1085f96..e05357fa1 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -187,6 +187,9 @@ struct XAigerWriter TimingInfo timing; for (auto cell : module->cells()) { + if (cell->type.in(ID($input_port), ID($output_port), ID($public))) + continue; + if (!cell->has_keep_attr()) { if (cell->type == ID($_NOT_)) { diff --git a/tests/arch/analogdevices/dsp_abc9.ys b/tests/arch/analogdevices/dsp_abc9.ys index 07d96304b..60c4583a9 100644 --- a/tests/arch/analogdevices/dsp_abc9.ys +++ b/tests/arch/analogdevices/dsp_abc9.ys @@ -37,6 +37,6 @@ verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1 synth_analogdevices techmap -autoproc -wb -map +/analogdevices/cells_sim.v opt -full -fine -select -assert-count 0 t:* t:$assert %d +select -assert-count 0 t:* t:$assert %d t:$*_port %d t:$public %d sat -verify -prove-asserts diff --git a/tests/arch/xilinx/dsp_abc9.ys b/tests/arch/xilinx/dsp_abc9.ys index 034948d1d..e3c5896bb 100644 --- a/tests/arch/xilinx/dsp_abc9.ys +++ b/tests/arch/xilinx/dsp_abc9.ys @@ -37,7 +37,7 @@ verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1 synth_xilinx -abc9 techmap -autoproc -wb -map +/xilinx/cells_sim.v opt -full -fine -select -assert-count 0 t:* t:$assert %d +select -assert-count 0 t:* t:$assert %d t:$*_port %d t:$public %d sat -verify -prove-asserts