From d0a11e26f391a670b73b822671e7b974e112e59a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Martin=20Povi=C5=A1er?= <povik@cutebit.org>
Date: Mon, 7 Oct 2024 11:59:52 +0200
Subject: [PATCH] aiger2: Add test of writing a flattened view

---
 tests/various/aiger2.ys | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/tests/various/aiger2.ys b/tests/various/aiger2.ys
index e008cdfaf..d2b024d2f 100644
--- a/tests/various/aiger2.ys
+++ b/tests/various/aiger2.ys
@@ -193,3 +193,32 @@ select -assert-none test/t:$_AND_ test/t:$_NOT_ %% test/c:* %D
 equiv_make gold test equiv
 equiv_induct -undef equiv
 equiv_status -assert equiv
+
+design -reset
+read_verilog -icells <<EOF
+module sm2(input wire [1:0] a, output wire [1:0] y);
+	assign y = a + 1;
+endmodule
+
+module sm1(input wire [2:0] a, output wire [2:0] y);
+	sm2 inst(a[1:0], y[2:1]);
+	assign y[0] = !a[2];
+endmodule
+
+module top(input wire [4:0] a, output wire [4:0] y);
+	sm1 i1(.a(a[2:0]), .y(y[2:0]));
+	sm2 i2(.a(a[4:3]), .y(y[4:3]));
+endmodule
+EOF
+
+prep -top top
+# deal with arithmetic which is unsupported inside aiger2
+techmap t:$add
+
+splitnets -ports top
+write_aiger2 -flatten aiger2_flatten.aig
+flatten
+rename top gold
+read_aiger -module_name gate aiger2_flatten.aig
+miter -equiv -flatten gold gate miter
+sat -verify -prove trigger 0 miter