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

Fix bugs in several Yosys cell implementations #1817

Merged
merged 4 commits into from
Mar 9, 2023
Merged

Conversation

chameco
Copy link
Contributor

@chameco chameco commented Feb 9, 2023

Several SAW implementations of the semantics of Yosys cells did not match the expected behavior. This PR hopefully fixes a few instances of this (there are undoubtedly more). I also refactored out some duplicated code for e.g. handling bit order - this is a common source of error in the semantics, as the convention in SAWCore is opposite Yosys.

Longer-term, we should ensure that we have good reason to trust these cell definitions - if they're incorrect, we're not reasoning about anything useful! I think at least some randomized testing would be a good start, and I plan to implement something to address this in the future. #1816 tracks this need.

@RyanGlScott
Copy link
Contributor

Out of curiosity, what were the actual buggy parts of the code? (It's somewhat hard to tell due to all of the adjacent refactorings in the diff.)

@chameco
Copy link
Contributor Author

chameco commented Feb 13, 2023

Specifically, the issues were:

  • the logic_not cell was producing SAWCore that did not typecheck (an incorrect width was being passed to bvNonzero)
  • another incorrect width was being used in the reduce_* cells
  • incorrect endianness with the bitwise shift cells (shl etc.)
  • the shiftx and pmux cells were unimplemented

Copy link
Contributor

@RyanGlScott RyanGlScott left a comment

Choose a reason for hiding this comment

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

Ah, OK. Part of me wonders if we should always call flipEndianness before calling each operation to avoid issues like this in the future, but then again, that would impose an additional simulation-time cost. In lieu of that, perhaps it is worth grouping up the operations in the code that are sensitive to the endianness so that is easier to tell them apart.

I don't have much insight into the rest of the code, so my approval here is mostly a formality :)

@chameco
Copy link
Contributor Author

chameco commented Feb 13, 2023

Ah, OK. Part of me wonders if we should always call flipEndianness before calling each operation to avoid issues like this in the future, but then again, that would impose an additional simulation-time cost.

Yeah, I thought about this, but the term size increase scared me off (in addition to simulation time, I find myself reading parts of the resulting SAWCore terms quite often, and lots of redundant reverses make that obnoxious). There are probably some relatively easy solutions but for now ¯\_(ツ)_/¯. I think the larger problem in any case is the lack of more exhaustive testing, which I hope to address in the (near?) future.

Thanks for the review!

@chameco chameco added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Feb 13, 2023
@chameco chameco merged commit 8eaf10e into master Mar 9, 2023
@mergify mergify bot deleted the sb/yosys-cells branch March 9, 2023 04:41
@RyanGlScott RyanGlScott added the subsystem: hardware Issues related to verification of hardware label Jun 20, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: hardware Issues related to verification of hardware
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants