[ImportVerilog] Add support for countones.#10549
Conversation
Squash to 2 valued and then count in naive way (given this is for testing/simulation goals, kept the sum direct/naive). Used the minimum-width needed as the type here. Using the minimum width resulted in some type mismatches due to different type used by slang constant. To address this, changed the convertAssertionCallExpression to use materializeConversion for all returned system call values. As part of this also noticed there were redundant conversions being inserted. Introduced castToTwoValued to ensure system functions natively returning standard SV two-valued types do not undergo redundant 4-valued logic domain round-tripping. (could also perhaps have relied on canonicalize or createOrFold, but seemed local enough).
There was a problem hiding this comment.
I think currently countones result is sign extended in convertAssertionCallExpression, and could cause some mismatch:
$ cat bar.sv
module countones_bug(
input logic clk,
input logic [7:0] x
);
assert property (@(posedge clk)
$countones(x) == 8
);
endmodule
$circt-verilog bar.sv | firtool -format=mlir
// Generated by CIRCT 30931a055
module countones_bug( // <stdin>:2:3
input clk, // <stdin>:2:31
input [7:0] x // <stdin>:2:45
);
wire [3:0] _GEN =
{3'h0, x[0]} + {3'h0, x[1]} + {3'h0, x[2]} + {3'h0, x[3]} + {3'h0, x[4]}
+ {3'h0, x[5]} + {3'h0, x[6]} + {3'h0, x[7]}; // <stdin>:4:14, :5:10, :6:10, :7:10, :8:10, :9:10, :10:10, :11:10, :12:10, :13:10, :14:10, :15:11, :16:11, :17:11, :18:11, :19:11, :20:11, :21:11
assert property (@(posedge clk) {{28{_GEN[3]}}, _GEN} == 32'h8); // <stdin>:3:15, :21:11, :22:11, :23:11, :24:11, :25:11, :26:5
endmoduleI believe this is incorrect when x = 11111111.
The alternave considered was adding an extra bit here so that sign extension works, but skipping it is more efficient (at least by looking at the MLIR output).
|
You are correct yes - it was treating the expression as signed and as it was using just enough bits to capture unsigned output, failed. I switched to treating as unsigned (that also avoids expanding to 32-bit for the compare before the assert). I checked the other ones, and they seemed fine. Alternative considered was adding one extra bit so that sign extension is valid - cost is extra bits but does remove the ternary in the extension. |
|
Results of circt-tests run for c9e04ef compared to results for e2cbd2d: sv-testsChanges in emitted diagnostics:
|
fabianschuiki
left a comment
fabianschuiki
left a comment
There was a problem hiding this comment.
Hey @jpienaar, thanks for adding this! One nit: could we add this to Expressions.cpp instead of AssertionExpr.cpp? These builtins don't really have anything to do with SVAs and the LTL dialect, they are just regular SV builtins. (We'll probably want to eventually move IsUnknown, OneHot, and OneHot0 over into Expressions.cpp, too.
|
That is a good point, I had put them here as they were listed as unsupported in the LTL.md doc and I only had these inside assert blocks, so didn't think about that. Makes sense. |
|
|
||
| > The following functions are not yet supported by CIRCT: | ||
| > - **`$countones(a)`** | ||
| - **`$countones(a)`**: |
There was a problem hiding this comment.
Should I move these to Moore.md or add a new ImportVerilog.md doc? (and with this PR or a follow up?)
|
Results of circt-tests run for bdb7e33 compared to results for e2cbd2d: sv-testsChanges in emitted diagnostics:
|
|
Results of circt-tests run for 75cf609 compared to results for e2cbd2d: sv-testsChanges in emitted diagnostics:
|
3 participants
Squash to 2 valued and then count in naive way (given this is for
testing/simulation goals, kept the sum direct/naive). Used the
minimum-width needed as the type here.
Using the minimum width resulted in some type mismatches due to
different type used by slang constant. To address this, changed
the convertAssertionCallExpression to use materializeConversion for
all returned system call values.
As part of this also noticed there were redundant conversions being
inserted. Introduced castToTwoValued to ensure system functions natively
returning standard SV two-valued types do not undergo redundant 4-valued
logic domain round-tripping. (could also perhaps have relied on
canonicalize or createOrFold, but seemed local enough).
Assisted-by: Antigravity:Gemini