aiger2: Support `$bwmux`, comparison operators

backends/aiger2/aiger.cc

@@ -25,7 +25,8 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
-#define BITWISE_OPS ID($buf), ID($not), ID($mux), ID($and), ID($or), ID($xor), ID($xnor), ID($fa)
+#define BITWISE_OPS ID($buf), ID($not), ID($mux), ID($and), ID($or), ID($xor), ID($xnor), ID($fa), \
+					ID($bwmux)
 
 #define REDUCE_OPS ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_xnor), ID($reduce_bool)
 
@@ -35,10 +36,12 @@ PRIVATE_NAMESPACE_BEGIN
 				 ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_), ID($_MUX_), ID($_NMUX_), \
 				 ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_)
 
-// TODO
-//#define ARITH_OPS ID($add), ID($sub), ID($lt), ID($le), ID($ge), ID($gt), ID($neg)
+#define CMP_OPS ID($eq), ID($ne), ID($lt), ID($le), ID($ge), ID($gt)
 
-#define KNOWN_OPS BITWISE_OPS, REDUCE_OPS, LOGIC_OPS, GATE_OPS, ID($pos) /*, ARITH_OPS*/
+// TODO
+//#define ARITH_OPS ID($add), ID($sub), ID($neg)
+
+#define KNOWN_OPS BITWISE_OPS, REDUCE_OPS, LOGIC_OPS, GATE_OPS, ID($pos), CMP_OPS /*, ARITH_OPS*/
 
 template<typename Writer, typename Lit>
 struct Index {
@@ -178,10 +181,61 @@ struct Index {
 		return OR(AND(a, NOT(b)), AND(NOT(a), b));
 	}
 
+	Lit XNOR(Lit a, Lit b)
+	{
+		return NOT(OR(AND(a, NOT(b)), AND(NOT(a), b)));
+	}
+
+	Lit CARRY(Lit a, Lit b, Lit c)
+	{
+		if (const_folding) {
+			if (c == CTRUE) {
+				return OR(a, b);
+			} else if (c == CFALSE) {
+				return AND(a, b);
+			}
+		}
+		return OR(AND(a, b), AND(c, OR(a, b)));
+	}
+
 	Lit impl_op(HierCursor &cursor, Cell *cell, IdString oport, int obit)
 	{
-		if (cell->type.in(REDUCE_OPS, LOGIC_OPS) && obit != 0) {
-			return Writer::CONST_FALSE;
+		if (cell->type.in(REDUCE_OPS, LOGIC_OPS, CMP_OPS) && obit != 0) {
+			return CFALSE;
+		} else if (cell->type.in(CMP_OPS)) {
+			SigSpec aport = cell->getPort(ID::A);
+			bool asigned = cell->getParam(ID::A_SIGNED).as_bool();
+			SigSpec bport = cell->getPort(ID::B);
+			bool bsigned = cell->getParam(ID::B_SIGNED).as_bool();
+
+			int width = std::max(aport.size(), bport.size()) + 1;
+			aport.extend_u0(width, asigned);
+			bport.extend_u0(width, bsigned);
+
+			if (cell->type.in(ID($eq), ID($ne))) {
+				int carry = CTRUE;
+				for (int i = 0; i < width; i++) {
+					Lit a = visit(cursor, aport[i]);
+					Lit b = visit(cursor, bport[i]);
+					carry = AND(carry, XNOR(a, b));
+				}
+				return (cell->type == ID($eq)) ? carry : /* $ne */ NOT(carry);
+			} else if (cell->type.in(ID($lt), ID($le), ID($gt), ID($ge))) {
+				if (cell->type.in(ID($gt), ID($ge)))
+					std::swap(aport, bport);
+				int carry = cell->type.in(ID($le), ID($ge)) ? CFALSE : CTRUE; 
+				Lit a, b;
+				// TODO: this might not be the most economic structure; revisit at a later date
+				for (int i = 0; i < width; i++) {
+					a = visit(cursor, aport[i]);
+					b = visit(cursor, bport[i]);
+					if (i != width - 1)
+						carry = CARRY(a, NOT(b), carry);
+				}
+				return XOR(carry, XNOR(a, b));
+			} else {
+				log_abort();
+			}
 		} else if (cell->type.in(REDUCE_OPS, ID($logic_not))) {
 			SigSpec inport = cell->getPort(ID::A);
 
@@ -274,6 +328,9 @@ struct Index {
 				} else if (cell->type.in(ID($mux), ID($_MUX_))) {
 					Lit s = visit(cursor, cell->getPort(ID::S));
 					return MUX(a, b, s);
+				} else if (cell->type.in(ID($bwmux))) {
+					Lit s = visit(cursor, cell->getPort(ID::S)[obit]);
+					return MUX(a, b, s);
 				} else if (cell->type.in(ID($_NMUX_))) {
 					Lit s = visit(cursor, cell->getPort(ID::S)[obit]);
 					return NOT(MUX(a, b, s));

tests/various/aiger2.ys

@@ -83,6 +83,12 @@ assign name``_y2 = op name``_a2;
 `BIOP(xnor, ~^, 3, 3, 3)
 `BIOP(logic_and, &&, 4, 3, 1)
 `BIOP(logic_or, ||, 3, 3, 2)
+`BIOP(eq, ==, 3, 3, 1)
+`BIOP(ne, !=, 3, 3, 1)
+`BIOP(lt, <, 3, 3, 1)
+`BIOP(le, <=, 3, 3, 1)
+`BIOP(gt, >, 3, 3, 1)
+`BIOP(ge, >=, 3, 3, 1)
 `UNOP(not, ~, 3)
 `UNOP_REDUCE(logic_not, !, 3)
 `UNOP_REDUCE(reduce_and, &, 3)
@@ -97,6 +103,11 @@ wire [1:0] fa_a, fa_b, fa_c, fa_x, fa_y;
 \$fa #(
 	.WIDTH(2)
 ) fa(.A(fa_a), .B(fa_b), .C(fa_c), .X(fa_x), .Y(fa_y));
+
+wire [1:0] bwmux_a, bwmux_b, bwmux_s, bwmux_y;
+\$bwmux #(
+	.WIDTH(2)
+) bwmux(.A(bwmux_a), .B(bwmux_b), .S(bwmux_s), .Y(bwmux_y));
 endmodule
 EOF
 
@@ -110,8 +121,8 @@ select -clear
 delete test
 read_aiger -module_name test aiger2_ops.aig
 select -assert-none test/t:$_AND_ test/t:$_NOT_ %% test/c:* %D
-miter -equiv -flatten gold test miter
-sat -verify -prove trigger 0 miter
+miter -equiv -make_outcmp -flatten gold test miter
+sat -verify -show-ports -prove trigger 0 miter
 
 design -reset
 read_verilog -icells <<EOF