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

ARM: Add signed multiply halfwords instructions #644

Merged
merged 1 commit into from
Nov 18, 2023
Merged

ARM: Add signed multiply halfwords instructions #644

merged 1 commit into from
Nov 18, 2023

Conversation

sarranz
Copy link
Collaborator

@sarranz sarranz commented Nov 12, 2023 •
edited
Loading

Closes #358.

@sarranz sarranz marked this pull request as draft November 12, 2023 21:33
@sarranz sarranz marked this pull request as ready for review November 12, 2023 22:35
bgregoir
bgregoir reviewed Nov 13, 2023
View reviewed changes
Copy link
Contributor

@bgregoir bgregoir left a comment

Choose a reason for hiding this comment

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

I think the current semantic is wrong. Also, I do not like the fact that we add 4 versions of the "same" operation. Is it possible to add only a single parametric constructor ?

proofs/compiler/arm_instr_decl.v Outdated Show resolved Hide resolved
@sarranz
Copy link
Collaborator Author

sarranz commented Nov 13, 2023

I think the current semantic is wrong. Also, I do not like the fact that we add 4 versions of the "same" operation. Is it possible to add only a single parametric constructor ?

I also think this would be better. I did this initially and added the four specific names as extra_ops. But then I thought that to avoid introducing four new things that need maintenance, I was introducing five. Do you think it would be better that way?

@sarranz sarranz marked this pull request as draft November 13, 2023 09:32
@sarranz
Copy link
Collaborator Author

sarranz commented Nov 15, 2023

I introduced 3 parametric mnemonics, and redefined the semantics so that it coincides more directly with the ARM documentation.
I don't know if my definition of split_32_2x16 is ideal, same with the use of \bits16 in EasyCrypt.
Also, unrelated, I added conditional to the test of CLZ.

@sarranz sarranz marked this pull request as ready for review November 15, 2023 20:58
bgregoir
bgregoir reviewed Nov 16, 2023
View reviewed changes
Copy link
Contributor

@bgregoir bgregoir left a comment

Choose a reason for hiding this comment

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

Excepted that, I think it is ok.

eclib/JModel_m4.ec Outdated Show resolved Hide resolved
vbgl
vbgl reviewed Nov 16, 2023
View reviewed changes
proofs/lang/word.v Outdated Show resolved Hide resolved
@bgregoir bgregoir merged commit 778d2df into main Nov 18, 2023
1 check passed
@bgregoir bgregoir deleted the arm-add-subword-mul branch November 18, 2023 20:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@vbgl vbgl vbgl left review comments

@bgregoir bgregoir bgregoir approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Add ARM Cortex M4 instructions for subword multiplication
3 participants
@sarranz @bgregoir @vbgl