Skip to content

Adopt register initial values from initial blocks in SEC - #256

Draft
Emin017 wants to merge 14 commits into
keplertech:mainfrom
Emin017:emin/support-initial-statement
Draft

Emin017 wants to merge 14 commits into
keplertech:mainfrom
Emin017:emin/support-initial-statement

Conversation

@Emin017

@Emin017 Emin017 commented Sep 22, 2026

Copy link
Copy Markdown

We hit a hard failure when loading SystemVerilog designs containing initial blocks into kepler-formal. Following the approach used by yosys-slang (evaluate initialization at load time in the frontend, store it as DFF INIT metadata, let downstream consumers just read it), we added initial-value support to SEC: the naja frontend now canonicalizes sized bit-literal parameters to a canonical binary form at the boundary, and SEC extraction harvests INIT into initialStateValueByKey, with no engine changes. Covered by unit tests and end-to-end CLI checks.

@Emin017

Emin017 commented Sep 22, 2026

Copy link
Copy Markdown
Author

One question before opening PRs: the change spans two repositories, and thirdparty/naja in kepler-formal points to your fork (nanocoh/naja) rather than najaeda/naja — we're unsure how that fork tracks upstream. How would you like the PRs organized: a PR to nanocoh/naja first, then a kepler-formal PR bumping the submodule? Or should the naja-side change go to najaeda/naja upstream? Happy to reshape the commits either way.

@nanocoh

nanocoh commented Sep 23, 2026

Copy link
Copy Markdown
Contributor

Hello @Emin017 and thank you for your interest in the project! :)

As the project is still growing rapidly, we prefer for now that our users will file issues rather than open PRs as it is hard to stabilize across our development. We are trying to be extremely responsive and fast with solving the issues!

For issues, we need a clear description of the problem + a reproduction test that can be included in the unit tests after the fix.

Will this work for you?

@Emin017

Emin017 commented Sep 23, 2026

Copy link
Copy Markdown
Author

Hello @Emin017 and thank you for your interest in the project! :)

As the project is still growing rapidly, we prefer for now that our users will file issues rather than open PRs as it is hard to stabilize across our development. We are trying to be extremely responsive and fast with solving the issues!

For issues, we need a clear description of the problem + a reproduction test that can be included in the unit tests after the fix.

Will this work for you?

Got it, I’ll put together a summary report of the issues first :)

@Emin017
Emin017 marked this pull request as draft September 23, 2026 08:35
@codecov

codecov Bot commented Sep 24, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 95.65217% with 2 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
src/sec/model/SequentialDesignModel.cpp 95.65% 2 Missing ⚠️

📢 Thoughts on this report? Let us know!

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants