Skip to content
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

Add $check cell to represent assertions with messages #4128

Merged
merged 6 commits into from
Feb 3, 2024

Conversation

whitequark
Copy link
Member

@whitequark whitequark commented Jan 11, 2024

Relates to #4143.

@whitequark whitequark requested a review from jix January 11, 2024 09:40
@whitequark whitequark requested a review from zachjs as a code owner January 11, 2024 09:40
@jix jix added the check-sby Run sby tests for this PR label Jan 11, 2024
@jix
Copy link
Member

jix commented Jan 11, 2024

Just leaving a note that async2sync and clk2fflogic will require support to lower $check into $assert/$assume/etc before merging this to avoid breaking our formal verification flows. (I added the check-sby label which should cause jenkins CI runs to also run the SBY tests exercising the FV flows.)

@whitequark
Copy link
Member Author

Just leaving a note that async2sync and clk2fflogic will require support to lower $check into $assert/$assume/etc before merging this

You mentioned that you would be able to do this--is that still the case?

@povik
Copy link
Member

povik commented Jan 19, 2024

Just occurred to me, so noting it down: we need to visit set_keep_assert in hierarchy.c in this PR

@whitequark
Copy link
Member Author

we need to visit set_keep_assert in hierarchy.c in this PR

Done

@whitequark
Copy link
Member Author

From my point of view this PR is done, though of course it breaks formal flows, and the tests that are looking for formal flow cells don't pass.

@jix
Copy link
Member

jix commented Jan 22, 2024

My branch with the necessary yosys changes to keep the FV flows working by handling $check cells in async2sync and clk2fflogic and by ensuring that all yosys tests call either as required is at https://github.com/jix/yosys/tree/check-fv-compat (which contains a cherry-pick of this PR's commit, such that the tests pass before and after $check is added). It passes all yosys tests apart from tests/verilog/conflict_assert.ys which we discussed during the dev JF (I didn't look more into that yet).

The corresponding changes on the SBY side are at YosysHQ/sby#259 which keeps all SBY tests passing when using the yosys from my check-fv-compat branch.

@whitequark
Copy link
Member Author

whitequark commented Jan 22, 2024

Fantastic work! Thank you @jix. I'll take a look at the final test failure, probably, tomorrow.

@whitequark
Copy link
Member Author

I've updated the PR to not emit an assertion message in the Verilog frontend and to ignore empty message in the Verilog backend; and to check for non-unique names of procedural assertions. I think that's all!

@whitequark
Copy link
Member Author

There are a few failures of the kind:

ERROR: Failed to import cell $assert$static_cast_simple.sv:35$6 (type $check) to SAT database.

@jix
Copy link
Member

jix commented Jan 23, 2024

Ah I missed the tests that end up using read instead of read_verilog as the build I was using has verific enabled which doesn't yet emit $check cells. I'll go over the remaining tests with verific disabled later today.

@whitequark whitequark changed the title [WIP] Add $check cell to represent assertions with messages Add $check cell to represent assertions with messages Jan 23, 2024
@whitequark
Copy link
Member Author

@jix @povik Any further review comments, or are we basically done with this patch?

@povik
Copy link
Member

povik commented Jan 23, 2024

@whitequark I can have a final look-over tomorrow.

@whitequark
Copy link
Member Author

Thanks, that would be great.

passes/sat/async2sync.cc Outdated Show resolved Hide resolved
passes/sat/clk2fflogic.cc Outdated Show resolved Hide resolved
passes/sat/clk2fflogic.cc Outdated Show resolved Hide resolved
passes/cmds/chformal.cc Outdated Show resolved Hide resolved
passes/cmds/chformal.cc Outdated Show resolved Hide resolved
passes/cmds/chformal.cc Outdated Show resolved Hide resolved
Copy link
Member

@povik povik left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I went through all of it, only skipped some of the CXXRTL bits, and other than the things I commented on nothing jumped at me.

jix and others added 5 commits February 1, 2024 16:14
This compares the write_smt2 output pretty much verbatim, which contains
auto generated private names and fixes an arbitrary ordering. The tested
functionality is also covered by SBY tests which actually interpret the
write_smt2 output using an SMT solver and thus are much more robust, so
we can safely remove this test.
Right now neither `sat` nor `sim` have support for the `$check` cell.
For formal verification it is a good idea to always run either
async2sync or clk2fflogic which will (in a future commit) lower `$check`
to `$assert`, etc.

While `sim` should eventually support `$check` directly, using
`async2sync` is ok for the current tests that use `sim`, so this commit
also runs `async2sync` before running sim on designs containing
assertions.
This adds support for `$check` cells in chformal and adds a `-lower`
mode which converts `$check` cells into `$assert` etc. cells with a
`$print` cell to output the `$check` message.
@jix jix force-pushed the check-cell branch 2 times, most recently from 88681fb to d29a294 Compare February 2, 2024 12:42
Copy link
Member

@jix jix left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should address everything @povik brought up during review and also adds some tests that would have detected the issues with the now fixed clk2fflogic code and now also passes all tests on CI including the SBY tests.

@whitequark
Copy link
Member Author

I'll do the honors.

@whitequark whitequark merged commit 3caac53 into YosysHQ:master Feb 3, 2024
17 checks passed
@whitequark whitequark deleted the check-cell branch February 3, 2024 18:39
cell->setPort(ID::EN, module->And(NEW_ID, sig_en_sampled, sig_trg_combined));
cell->setPort(ID::ARGS, sig_args_sampled);
if (cell->type == ID($check)) {
SigBit sig_a_sampled = sample_data(module, sig_en, State::S1, false, false).sampled;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should be sampling sig_a

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
check-sby Run sby tests for this PR
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants