Do not infer a memory for an array written from several always blocks - #455
Merged
Merged
Conversation
Bring the shared Python runtime SDK and safe parameter lifetimes onto main, on top of the upstream 0.7.26 changes. Kepler Formal's Python package depends on these (najaeda.sdk, NajaPythonRuntimeAPI.h, NLUniverse::getRuntimeIdentity, DNL::exchange). Conflict in src/core/NajaVersion.h.in resolved to 0.7.24.dev0, the development provider version Kepler Formal pins. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
The fix7 merge carried its 0.7.24.dev0 version onto main. Use the version from main instead so the provider built from this source matches the release it is based on. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Memory inference matched one sequential block per array. When an unpacked array was written by one always block per element, as a generate loop produces, the first block became the memory's write port and the others were skipped as already inferred. The generic sequential lowering then built a flop for each skipped block, and that flop drove the memory's read data net a second time. Every cone through such a net was unverifiable. Count the sequential blocks that write each candidate array first. An array with more than one writer block is left to the generic sequential lowering for all of its writers, with a warning naming the array and the number of blocks. Arrays with a single writer block are unchanged. Reported in keplertech/kepler-formal#250 on Systolic_MAC_with_DFT, whose self compare covered 15 of 24 outputs. It now proves 24 of 24.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #455 +/- ##
==========================================
- Coverage 97.30% 97.20% -0.10%
==========================================
Files 246 237 -9
Lines 45463 43374 -2089
==========================================
- Hits 44237 42162 -2075
+ Misses 1226 1212 -14
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Install the headers matching the wheel's libraries under najaeda/sdk/include and keep the Windows export change. A native consumer such as kepler-formal resolves the installed libraries, validates the build and swaps the DNL singleton itself, so remove sdk.py, the CMake package and build identity files, the _C_API capsule, NLUniverse::getRuntimeIdentity, DNL::exchange and their tests.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.