Skip to content

Conversation

kroening
Copy link
Collaborator

No description provided.

@kroening kroening force-pushed the verilog_equality branch 2 times, most recently from d2bd5da to 2c6ff3c Compare July 15, 2024 14:27
@kroening kroening marked this pull request as ready for review July 15, 2024 14:52

tc_binary_expr(expr);

// This returns 'x' if either of the operands contains x or z.
Copy link
Collaborator

Choose a reason for hiding this comment

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

I have to admit that I don't understand how this comment relates to or explains what follows?!

Copy link
Collaborator Author

@kroening kroening Jul 16, 2024

Choose a reason for hiding this comment

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

Maybe by example:

'b0 == 'b0 is 0
'b1x == 'b10 is x
'b1z == 'b1z is x

Hence, if both operands are two-valued, the result is two-valued. If either operand is four-valued, the result is four-valued.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I understand the example and was assuming as much, but the code that follows just deals with types, it doesn't actually change the expression id or the likes. To me, the comment suggested that the code that follows actually evaluates the expression (or, rather, constructs some code to produce a value for the given operands).

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

It does change the ID when it's two-valued -- lines 2431 and 2433.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Yes, but not in the four-valued case. So I was just a bit confused - but really only by the comment, not the actual implementation.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yes, in the four-valued case, the ID stays D_verilog_logical_equality/D_verilog_logical_inequality. I'll add a comment for that.

The Verilog logical equality and inequality now have their own ID as they
return a four-valued result when applied to four-valued logic.

When applied to two-valued logic, the typechecker maps these to mathematical
equality.
@kroening kroening merged commit 61e797f into main Jul 16, 2024
@kroening kroening deleted the verilog_equality branch July 16, 2024 21:15
Romy15200 pushed a commit to Romy15200/nws that referenced this pull request Aug 19, 2025
Verilog logical (in)equality expression
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants