Skip to content

Procedural blocks and expressions #85

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.

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

Draft
wants to merge 5 commits into
base: master
Choose a base branch
from
Draft

Procedural blocks and expressions #85

wants to merge 5 commits into from

Conversation

GlebChili
Copy link
Collaborator

No description provided.

@buzden buzden requested review from L3odr0id and buzden May 12, 2025 14:20
Comment on lines +271 to +273
(==) x y with (decEq x y)
_ | Yes _ = True
_ | No _ = False
Copy link
Collaborator

@buzden buzden May 12, 2025

Choose a reason for hiding this comment

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

(==) = isYes .: decEq

@@ -11,3 +11,5 @@ import public Test.Verilog.Module
Test.Verilog.Module.genNotEqFin = deriveGen
Test.Verilog.Module.genSourceForSink = deriveGen
Test.Verilog.Module.genModules = deriveGen

Test.Verilog.ProceduralBlock.genProceduralBlock = deriveGen
Copy link
Collaborator

Choose a reason for hiding this comment

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

Should be done in Test.Verilog.ProceduralBlock.Derived

@buzden
Copy link
Collaborator

buzden commented May 12, 2025

@L3odr0id, I' d like to hear your optinion on:

  • how proposed expressions are modelled;
  • whether or not proposed expressions are usable in your part of the model;
  • this proposition contains some notion of type compatibility; is it correct and how does it correspond to the notion of port assignability in your part of the model; whether they should be harmonised?

ArrSupremum (Packed @{al1} (Arr x) start1 end1) (Packed @{al2} (Arr y) start2 end2) (Packed @{al3} (Arr z) startR endR)

public export
data SVBinaryOperator : (lType : SVType) -> (rType : SVType) -> (retType : SVType) -> Type where
Copy link
Collaborator

Choose a reason for hiding this comment

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

I think that the result of each specific operation isn't that important. Do we really need to declare a new constructor for each operation? Maybe we could, for example, define a single constructor for all binary bitwise, modulus, shift operations, then a single constructor for all arithmetic and logical operations etc. Of course, to create such group constructors, it is necessary to check which operand data types each operation supports.

Then we could implement a non-deterministic printer. For example, for the binary operation with integral operands we can choose and print any symbol like & | >> <<

There is a full list of operators from IEEE:

||| Table 11-1—Operators and data types
||| | Operator Token      | Name                                  | Operand Data Types                  |
||| |---------------------|---------------------------------------|-------------------------------------|
||| | =                   | Binary assignment operator            | Any                                 |
||| | += -= /= *=         | Binary arithmetic assignment operators| Integral, real, shortreal           |
||| | %=                  | Binary arithmetic modulus assignment  | Integral                            |
||| | &= |= ^=            | Binary bitwise assignment operators   | Integral                            |
||| | >>= <<=             | Binary logical shift assignment       | Integral                            |
||| | >>>= <<<=           | Binary arithmetic shift assignment    | Integral                            |
||| | ?:                  | Conditional operator                  | Any                                 |
||| | + -                 | Unary arithmetic operators            | Integral, real, shortreal           |
||| | ~                   | Unary bitwise negation operator       | Integral                            |
||| | !                   | Unary logical negation operator       | Integral, real, shortreal           |
||| | & ~& | ~| ^ ~^ ^~   | Unary reduction operators             | Integral                            |
||| | + - * / **          | Binary arithmetic operators           | Integral, real, shortreal           |
||| | %                   | Binary arithmetic modulus operator    | Integral                            |
||| | & | ^ ^~ ~^         | Binary bitwise operators              | Integral                            |
||| | >> <<               | Binary logical shift operators        | Integral                            |
||| | >>> <<<             | Binary arithmetic shift operators     | Integral                            |
||| | && || –> <–>        | Binary logical operators              | Integral, real, shortreal           |
||| | < <= > >=           | Binary relational operators           | Integral, real, shortreal           |
||| | === !==             | Binary case equality operators        | Any except real and shortreal       |
||| | == !=               | Binary logical equality operators     | Any                                 |
||| | ==? !=?             | Binary wildcard equality operators    | Integral                            |
||| | ++ --               | Unary increment, decrement operators  | Integral, real, shortreal           |
||| | inside              | Binary set membership operator        | Singular for the left operand       |
||| | dist                | Binary distribution operator          | Integral                            |
||| | {} {{}}             | Concatenation, replication operators  | Integral                            |
||| | {<<{}} {>>{}}       | Stream operators                      | Integral                            |

Copy link
Collaborator

Choose a reason for hiding this comment

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

Also if we don't need to get the exact SVType as a result of an expression, we can define the type of the expression (and operand) like this:

public export
data DataType = Any' | Integral' | Real' -- Real' = Real + ShortReal

UwireIsIntegral : IsIntegralType (Var Uwire')
IntIsIntegral : IsIntegralType (Var Int')
IntegerIsIntegral : IsIntegralType (Var Integer')
UnpackedArrysIsIntegral : IsIntegralType t -> IsIntegralType (Arr (Unpacked t s e))
Copy link
Collaborator

@L3odr0id L3odr0id May 12, 2025

Choose a reason for hiding this comment

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

I'm not sure that an unpacked array can be an integral type. IEEE says

||| 6.11.1 Integral types
|||
||| The term integral is used throughout this standard to refer to the data types that can represent a single basic
||| integer data type, packed array, packed structure, packed union, or enum.

I would use VarOrPacked to filter values of packed types

SVBitwiseNegationPacked : AllowedInPackedArr iType => IsIntegralType iType => SVUnaryOperator (Arr $ Packed iType s e) (Arr $ Packed iType s e)

public export
data SVExpression : (expressionType : SVType) -> (ports : PortsList) -> (usedPorts : ListOfPortsIndices ports) -> Type where
Copy link
Collaborator

Choose a reason for hiding this comment

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

Does this ports list represent connections outside the context of the expression?

@L3odr0id
Copy link
Collaborator

@buzden

@L3odr0id, I' d like to hear your optinion on:

  • how proposed expressions are modelled;

Actually I think they are too explicit. I suggest making the expressions declarations more abstract. But this should be discussed further to find the most useful implementation

  • whether or not proposed expressions are usable in your part of the model;
  • this proposition contains some notion of type compatibility; is it correct and how does it correspond to the notion of port assignability in your part of the model; whether they should be harmonised?

It seems that expressions take a PortsList as input. We can easily pass the connection types from the context into these expressions. This means these expressions are fully compatible with my part of the model. Although It's not clear to me how to resolve names of these ports in the printer.

Also, I like that this PR adds decEq. I’ve been avoiding it for months 😅

||| — Unpacked array element bit-select or part-select, element, or slice
||| — A call to a user-defined function, system function, or method that returns any of the above
public export
data SVExpression : (expressionType : SVType) -> (ports : PortsList) -> (usedPorts : ListOfPortsIndices ports) -> Type
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Consider using Fin lists instead of ListOfPortsIndices for better support of pretty printers.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants