From 2e2935f3a53fd7d68bb8fce3802945c2b9b98a5b Mon Sep 17 00:00:00 2001
From: Martin Erhart <maerhart@outlook.com>
Date: Fri, 29 Nov 2024 11:41:05 +0000
Subject: [PATCH] [circt-bmc] Add a simple test with a register storing an
 aggregate

---
 integration_test/circt-bmc/seq.mlir | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/integration_test/circt-bmc/seq.mlir b/integration_test/circt-bmc/seq.mlir
index 9f65a8494922..28369d33931a 100644
--- a/integration_test/circt-bmc/seq.mlir
+++ b/integration_test/circt-bmc/seq.mlir
@@ -17,3 +17,17 @@ hw.module @StateProp(in %clk: !seq.clock, in %i0: i1) {
   %imp = comb.or bin %nclk, %eq : i1
   verif.assert %imp : i1
 }
+
+// RUN: circt-bmc %s -b 10 --module aggregateReg --shared-libs=%libz3 | FileCheck %s --check-prefix=AGGREGATEREG
+// Can be violated because the register does not have an initial value specified.
+// TODO: add support for aggregate initial values and adjust this test accordingly.
+// AGGREGATEREG: Assertion can be violated!
+hw.module @aggregateReg(in %clk: !seq.clock) {
+  %c0 = hw.constant 0 : i32
+  %arr = hw.array_create %c0, %c0 : i32
+  %res = seq.compreg %arr, %clk : !hw.array<2xi32>
+  %idx = hw.constant 0 : i1
+  %get = hw.array_get %res[%idx] : !hw.array<2xi32>, i1
+  %eq = comb.icmp bin eq %c0, %get : i32
+  verif.assert %eq : i1
+}