-
Notifications
You must be signed in to change notification settings - Fork 309
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[HW][circt-synth] Implement AggregateToComb pass and add to circt-synth pipeline #8068
base: main
Are you sure you want to change the base?
Changes from 1 commit
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,7 +1,7 @@ | ||
// REQUIRES: libz3 | ||
// REQUIRES: circt-lec-jit | ||
|
||
// RUN: circt-opt %s --convert-comb-to-aig --convert-aig-to-comb -o %t.mlir | ||
// RUN: circt-opt %s --hw-aggregate-to-comb --convert-comb-to-aig --convert-aig-to-comb -o %t.mlir | ||
// RUN: circt-lec %t.mlir %s -c1=bit_logical -c2=bit_logical --shared-libs=%libz3 | FileCheck %s --check-prefix=COMB_BIT_LOGICAL | ||
// COMB_BIT_LOGICAL: c1 == c2 | ||
hw.module @bit_logical(in %arg0: i32, in %arg1: i32, in %arg2: i32, in %arg3: i32, | ||
|
@@ -78,3 +78,19 @@ hw.module @shift5(in %lhs: i5, in %rhs: i5, out out_shl: i5, out out_shr: i5, ou | |
%2 = comb.shrs %lhs, %rhs : i5 | ||
hw.output %0, %1, %2 : i5, i5, i5 | ||
} | ||
|
||
// RUN: circt-lec %t.mlir %s -c1=array -c2=array --shared-libs=%libz3 | FileCheck %s --check-prefix=COMB_ARRAY | ||
// COMB_ARRAY: c1 == c2 | ||
hw.module @array(in %arg0: i2, in %arg1: i2, in %arg2: i2, in %arg3: i2, in %sel1: i2, in %sel2: i2, out out1: i2, out out2: i2) { | ||
%0 = hw.array_create %arg0, %arg1, %arg2, %arg3 : i2 | ||
%1 = hw.array_get %0[%sel1] : !hw.array<4xi2>, i2 | ||
%2 = hw.array_create %arg0, %arg1, %arg2 : i2 | ||
%c3_i2 = hw.constant 3 : i2 | ||
// NOTE: If the index is out of bounds, the result value is undefined. | ||
// In LEC such value is lowered into unbounded SMT variable and cause | ||
// the LEC to fail. So just asssume that the index is in bounds. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yeah, for these kind of things, a translation validation tool would be quite nice 🙂 There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yeah without circt-lec it has been almost impossible to implement lowering pattern with confidence for the correctness. Thank you @maerhart @frog-in-the-well @TaoBi22 for outstanding work! |
||
%inbound = comb.icmp ult %sel2, %c3_i2 : i2 | ||
verif.assume %inbound : i1 | ||
%3 = hw.array_get %2[%sel2] : !hw.array<3xi2>, i2 | ||
hw.output %1, %3 : i2, i2 | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we mention here how it changes the behavior? If I understand correctly it's just a refinement, so we're all good and wouldn't even need to mention it here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes. I'll do.
Yes, it's refinement so it should be fine from the semantics perspective but i would at least mention in the doc. Maybe in the future we might want to run post-synthesis simulation on arcilator but only pre-synthesis IR can catch out-of-bounds access in this case.