From 3ec00cceaa62ad7e06bdaa0fa48eaaffeae8982c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 10 Jul 2023 12:28:22 +0200 Subject: [PATCH] cellaigs: Generate models for integer comparison cells Add the case of $lt, $le, $gt, $ge to the code generating AIGs. --- kernel/cellaigs.cc | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/kernel/cellaigs.cc b/kernel/cellaigs.cc index 292af3f51b0..6246e59c7c1 100644 --- a/kernel/cellaigs.cc +++ b/kernel/cellaigs.cc @@ -385,6 +385,26 @@ Aig::Aig(Cell *cell) goto optimize; } + if (cell->type.in({ID($lt), ID($gt), ID($le), ID($ge)})) + { + int width = std::max(GetSize(cell->getPort(ID::A)), + GetSize(cell->getPort(ID::B))) + 1; + vector A = mk.inport_vec(ID::A, width); + vector B = mk.inport_vec(ID::B, width); + + if (cell->type.in({ID($gt), ID($ge)})) + std::swap(A, B); + + int carry = mk.bool_node(!cell->type.in({ID($le), ID($ge)})); + for (auto &n : B) + n = mk.not_gate(n); + vector Y = mk.adder(A, B, carry); + mk.outport(Y.back(), ID::Y); + for (int i = 1; i < GetSize(cell->getPort(ID::Y)); i++) + mk.outport(mk.bool_node(false), ID::Y, i); + goto optimize; + } + if (cell->type == ID($alu)) { int width = GetSize(cell->getPort(ID::Y));