From afa4389445adc8e53871af78ab1c38c98e03a6fc Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 14 Feb 2019 13:27:26 -0800 Subject: [PATCH] Get rid of formal stuff from xaiger backend --- backends/aiger/xaiger.cc | 58 ---------------------------------------- 1 file changed, 58 deletions(-) diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 7fc61fa9a..c5cede3b1 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -205,64 +205,6 @@ struct XAigerWriter continue; } - if (cell->type == "$assert") - { - SigBit A = sigmap(cell->getPort("\\A").as_bit()); - SigBit EN = sigmap(cell->getPort("\\EN").as_bit()); - unused_bits.erase(A); - unused_bits.erase(EN); - asserts.push_back(make_pair(A, EN)); - continue; - } - - if (cell->type == "$assume") - { - SigBit A = sigmap(cell->getPort("\\A").as_bit()); - SigBit EN = sigmap(cell->getPort("\\EN").as_bit()); - unused_bits.erase(A); - unused_bits.erase(EN); - assumes.push_back(make_pair(A, EN)); - continue; - } - - if (cell->type == "$live") - { - SigBit A = sigmap(cell->getPort("\\A").as_bit()); - SigBit EN = sigmap(cell->getPort("\\EN").as_bit()); - unused_bits.erase(A); - unused_bits.erase(EN); - liveness.push_back(make_pair(A, EN)); - continue; - } - - if (cell->type == "$fair") - { - SigBit A = sigmap(cell->getPort("\\A").as_bit()); - SigBit EN = sigmap(cell->getPort("\\EN").as_bit()); - unused_bits.erase(A); - unused_bits.erase(EN); - fairness.push_back(make_pair(A, EN)); - continue; - } - - if (cell->type == "$anyconst") - { - for (auto bit : sigmap(cell->getPort("\\Y"))) { - undriven_bits.erase(bit); - ff_map[bit] = bit; - } - continue; - } - - if (cell->type == "$anyseq") - { - for (auto bit : sigmap(cell->getPort("\\Y"))) { - undriven_bits.erase(bit); - input_bits.insert(bit); - } - continue; - } - log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell)); } -- 2.30.2