search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
442 stars 63 forks source link

Delete experimental CompositionalTranslation.hs #2131

Closed mccleeary-galois closed 1 month ago

mccleeary-galois commented 1 month ago

Delete experimental CompositionalTranslation.hs and convert back to using Netgraph.hs in Yosys as the CompositionalTranslation graph was ballooning in memory.

Close #1944 Close #1946

RyanGlScott commented 1 month ago

Thanks for working on this! Although the compositional VHDL verification features were highly experimental, we should still advertise their removal in the changelog as a precaution.

Have you confirmed whether this allows SAW to load some large VHDL test cases that used to work (e.g., the test case in #1944)? They are large enough that I don't think we'd want to use them as regression tests, but it would still be worthwhile to check to see if they work now.

mccleeary-galois commented 1 month ago

Thanks for working on this! Although the compositional VHDL verification features were highly experimental, we should still advertise their removal in the changelog as a precaution.

Have you confirmed whether this allows SAW to load some large VHDL test cases that used to work (e.g., the test case in #1944)? They are large enough that I don't think we'd want to use them as regression tests, but it would still be worthwhile to check to see if they work now.

I have confirmed on a few. I was going to add a previously failing test as well to this draft before marking it as ready for full review. Agreed on updating the changelog as well.

mccleeary-galois commented 1 month ago

Another regression that might need to be fixed: https://github.com/GaloisInc/saw-script/issues/1946