@@ -458,6 +458,59 @@ TEST_F(ArrayUntuplePassTest, ProcStateArrayImplicitNext) {
458458 m::StateElement (_, m::Type (" bits[3][4]" ))}));
459459}
460460
461+ TEST_F (ArrayUntuplePassTest, ProcStateArrayActiveMultiReadOptimization) {
462+ auto p = CreatePackage ();
463+ XLS_ASSERT_OK_AND_ASSIGN (
464+ auto chan_resp, p->CreateStreamingChannel (" resp" , ChannelOps::kSendOnly ,
465+ p->GetBitsType (3 )));
466+ ProcBuilder pb (TestName (), p.get ());
467+ BValue state = pb.StateElement (
468+ " foo" , ValueBuilder::ArrayB ({
469+ ValueBuilder::Tuple ({ValueBuilder::Bits (UBits (0 , 1 )),
470+ ValueBuilder::Bits (UBits (1 , 3 ))}),
471+ }));
472+
473+ // Read #1: Extract the inner tuple value out of the array
474+ BValue extracted_tuple = pb.ArrayIndex (state, {pb.Literal (UBits (0 , 1 ))});
475+ BValue extracted_data = pb.TupleIndex (extracted_tuple, 1 );
476+
477+ // Send required by equivalence checker to observe proc mutations
478+ pb.Send (chan_resp, pb.Literal (Value::Token ()), extracted_data);
479+
480+ // Read #2: Perform an independent update on the state
481+ BValue updated_tuple = pb.Tuple ({pb.Literal (UBits (1 , 1 )), extracted_data});
482+ BValue next_state =
483+ pb.ArrayUpdate (state, updated_tuple, {pb.Literal (UBits (0 , 1 ))});
484+
485+ XLS_ASSERT_OK_AND_ASSIGN (Proc * pr, pb.Build ({next_state}));
486+ solvers::z3::ScopedVerifyProcEquivalence svpe (pr, /* activation_count=*/ 2 ,
487+ /* include_state=*/ false );
488+ ScopedRecordIr sri (p.get ());
489+ ASSERT_THAT (RunPass (p.get ()), IsOkAndHolds (true ));
490+ EXPECT_THAT (pr->StateElements (),
491+ IsSupersetOf ({m::StateElement (_, m::Type (" bits[1][1]" )),
492+ m::StateElement (_, m::Type (" bits[3][1]" ))}));
493+ }
494+
495+ TEST_F (ArrayUntuplePassTest, ProcStateArrayIdentityUpdateOnly) {
496+ auto p = CreatePackage ();
497+ ProcBuilder pb (TestName (), p.get ());
498+ BValue state = pb.StateElement (
499+ " foo" , ValueBuilder::ArrayB ({
500+ ValueBuilder::Tuple ({ValueBuilder::Bits (UBits (0 , 1 )),
501+ ValueBuilder::Bits ((UBits (1 , 3 )))}),
502+ }));
503+ pb.Next (state, state);
504+
505+ XLS_ASSERT_OK (pb.Build ().status ());
506+ ScopedRecordIr sri (p.get ());
507+
508+ ArrayUntuplePass pass;
509+ PassResults res;
510+ OptimizationContext ctx;
511+ ASSERT_THAT (pass.Run (p.get (), {}, &res, ctx), IsOkAndHolds (false ));
512+ }
513+
461514void IrFuzzArrayUntuple (FuzzPackageWithArgs fuzz_package_with_args) {
462515 ArrayUntuplePass pass;
463516 OptimizationPassChangesOutputs (std::move (fuzz_package_with_args), pass);
0 commit comments