c++ front end - #253
Open
nanocoh wants to merge 75 commits into
Open
c++ front end#253nanocoh wants to merge 75 commits into
nanocoh wants to merge 75 commits into
Conversation
Preserve C2RTL extraction and equivalence support while integrating main's opaque-cone handling, reset/export options, and in-process result API.
This reverts commit 115362c.
Preserve C2RTL and compact SEC extraction while integrating paired instance boundaries, shared NajaEDA Python verification, Windows wheels, and regression reporting. Resolve CMake and extraction conflicts, keep XLS dependencies out of Python builds, and reject unsupported temporal C2RTL boundaries before synthesis.
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
runExtractedModels returns Equivalent without a proof when both sides are the same model object. The internal relation tests merged from main passed one model twice, so the exact IMC test saw Equivalent where it expects Inconclusive, and three others passed without reaching an engine. Pass an equal copy so every engine is exercised. Also restore the indentation of the brace repaired after the merge.
q2SelectorFor inserts a new selector and then evicts least-recently-used status selectors while the cache is over its limit. When every other cached selector was a blocking one, the victim was the selector just inserted: it was disabled and still returned, so the caller's predecessor query was trivially UNSAT and PDR could report a false proof. Skip the new entry when choosing the status victim.
Upstream moved ConfigTinyRocketSecVerificationAccepted to dual_rail_steady and later expects every output proved, which relation learning delivers only in dual-rail mode where every register has an initial fact. The fork still ran the test with binary k-induction from an earlier build fix, so the merged expectation failed at 8/132. Use upstream's config; the test now proves 132/132.
Figure 7 literal removal is optional strengthening, but its queries ran with the full predecessor limits, a budget-limited answer set the global exhaustion flag and turned the whole run inconclusive, and every attempt counted against the multi-output probe's query budget. On sv2v_sky130hd_gcd the honest engine therefore proved 1 of 18 outputs, while the retired-selector bug had made those queries free. Run generalization queries on the narrow probe limits, keep the literal when such a query is budget-limited instead of aborting the proof, and exempt them from the batch probe query count. Raise that count to 20000 now that it bounds only blocking and propagation work, and expose it through KEPLER_SEC_PDR_DUAL_RAIL_BATCH_PREDECESSOR_QUERY_LIMIT. The gcd batch now converges at frame 13 in 17 s and proves 18 of 18; the tinyrocket self-compare and the C2RTL examples are unchanged. The strategy tests also get a per-test verification generation, as the CLI has for every run, because the per-DNL logic-cloud caches are keyed by addresses that a later test's universe can reuse.
A combinational C++ encoder against a three-stage pipelined RTL that deliberately differs wherever a result is unused. The cases cover the conditional output relations proving with the operand range, a counterexample without that range, a counterexample under unconditional equality, contradictory constraints being rejected unless the reachability check is off, and a planted tag bug being caught inside the legal domain.
This branch has not been deployed
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
1 participant
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.