Conversation
Accept VHDL for both designs through -vhdl or format: vhdl, using Naja's VHDL constructor. Top entities are selected per design with vhdl_design1_top and vhdl_design2_top. Naja loads one VHDL file per call and keeps earlier sources in the library, so files are loaded in the order given and must be in compile order. The requested top is elaborated after the last file. VHDL requires SEC verification, as the SystemVerilog formats do.
A truth table was converted to one term per row whose output is 1. That form is right for 0/1 inputs but pessimistic for unknown ones: a term never evaluates to 1 while it tests an unknown input, even when the known inputs already decide the output. In dual-rail SEC this kept a register unknown forever when it resets to 1 through a mux and only depends on itself, so its outputs were never compared and different designs were reported equivalent. Use the prime implicants of the table instead. They agree with the rows on 0/1 inputs and are exact for unknown inputs. Tables with more than 10 relevant inputs keep one term per row.
With a reset bootstrap, binary SEC assumes that the outputs agree on the first frame after reset unless the post-reset state is known. That state is no longer computed, so the assumption always applies. When the reset values of the two designs differ, no trace satisfies it and every engine then proves an empty problem. Check before dispatching to an engine whether any reset trace lets the outputs agree on that frame. If none does, report the mismatch with a counterexample.
Each evaluation memo was sized when its root was registered. Roots compiled afterwards add parents to nodes they share with earlier roots, and propagation visits those parents in every memo, reading past the end of the older ones. Add VHDL regression tests for this and for the reset frontier mismatch.
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
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.