Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix input ordering isses in Verilog generation #1294

Merged
merged 12 commits into from
May 21, 2021
Merged

Fix input ordering isses in Verilog generation #1294

merged 12 commits into from
May 21, 2021

Conversation

atomb
Copy link
Contributor

@atomb atomb commented May 14, 2021 •
edited
Loading

This adapts SAWScript to GaloisInc/what4#122 allowing SAW to control the order of inputs in generated Verilog modules.

Fixes GaloisInc/what4#121 and the associated buggy counterexamples in SAW.

Aaron Tomb added 9 commits May 17, 2021 16:28
Adapt to What4 Verilog interface changes
7d6edba
Fix w4_abc_verilog counterexamples
af6e5ef
Adapt write_verilog to use improved input ordering
6543d15 
This builds on the same changes to What4 used to fix counterexamples
for w4_abc_verilog.
Add the changes to What4 that this code depends on
41c2a49
Add test for ABC/Verilog counterexample ordering
ad5ad12
Bump what4 submodule
b522cfd
Remove unused language extension
34c5afc
Remove unused import
636cbf2
Better solution to ordering of Verilog CEXs
6afd00e 
Instead of ad-hoc reversing in various places, adapt readFiniteValues
to be parameterized by endianness. Typical Verilog ordering, including
in that generated by What4, is little endian.
@atomb atomb marked this pull request as ready for review May 18, 2021 15:25
robdockins
robdockins approved these changes May 18, 2021
View reviewed changes
Copy link
Contributor

@robdockins robdockins left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

minor nitpicks, otherwise looks OK to me

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs Outdated Show resolved Hide resolved
saw-core/src/Verifier/SAW/FiniteValue.hs Show resolved Hide resolved
@atomb atomb added the ready-to-merge If at least one person approves this PR, automatically merge it when CI finishes successfully. label May 21, 2021
@mergify mergify bot merged commit 5535b03 into master May 21, 2021
@mergify mergify bot deleted the at-verilog-inputs branch May 21, 2021 21:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@robdockins robdockins robdockins approved these changes

@brianhuffman brianhuffman Awaiting requested review from brianhuffman

Assignees
No one assigned
Labels
ready-to-merge If at least one person approves this PR, automatically merge it when CI finishes successfully.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

The order of inputs in generated Verilog is unpredictable
2 participants
@atomb @robdockins