diff --git a/src/Test/Verilog/Expression.idr b/src/Test/Verilog/Expression.idr
new file mode 100644
index 0000000..6a37fa9
--- /dev/null
+++ b/src/Test/Verilog/Expression.idr
@@ -0,0 +1,192 @@
+module Test.Verilog.Expression
+
+import Data.Fuel
+import Data.Vect
+
+import public Data.So
+
+import Test.DepTyCheck.Gen
+import Test.DepTyCheck.Gen.Coverage
+
+import public Test.Verilog.Module
+
+import public Test.Verilog.Literal
+
+
+%default total
+
+||| IEEE 1800-2023, 11.2
+||| An expression is a construct that combines operands with operators to produce a result that is a function of
+||| the values of the operands and the semantic meaning of the operator. Any legal operand, such as a net bit-
+||| select, without any operator is considered an expression. Wherever a value is needed in a SystemVerilog
+||| statement, an expression can be used.
+||| An operand can be one of the following:
+||| — Constant literal number, including real literals
+||| — String literal
+||| — Parameter, including local and specify parameters
+||| — Parameter bit-select or part-select, including local and specify parameters
+||| — Net (see 6.7)
+||| — Net bit-select or part-select
+||| — Variable (see 6.8)
+||| — Variable bit-select or part-select
+||| — Structure, either packed or unpacked
+||| — Structure member
+||| — Packed structure bit-select or part-select
+||| — Union, packed, unpacked, or tagged
+||| — Union member
+||| — Packed union bit-select or part-select
+||| — Array, either packed or unpacked
+||| — Packed array bit-select, part-select, element, or slice
+||| — 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
+
+||| The full list of available operators is described in the section 11.3 of the IEEE 1800-2023 standard.
+||| We deviate from the standard in the following ways:
+||| - Assignment operators are not included, they are considered the part of the statements instead.
+||| - Ternary conditioanl operator is included dirtectly into the expression type.
+
+||| Encodes that third SVType is the common supertype of the first two.
+||| TODO: Introduce a propper order lattice structure to the type.
+public export
+data SupremumType : SVBasic -> SVBasic -> SVBasic -> Type where
+  BitLogicLogic : SupremumType Bit' Logic' Logic'
+  LogicWireWire : SupremumType Logic' Wire' Wire'
+  BitWireWire : SupremumType Bit' Wire' Wire'
+  SupremumSym : SupremumType x y z => SupremumType y x z
+  SupremumReflex : SupremumType x x x
+
+||| The following three types are used to represent compatible types of arrays.
+
+public export
+data ArrEnd : (start : Nat) -> (end : Nat) -> (finalIndex : Nat) -> Type where
+  ArrEndA : So (start < end) -> So (finalIndex == (end `minus` start)) -> ArrEnd start end finalIndex
+  ArrEndB : So (end < start) -> So (finalIndex == (start `minus` end)) -> ArrEnd start end finalIndex
+
+public export
+data ArrSizeSupremum : (start1 : Nat) -> (end1 : Nat) ->
+                       (start2 : Nat) -> (end2 : Nat) ->
+                       (startR : Nat) -> (endR : Nat) -> Type where
+  ArrSizeSupremumConstructA : ArrEnd start1 end1 finalIndex1 ->
+                              ArrEnd start2 end2 finalIndex2 ->
+                              So (endR == (startR + (max finalIndex1 finalIndex2))) ->
+                              ArrSizeSupremum start1 end1 start2 end2 startR endR
+  ArrSizeSupremumConstructB : ArrEnd start1 end1 finalIndex1 ->
+                              ArrEnd start2 end2 finalIndex2 ->
+                              So (endR == (startR + (max finalIndex1 finalIndex2))) ->
+                              ArrSizeSupremum start1 end1 start2 end2 endR startR
+
+public export
+data ArrSupremum : (SVArray t1 start1 end1) -> (SVArray t2 start2 end2) -> (SVArray tR startR endR) -> Type where
+  ArrSupremumConstructA : SupremumType x y z ->
+                          ArrSizeSupremum start1 end1 start2 end2 startR endR ->
+                          ArrSupremum (Unpacked (Var x) start1 end1) (Unpacked (Var y) start2 end2) (Unpacked (Var z) startR endR)
+  ArrSupremumConstructB : SupremumType x y z ->
+                          ArrSizeSupremum start1 end1 start2 end2 startR endR ->
+                          AllowedInPackedArr (Var x) => AllowedInPackedArr (Var y) => AllowedInPackedArr (Var z) =>
+                          ArrSupremum (Packed (Var x) start1 end1) (Packed (Var y) start2 end2) (Packed (Var z) startR endR)
+  ArrSupremumConstructC : ArrSupremum x y z ->
+                          ArrSizeSupremum start1 end1 start2 end2 startR endR ->
+                          ArrSupremum (Unpacked (Arr x) start1 end1) (Unpacked (Arr y) start2 end2) (Unpacked (Arr z) startR endR)
+  ArrSupremumConstructD : ArrSupremum x y z ->
+                          ArrSizeSupremum start1 end1 start2 end2 startR endR ->
+                          (al1 : AllowedInPackedArr (Arr x)) => (al2 : AllowedInPackedArr (Arr y)) => (al3 : AllowedInPackedArr (Arr z)) =>
+                          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
+  SVLogicAnd : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var z)
+  SVLogicOr : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var z)
+  SVLogicImply : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var z)
+  SVLogicalEquiv : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var z)
+  SVBiteWiseAnd : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Arr z)
+  SVBiteWiseOr : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Arr z)
+  SVAddBits : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var z)
+  SVAddArrays : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Arr z)
+  SVSubBits : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var z)
+  SVSubArrays : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Arr z)
+  SVMultBits : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var z)
+  SVMultArrays : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Arr z)
+  SVDivBits : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var z)
+  SVDivArrays : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Arr z)
+  SVLessBits : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var z)
+  SVLessArrays : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Var Logic')
+  SVLessEqBits : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var z)
+  SVLessEqArrays : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Var Logic')
+  SVGreaterBits : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var z)
+  SVGreaterArrays : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Var Logic')
+  SVLogicalEqualBits : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var Logic')
+  SVLogicalEqualArrays : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Var Logic')
+  SVLogicalNotEqualBits : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var Logic')
+  SVLogicalNotEqualArrays : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Var Logic')
+  SVCaseEqualBits : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var Bit')
+  SVCaseEqualArrays : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Var Bit')
+  SVCaseNotEqualBits : SupremumType x y z => SVBinaryOperator (Var x) (Var y) (Var Bit')
+  SVCaseNotEqualArrays : ArrSupremum x y z => SVBinaryOperator (Arr x) (Arr y) (Var Bit')
+
+||| Predicate to test if the type is integral as described in the IEEE 1800-2023 standard.
+public export
+data IsIntegralType : SVType -> Type where
+  LogicIsIntegral : IsIntegralType (Var Logic')
+  BitIsIntegral : IsIntegralType (Var Bit')
+  WireIsIntegral : IsIntegralType (Var Wire')
+  UwireIsIntegral : IsIntegralType (Var Uwire')
+  IntIsIntegral : IsIntegralType (Var Int')
+  IntegerIsIntegral : IsIntegralType (Var Integer')
+  UnpackedArrysIsIntegral : IsIntegralType t -> IsIntegralType (Arr (Unpacked t s e))
+  PackedArrysIsIntegral : AllowedInPackedArr t => IsIntegralType t -> IsIntegralType (Arr (Packed t s e))
+
+public export
+data IsLogicOrBite : SVType -> Type where
+  LogicIs : IsLogicOrBite (Var Logic')
+  BitIs : IsLogicOrBite (Var Bit')
+  WireIs : IsLogicOrBite (Var Wire')
+  UwireIs : IsLogicOrBite (Var Uwire')
+
+public export
+data SVUnaryOperator : (iType : SVType) -> (oType : SVType) -> Type where
+  SVUnaryMinus : IsIntegralType iType => SVUnaryOperator iType iType
+  SVLogicalNegation : IsLogicOrBite iType => SVUnaryOperator iType iType
+  SVBitwiseNegationUnpacked : IsIntegralType iType => SVUnaryOperator (Arr $ Unpacked iType s e) (Arr $ Unpacked iType s e)
+  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
+  SVVarOrNet : (i : IndexInPorts ports)-> AtIndexInPorts i t => SVExpression t ports [i]
+  SVLogicConstant : SValue4 -> SVExpression (Var Logic') ports []
+  SVWireConstant : SValue4 -> SVExpression (Var Wire') ports []
+  SVUwireConstant : SValue4 -> SVExpression (Var Uwire') ports []
+  SVBitConstant : SValue2 -> SVExpression (Var Bit') ports []
+  SVUnpackedArrayConstant : BinaryList t (S (max s e `minus` min s e)) -> SVExpression (Arr $ Unpacked t s e) ports []
+  SVPackedArrayConstant : AllowedInPackedArr t => BinaryList t (S (max s e `minus` min s e)) -> SVExpression (Arr $ Packed t s e) ports []
+  SVIndexUnpackedArray : (i : IndexInPorts ports) -> AtIndexInPorts i (Arr $ Unpacked t s e) => (arrIndex : Nat) => LTE (min s e) arrIndex => LTE arrIndex (max s e) => SVExpression t ports [i]
+  SVIndexPackedArray : AllowedInPackedArr t => (i : IndexInPorts ports) -> AtIndexInPorts i (Arr $ Packed t s e) => (arrIndex : Nat) -> LTE (min s e) arrIndex => LTE arrIndex (max s e) => SVExpression t ports [i]
+  SVApplyBinaryOperator : {usedPortsL : _} -> {usedPortsR : _} ->
+                          SVBinaryOperator lType rType retType ->
+                          (l : SVExpression lType ports usedPortsL) -> (r : SVExpression rType ports usedPortsR) ->
+                          {default (usedPortsL `union` usedPortsR) resUsedPorts : _} -> So (resUsedPorts `setEqual` (usedPortsL `union` usedPortsR)) =>
+                          SVExpression retType ports resUsedPorts
+  SVApplyUnaryOperator : {usedPorts : _} -> SVUnaryOperator iType oType -> SVExpression iType ports usedPorts -> SVExpression oType ports usedPorts
+  -- TODO: Rework this part after the complete partial order of types is introduced.
+  SVConditionalExpression : {usedPortsCond : _} -> {cType : SVType} -> IsLogicOrBite cType =>
+                            SVExpression cType ports usedPortsCond ->
+                            {tType : SVBasic} -> {fType : SVBasic} -> {rType : SVBasic} -> SupremumType tType fType rType =>
+                            {usedPortsT : _} -> SVExpression (Var tType) ports usedPortsT ->
+                            {usedPortsF : _} -> SVExpression (Var fType) ports usedPortsF ->
+                            {default ((usedPortsCond `union` usedPortsT) `union` usedPortsF) resUsedPorts : _} -> So (resUsedPorts `setEqual` (((usedPortsCond `union` usedPortsT) `union` usedPortsF))) ->
+                            SVExpression (Var rType) ports resUsedPorts
+  SVCondtionExpressionArray : {usedPortsCond : _} -> {cType : SVType} -> IsLogicOrBite cType =>
+                              SVExpression cType ports usedPortsCond ->
+                              {t1 : _} -> {s1 : _} -> {e1 : _} -> {tType : SVArray t1 s1 e1} ->
+                              {t2 : _} -> {s2 : _} -> {e2 : _} -> {fType : SVArray t2 s2 e2} ->
+                              {t3 : _} -> {s3 : _} -> {e3 : _} -> {rType : SVArray t3 s3 e3} ->
+                              ArrSupremum tType fType rType =>
+                              {usedPortsT : _} -> SVExpression (Arr tType) ports usedPortsT ->
+                              {usedPortsF : _} -> SVExpression (Arr fType) ports usedPortsF ->
+                              {default ((usedPortsCond `union` usedPortsT) `union` usedPortsF) resUsedPorts : _} -> So (resUsedPorts `setEqual` (((usedPortsCond `union` usedPortsT) `union` usedPortsF))) ->
+                              SVExpression (Arr rType) ports resUsedPorts
+
+
+export
+genExpressions : Fuel -> (expressionType : SVType) -> (ports : PortsList) -> (usedPorts : ListOfPortsIndices ports) -> Gen MaybeEmpty (SVExpression expressionType ports usedPorts)
diff --git a/src/Test/Verilog/Expression/Derived.idr b/src/Test/Verilog/Expression/Derived.idr
new file mode 100644
index 0000000..9bec323
--- /dev/null
+++ b/src/Test/Verilog/Expression/Derived.idr
@@ -0,0 +1,11 @@
+module Test.Verilog.Expression.Derived
+
+import Deriving.DepTyCheck.Gen
+
+import public Test.Verilog.Expression
+
+%default total
+
+%logging "deptycheck" 20
+
+Test.Verilog.Expression.genExpressions = deriveGen
diff --git a/src/Test/Verilog/Module.idr b/src/Test/Verilog/Module.idr
index 1449999..acddd8d 100644
--- a/src/Test/Verilog/Module.idr
+++ b/src/Test/Verilog/Module.idr
@@ -47,6 +47,58 @@ import Test.DepTyCheck.Gen.Coverage
 public export
 data SVBasic = Logic' | Wire' | Uwire' | Int' | Integer' | Bit' | Real'
 
+public export
+DecEq SVBasic where
+  decEq Logic' Logic' = Yes Refl
+  decEq Logic' Wire' = No $ \Refl impossible
+  decEq Logic' Uwire' = No $ \Refl impossible
+  decEq Logic' Int' = No $ \Refl impossible
+  decEq Logic' Integer' = No $ \Refl impossible
+  decEq Logic' Bit' = No $ \Refl impossible
+  decEq Logic' Real' = No $ \Refl impossible
+  decEq Wire' Logic' = No $ \Refl impossible
+  decEq Wire' Wire' = Yes Refl
+  decEq Wire' Uwire' = No $ \Refl impossible
+  decEq Wire' Int' = No $ \Refl impossible
+  decEq Wire' Integer' = No $ \Refl impossible
+  decEq Wire' Bit' = No $ \Refl impossible
+  decEq Wire' Real' = No $ \Refl impossible
+  decEq Uwire' Logic' = No $ \Refl impossible
+  decEq Uwire' Wire' = No $ \Refl impossible
+  decEq Uwire' Uwire' = Yes Refl
+  decEq Uwire' Int' = No $ \Refl impossible
+  decEq Uwire' Integer' = No $ \Refl impossible
+  decEq Uwire' Bit' = No $ \Refl impossible
+  decEq Uwire' Real' = No $ \Refl impossible
+  decEq Int' Logic' = No $ \Refl impossible
+  decEq Int' Wire' = No $ \Refl impossible
+  decEq Int' Uwire' = No $ \Refl impossible
+  decEq Int' Int' = Yes Refl
+  decEq Int' Integer' = No $ \Refl impossible
+  decEq Int' Bit' = No $ \Refl impossible
+  decEq Int' Real' = No $ \Refl impossible
+  decEq Integer' Logic' = No $ \Refl impossible
+  decEq Integer' Wire' = No $ \Refl impossible
+  decEq Integer' Uwire' = No $ \Refl impossible
+  decEq Integer' Int' = No $ \Refl impossible
+  decEq Integer' Integer' = Yes Refl
+  decEq Integer' Bit' = No $ \Refl impossible
+  decEq Integer' Real' = No $ \Refl impossible
+  decEq Bit' Logic' = No $ \Refl impossible
+  decEq Bit' Wire' = No $ \Refl impossible
+  decEq Bit' Uwire' = No $ \Refl impossible
+  decEq Bit' Int' = No $ \Refl impossible
+  decEq Bit' Integer' = No $ \Refl impossible
+  decEq Bit' Bit' = Yes Refl
+  decEq Bit' Real' = No $ \Refl impossible
+  decEq Real' Logic' = No $ \Refl impossible
+  decEq Real' Wire' = No $ \Refl impossible
+  decEq Real' Uwire' = No $ \Refl impossible
+  decEq Real' Int' = No $ \Refl impossible
+  decEq Real' Integer' = No $ \Refl impossible
+  decEq Real' Bit' = No $ \Refl impossible
+  decEq Real' Real' = Yes Refl
+
 public export
 data EqSVBasic : SVBasic -> SVBasic -> Type where
   EqLogic'   : EqSVBasic Logic'   Logic'
@@ -62,7 +114,13 @@ data SVArray : SVType -> Nat -> Nat -> Type
 data AllowedInPackedArr : SVType -> Type
 
 public export
-data SVType = Arr (SVArray t s e) | Var SVBasic
+data SVType : Type where
+  Arr : {t : _} -> {s : _} -> {e : _} -> (SVArray t s e) -> SVType
+  Var : SVBasic -> SVType
+
+public export
+Injective Var where
+  injective Refl = Refl
 
 ||| The main difference between an unpacked array and a packed array is that
 ||| an unpacked array is not guaranteed to be represented as a contiguous set of bits
@@ -93,6 +151,49 @@ data AllowedInPackedArr : SVType -> Type where
   -- R : AllowedInPackedArr Reg' -- Uncomment when Reg is added to the SVBasic
   P : AllowedInPackedArr (Arr (Packed {} @{_}))
 
+public export
+DecEq (AllowedInPackedArr t)
+
+public export
+DecEq (SVArray t start end)
+
+public export
+DecEq SVType where
+  decEq (Arr (Unpacked t s e)) (Arr (Unpacked t' s' e')) with (decEq t t')
+    decEq (Arr (Unpacked t s e)) (Arr (Unpacked t' s' e')) | No p = No $ \Refl => p Refl
+    decEq (Arr (Unpacked t s e)) (Arr (Unpacked t s' e')) | Yes Refl with (decEq s s')
+      decEq (Arr (Unpacked t s e)) (Arr (Unpacked t s' e')) | Yes Refl | No p = No $ \Refl => p Refl
+      decEq (Arr (Unpacked t s e)) (Arr (Unpacked t s e')) | Yes Refl | Yes Refl with (decEq e e')
+        decEq (Arr (Unpacked t s e)) (Arr (Unpacked t s e')) | Yes Refl | Yes Refl | No p = No $ \Refl => p Refl
+        decEq (Arr (Unpacked t s e)) (Arr (Unpacked t s e)) | Yes Refl | Yes Refl | Yes Refl = Yes Refl
+  decEq (Arr (Unpacked t s e)) (Arr (Packed t' s' e' @{k'})) = No $ \Refl impossible
+  decEq (Arr (Packed t s e @{k})) (Arr (Unpacked t' s' e')) = No $ \Refl impossible
+  decEq (Arr (Packed t s e @{k})) (Arr (Packed t' s' e' @{k'})) with (decEq t t')
+    decEq (Arr (Packed t s e @{k})) (Arr (Packed t' s' e' @{k'})) | No p = No $ \Refl => p Refl
+    decEq (Arr (Packed t s e @{k})) (Arr (Packed t s' e' @{k'})) | Yes Refl with (decEq s s')
+      decEq (Arr (Packed t s e @{k})) (Arr (Packed t s' e' @{k'})) | Yes Refl | No p = No $ \Refl => p Refl
+      decEq (Arr (Packed t s e @{k})) (Arr (Packed t s e' @{k'})) | Yes Refl | Yes Refl with (decEq e e')
+        decEq (Arr (Packed t s e @{k})) (Arr (Packed t s e' @{k'})) | Yes Refl | Yes Refl | No p = No $ \Refl => p Refl
+        decEq (Arr (Packed t s e @{k})) (Arr (Packed t s e @{k'})) | Yes Refl | Yes Refl | Yes Refl with (decEq k k')
+          decEq (Arr (Packed t s e @{k})) (Arr (Packed t s e @{k'})) | Yes Refl | Yes Refl | Yes Refl | No p = No $ \Refl => p Refl
+          decEq (Arr (Packed t s e @{k})) (Arr (Packed t s e @{k})) | Yes Refl | Yes Refl | Yes Refl | Yes Refl = Yes Refl
+  decEq (Arr x) (Var y) = No $ \Refl impossible
+  decEq (Var x) (Arr y) = No $ \Refl impossible
+  decEq (Var x) (Var y) = decEqCong (decEq x y)
+
+DecEq (AllowedInPackedArr t) where
+  decEq B B = Yes Refl
+  decEq L L = Yes Refl
+  decEq P P = Yes Refl
+
+DecEq (SVArray t start end) where
+  decEq (Unpacked t start end) (Unpacked t start end) = Yes Refl
+  decEq (Unpacked _ _ _) (Packed _ _ _) = No $ \Refl impossible
+  decEq (Packed t start end @{k}) (Unpacked t start end) = No $ \Refl impossible
+  decEq (Packed t start end @{k}) (Packed t start end @{k'}) with (decEq k k')
+    decEq (Packed t start end @{k}) (Packed t start end @{k'}) | No p = No $ \Refl => p Refl
+    decEq (Packed t start end @{k}) (Packed t start end @{k})  | Yes Refl = Yes Refl
+
 namespace Ports
 
   public export
@@ -122,13 +223,112 @@ namespace Ports
   portsListAppendLen []        ys = Refl
   portsListAppendLen (_ :: xs) ys = rewrite portsListAppendLen xs ys in Refl
 
-  -- Maybe, specialised type `IndexIn : PortsList -> Type` isomorphic to `Fin (length xs)`
-
   public export
   typeOf : (xs : PortsList) -> Fin (length xs) -> SVType
   typeOf (p::_ ) FZ     = p
   typeOf (_::ps) (FS i) = typeOf ps i
 
+namespace IndexInPorts
+
+  public export
+  data IndexInPorts : PortsList -> Type where
+    Here : {x : SVType} -> {xs : PortsList} -> IndexInPorts (x :: xs)
+    There : {x : SVType} -> {xs : PortsList} -> IndexInPorts xs -> IndexInPorts (x :: xs)
+
+  public export
+  DecEq (IndexInPorts ports) where
+    decEq Here Here = Yes Refl
+    decEq (Here) (There _) = No $ \Refl impossible
+    decEq (There _) Here = No $ \Refl impossible
+    decEq (There i) (There i') with (decEq i i')
+      decEq (There i) (There i') | No p = No $ \Refl => p Refl
+      decEq (There i) (There i) | Yes Refl = Yes Refl
+
+  public export
+  Eq (IndexInPorts ports) where
+    (==) x y with (decEq x y)
+      _ | Yes _ = True
+      _ | No _  = False
+
+  public export
+  data ListOfPortsIndices : PortsList -> Type where
+    Nil  : {ports : _} -> ListOfPortsIndices ports
+    (::) : {ports : _} -> IndexInPorts ports -> ListOfPortsIndices ports -> ListOfPortsIndices ports
+
+  public export
+  DecEq (ListOfPortsIndices ports) where
+    decEq [] [] = Yes Refl
+    decEq (a :: as) [] = No $ \Refl impossible
+    decEq [] (b :: bs) = No $ \Refl impossible
+    decEq (a :: as) (b :: bs) with (decEq a b)
+      decEq (a :: as) (b :: bs) | No p = No $ \Refl => p Refl
+      decEq (a :: as) (a :: bs) | Yes Refl with (decEq as bs)
+        decEq (a :: as) (a :: bs) | Yes Refl | No p = No $ \Refl => p Refl
+        decEq (a :: as) (a :: as) | Yes Refl | Yes Refl = Yes Refl
+
+  public export
+  Eq (ListOfPortsIndices ports) where
+    (==) x y with (decEq x y)
+      _ | Yes _ = True
+      _ | No _  = False
+
+  public export
+  (++) : ListOfPortsIndices ports -> ListOfPortsIndices ports -> ListOfPortsIndices ports
+  (++) [] bs = bs
+  (++) (a :: as) bs = a :: (as ++ bs)
+
+  public export
+  (.toList) : ListOfPortsIndices ports -> List (IndexInPorts ports)
+  (.toList) []        = []
+  (.toList) (x :: xs) = x :: xs.toList
+
+  public export
+  (.fromList) : {ports : _} -> List (IndexInPorts ports) -> ListOfPortsIndices ports
+  (.fromList) []        = []
+  (.fromList) (x :: xs) = x :: xs.fromList
+
+  public export
+    data AtIndexInPorts : {ports : PortsList} -> (i : IndexInPorts ports) -> (typeOfPort : SVType) -> Type where
+      [search ports i]
+      HereAt : {typeOfPort : SVType} -> {xs : PortsList}
+            -> AtIndexInPorts {ports = typeOfPort :: xs} Here typeOfPort
+
+      ThereAt : {typeOfPort : SVType} -> {x : SVType} -> {xs : PortsList} -> {i : IndexInPorts xs}
+             -> (ati : AtIndexInPorts {ports = xs} i typeOfPort) -> AtIndexInPorts {ports = x :: xs} (There i) typeOfPort
+
+  public export
+  appendIfNew : {ports: _} -> ListOfPortsIndices ports -> (i : IndexInPorts ports) -> ListOfPortsIndices ports
+  appendIfNew [] i = [i]
+  appendIfNew (a :: as) i with (a == i)
+    _ | True = a :: as
+    _ | False = a :: appendIfNew as i
+
+  public export
+  union : {ports : _} -> ListOfPortsIndices ports -> ListOfPortsIndices ports -> ListOfPortsIndices ports
+  union x y = (x.toList `union` y.toList).fromList
+
+  public export
+  setEqual : ListOfPortsIndices ports -> ListOfPortsIndices ports -> Bool
+  setEqual x y = ((x.toList `intersect` y.toList) == x.toList) && ((y.toList `intersect` x.toList) == y.toList)
+
+  public export
+  elem : IndexInPorts ports -> ListOfPortsIndices ports -> Bool
+  elem i [] = False
+  elem i (x :: xs) with (decEq i x)
+    _ | Yes _ = True
+    _ | No _  = elem i xs
+
+  public export
+  data IsElemOf : IndexInPorts ports -> ListOfPortsIndices ports -> Type where
+    InHead : {x : IndexInPorts ports} -> IsElemOf x (x :: xs)
+    InTail : IsElemOf y xs -> IsElemOf y (x :: xs)
+
+  public export
+  shortenIndexPorts : ListOfPortsIndices (p :: ports) -> ListOfPortsIndices ports
+  shortenIndexPorts []        = []
+  shortenIndexPorts (Here :: xs) = shortenIndexPorts xs
+  shortenIndexPorts ((There x) :: xs) = x :: (shortenIndexPorts xs)
+
 namespace ModuleSig
 
   public export
@@ -263,7 +463,7 @@ namespace ConnsList
     ZS  : NotEqFin FZ (FS i)
     SZ  : NotEqFin (FS i) FZ
     Rec : NotEqFin x y -> NotEqFin (FS x) (FS y)
-  
+
   public export
   data Connections : (srcs, sinks : PortsList) -> (isUnique : Bool) -> Type
 
@@ -276,7 +476,7 @@ namespace ConnsList
   data Connections : (srcs, sinks : PortsList) -> (isUnique : Bool) -> Type where
     Empty : Connections srcs [] u
     Cons  : (sfs : SourceForSink srcs sink) -> (rest : Connections srcs sinks u) -> NoSourceConns sfs rest -> Connections srcs (sink :: sinks) u
-  
+
   ||| List of source indexes
   public export
   consToFins : Connections srcs sinks u -> FinsList (srcs.length)
diff --git a/src/Test/Verilog/Module/Derived.idr b/src/Test/Verilog/Module/Derived.idr
index b3adf38..793c882 100644
--- a/src/Test/Verilog/Module/Derived.idr
+++ b/src/Test/Verilog/Module/Derived.idr
@@ -2,7 +2,7 @@ module Test.Verilog.Module.Derived
 
 import Deriving.DepTyCheck.Gen
 
-import public Test.Verilog.Module
+import public Test.Verilog.ProceduralBlock
 
 %default total
 
@@ -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
diff --git a/src/Test/Verilog/ProceduralBlock.idr b/src/Test/Verilog/ProceduralBlock.idr
new file mode 100644
index 0000000..853b7c2
--- /dev/null
+++ b/src/Test/Verilog/ProceduralBlock.idr
@@ -0,0 +1,224 @@
+module Test.Verilog.ProceduralBlock
+
+import Data.Fuel
+import Data.Vect
+
+import public Data.So
+
+import public Test.Verilog.Module
+import public Test.Verilog.Expression
+
+import Test.DepTyCheck.Gen
+import Test.DepTyCheck.Gen.Coverage
+
+%default total
+
+public export
+data MaybeSVType : Type where
+  Nothing : MaybeSVType
+  Just : SVType -> MaybeSVType
+
+
+||| Procudaral blocks are described in the section 12 of the IEEE 1800-2023.
+||| According to the subsectionsection 12.3, the statement item is one of the following:
+||| - blocking assignment
+||| - nonblocking_assignment
+||| - procedural_continuous_assignment
+||| - case_statement
+||| - conditional_statement
+||| - subroutine_call_statement
+||| - disable_statement
+||| - event_trigger
+||| - loop_statement
+||| - jump_statement
+||| - par_block
+||| - procedural_timing_control_statement
+||| - seq_block
+||| - wait_statement
+||| - procedural_assertion_statement
+||| - clocking_drive ;
+||| - randsequence_statement
+||| - randcase_statement
+||| - expect_property_statement
+public export
+data ProceduralBlock : (ports : PortsList) ->
+                       (isCombinatorial : Bool) ->
+                       (procAssignedPorts : ListOfPortsIndices ports) ->
+                       (contAssignedPorts : ListOfPortsIndices ports) ->
+                       (retTy : MaybeSVType) -> Type
+
+public export
+data IsAssignableTo : SVType -> SVType -> Type where
+  IsAssignableToA : SupremumType x y y -> (Var x) `IsAssignableTo` (Var y)
+  IsAssignambleToB : ArrSupremum x y y -> (Arr x) `IsAssignableTo` (Arr y)
+
+public export
+data NotInList : (i : IndexInPorts ports) -> (l : ListOfPortsIndices ports) -> Type where
+  NotInListA : So (not (i `elem` ports)) -> NotInList i ports
+
+public export
+data IsSubblockRetCompatible : MaybeSVType -> MaybeSVType -> Type where
+  NothingIsAlwaysCompatible : IsSubblockRetCompatible Nothing x
+  ReflexiveComaptibility : IsSubblockRetCompatible (Just x) (Just x)
+
+namespace CombinatorialElseIf
+
+  public export
+  data CombinatorialElseIfCase : (procAssignedPorts : ListOfPortsIndices ports) ->
+                                 (contAssignedPorts : ListOfPortsIndices ports) ->
+                                 (retTy : MaybeSVType) -> Type where
+    CombinatorialCaseConstructor : SVExpression caseExprType ports usedPorts ->
+                                   IsLogicOrBite caseExprType =>
+                                   (caseBlock : ProceduralBlock ports True procAssignedPorts contAssignedPorts caseTy) ->
+                                   caseTy `IsSubblockRetCompatible` retTy =>
+                                   CombinatorialElseIfCase procAssignedPorts contAssignedPorts retTy
+
+  public export
+  data CombinatorialElseIfCaseList : (procAssignedPorts : ListOfPortsIndices ports) ->
+                                     (contAssignedPorts : ListOfPortsIndices ports) ->
+                                     (retTy : MaybeSVType) -> Type where
+    Nil : CombinatorialElseIfCaseList procAssignedPorts contAssignedPorts retTy
+    (::) : CombinatorialElseIfCase procAssignedPorts contAssignedPorts retTy ->
+           CombinatorialElseIfCaseList procAssignedPorts contAssignedPorts retTy ->
+           CombinatorialElseIfCaseList procAssignedPorts contAssignedPorts retTy
+
+namespace NonCombinatorialElseIf
+
+  public export
+  data NonCombinatorialElseIfCase : (ports : PortsList) -> (retTy : MaybeSVType) -> Type where
+    NonCombinatorialCaseConstructor : {ports : _} -> {usedPorts : _} -> {procAssignedPorts : _} -> {contAssignedPorts : _} ->
+                                      SVExpression caseExprType ports usedPorts ->
+                                      IsLogicOrBite caseExprType =>
+                                      (caseBlock : ProceduralBlock ports _ procAssignedPorts contAssignedPorts caseTy) ->
+                                      caseTy `IsSubblockRetCompatible` retTy =>
+                                      NonCombinatorialElseIfCase ports retTy
+
+  public export
+   data NonCombinatorialElseIfCaseList : (ports : PortsList) -> (retTy : MaybeSVType) -> Type where
+    Nil : NonCombinatorialElseIfCaseList ports retTy
+    (::) : {ports : _} ->
+           NonCombinatorialElseIfCase ports retTy ->
+           NonCombinatorialElseIfCaseList ports retTy ->
+           NonCombinatorialElseIfCaseList ports retTy
+
+  public export
+  getAllProcAssignments : {ports : _} -> NonCombinatorialElseIfCaseList ports retTy -> ListOfPortsIndices ports
+  getAllProcAssignments Nil = []
+  getAllProcAssignments ((NonCombinatorialCaseConstructor {procAssignedPorts} _ _) :: xs) = procAssignedPorts `union` (getAllProcAssignments xs)
+
+  public export
+  gettAllContAssignments : {ports : _} -> NonCombinatorialElseIfCaseList ports retTy -> ListOfPortsIndices ports
+  gettAllContAssignments Nil = []
+  gettAllContAssignments ((NonCombinatorialCaseConstructor {contAssignedPorts} _ _) :: xs) = contAssignedPorts `union` (gettAllContAssignments xs)
+
+
+public export
+data ProceduralBlock : (ports : PortsList) ->
+                       (isCombinatorial : Bool) ->
+                       (procAssignedPorts : ListOfPortsIndices ports) ->
+                       (contAssignedPorts : ListOfPortsIndices ports) ->
+                       (retTy : MaybeSVType) -> Type where
+
+  BlockingAssignment : (i : IndexInPorts ports) -> (expr : SVExpression expType ports usedPorts) ->
+                       AtIndexInPorts i portType => expTpype `IsAssignableTo` portType =>
+                       (continuation : ProceduralBlock ports isCombinatorial procAssignedPorts contAssignedPorts retTy) ->
+                       NotInList i contAssignedPorts =>
+                       ProceduralBlock ports isCombinatorial (i :: procAssignedPorts) contAssignedPorts retTy
+
+  ContinuousAssignment : (i : IndexInPorts ports) -> (expr : SVExpression expType ports usedPorts) ->
+                         AtIndexInPorts i portType => expTpype `IsAssignableTo` portType =>
+                         (continuation : ProceduralBlock ports isCombinatorial procAssignedPorts contAssignedPorts retTy) ->
+                         NotInList i procAssignedPorts =>
+                         NotInList i contAssignedPorts =>
+                         ProceduralBlock ports isCombinatorial procAssignedPorts (i :: contAssignedPorts) retTy
+
+  CombinatorialIf : {finalRetType : MaybeSVType} ->
+                    IsLogicOrBite baseExprType =>
+                    {baseProcAssignedPorts :  _} -> {baseContAssignedPorts :  _} ->
+                    (baseExpr : SVExpression baseExprType ports usedPorts) ->
+                    retTy `IsSubblockRetCompatible` finalRetType =>
+                    (baseBlock : ProceduralBlock ports True baseProcAssignedPorts baseContAssignedPorts retTy) ->
+                    retTy' `IsSubblockRetCompatible` finalRetType =>
+                    (elseBlock : ProceduralBlock ports True baseProcAssignedPorts baseContAssignedPorts retTy') ->
+                    (additinalCases : CombinatorialElseIfCaseList baseProcAssignedPorts baseContAssignedPorts finalRetType) ->
+                    {continuationProcAssignedPorts : _} -> {continuationContAssignedPorts : _} ->
+                    (continuation : ProceduralBlock ports _ continuationProcAssignedPorts continuationContAssignedPorts finalRetType) ->
+                    {default (baseProcAssignedPorts `union` continuationProcAssignedPorts) finalProcAssignedPorts : ListOfPortsIndices ports} ->
+                    So (finalProcAssignedPorts `setEqual` (baseProcAssignedPorts `union` continuationProcAssignedPorts)) =>
+                    {default (baseContAssignedPorts `union` continuationContAssignedPorts) finalContAssignedPorts : ListOfPortsIndices ports} ->
+                    So (finalContAssignedPorts `setEqual` (baseContAssignedPorts `union` continuationContAssignedPorts)) =>
+                    ProceduralBlock ports _ finalProcAssignedPorts finalContAssignedPorts finalRetType
+
+  NonCombinatorialIf : {finalRetType : MaybeSVType} ->
+                       IsLogicOrBite baseExprType =>
+                       {baseProcAssignedPorts :  _} -> {baseContAssignedPorts :  _} ->
+                       (baseExpr : SVExpression baseExprType ports usedPorts) ->
+                       retTy `IsSubblockRetCompatible` finalRetType =>
+                       (baseBlock : ProceduralBlock ports _ baseProcAssignedPorts baseContAssignedPorts retTy) ->
+                       {elseProcAssignedPorts : _} -> {elseContAssignedPorts : _} ->
+                       (elseBlock : ProceduralBlock ports _ elseProcAssignedPorts elseContAssignedPorts retTy') ->
+                       retTy' `IsSubblockRetCompatible` finalRetType =>
+                       (additinalCases : NonCombinatorialElseIfCaseList ports finalRetType) ->
+                       {continuationProcAssignedPorts : _} -> {continuationContAssignedPorts : _} ->
+                       (continuation : ProceduralBlock ports _ continuationProcAssignedPorts continuationContAssignedPorts finalRetType) ->
+                       {default (((baseProcAssignedPorts `union` elseProcAssignedPorts) `union` (getAllProcAssignments additinalCases)) `union` continuationProcAssignedPorts) finalProcAssignedPorts : ListOfPortsIndices ports} ->
+                       So (finalProcAssignedPorts `setEqual` (((baseProcAssignedPorts `union` elseProcAssignedPorts) `union` (getAllProcAssignments additinalCases)) `union` continuationProcAssignedPorts)) =>
+                       {default (((baseContAssignedPorts `union` elseContAssignedPorts) `union` (gettAllContAssignments additinalCases)) `union` continuationContAssignedPorts) finalContAssignedPorts : ListOfPortsIndices ports} ->
+                       So (finalContAssignedPorts `setEqual` (((baseContAssignedPorts `union` elseContAssignedPorts) `union` (gettAllContAssignments additinalCases)) `union` continuationContAssignedPorts)) =>
+                       ProceduralBlock ports False finalProcAssignedPorts finalContAssignedPorts finalRetType
+
+  NonCombinatorialIfNoElse : {finalRetType : MaybeSVType} ->
+                             IsLogicOrBite baseExprType =>
+                             {baseProcAssignedPorts :  _} -> {baseContAssignedPorts :  _} ->
+                             (baseExpr : SVExpression baseExprType ports usedPorts) ->
+                             retTy `IsSubblockRetCompatible` finalRetType =>
+                             (baseBlock : ProceduralBlock ports _ baseProcAssignedPorts baseContAssignedPorts retTy) ->
+                             (additinalCases : NonCombinatorialElseIfCaseList ports finalRetType) ->
+                             {continuationProcAssignedPorts : _} -> {continuationContAssignedPorts : _} ->
+                             (continuation : ProceduralBlock ports _ continuationProcAssignedPorts continuationContAssignedPorts finalRetType) ->
+                             {default ((baseProcAssignedPorts `union` (getAllProcAssignments additinalCases)) `union` continuationProcAssignedPorts) finalProcAssignedPorts : ListOfPortsIndices ports} ->
+                             So (finalProcAssignedPorts `setEqual` ((baseProcAssignedPorts `union` (getAllProcAssignments additinalCases)) `union` continuationProcAssignedPorts)) =>
+                             {default ((baseContAssignedPorts `union` (gettAllContAssignments additinalCases)) `union` continuationContAssignedPorts) finalContAssignedPorts : ListOfPortsIndices ports} ->
+                             So (finalContAssignedPorts `setEqual` ((baseContAssignedPorts `union` (gettAllContAssignments additinalCases)) `union` continuationContAssignedPorts)) =>
+                             ProceduralBlock ports False finalProcAssignedPorts finalContAssignedPorts finalRetType
+
+  WhileBlock : IsLogicOrBite exprType =>
+               (expr : SVExpression exprType ports usedPorts) ->
+               {innerProcAssignedPorts : _} ->
+               (innerBlock : ProceduralBlock ports isCombinatorial innerProcAssignedPorts [] Nothing) ->
+               {continuationProcAssignedPorts : _} -> {continuationContAssignedPorts : _} ->
+               (continuation : ProceduralBlock ports isCombinatorial continuationProcAssignedPorts continuationContAssignedPorts Nothing) ->
+               {default (innerProcAssignedPorts `union` continuationProcAssignedPorts) finalProcAssignedPorts : ListOfPortsIndices ports} ->
+               So (finalProcAssignedPorts `setEqual` (innerProcAssignedPorts `union` continuationProcAssignedPorts)) =>
+               ProceduralBlock ports isCombinatorial finalProcAssignedPorts continuationContAssignedPorts retTy
+
+  ForBlock : {innerExpressionType : _} ->
+             (innerAssignment : SVExpression innerExpressionType ports usedPorts) ->
+             {0 usedPorts' : ListOfPortsIndices (innerExpressionType :: ports)} ->
+             Here `IsElemOf` usedPorts' =>
+             (conditionalExpression : SVExpression conditionalExpressionType (innerExpressionType :: ports) usedPorts') ->
+             IsLogicOrBite conditionalExpressionType =>
+             {0 usedPorts'' : ListOfPortsIndices (innerExpressionType :: ports)} ->
+             (stepExpression : SVExpression stepExpressionType (innerExpressionType :: ports) usedPorts'') ->
+             {innerProcAssignedPorts : ListOfPortsIndices (innerExpressionType :: ports)} ->
+             (innerBlock : ProceduralBlock (innerExpressionType :: ports) isCombinatorial innerProcAssignedPorts [] Nothing) ->
+             {continuationProcAssignedPorts : ListOfPortsIndices ports} ->
+             (continuation : ProceduralBlock ports isCombinatorial continuationProcAssignedPorts continuationContAssignedPorts retTy) ->
+             {default ((shortenIndexPorts innerProcAssignedPorts) `union` continuationProcAssignedPorts) finalProcAssignedPorts : ListOfPortsIndices ports} ->
+             So (finalProcAssignedPorts `setEqual` ((shortenIndexPorts innerProcAssignedPorts) `union` continuationProcAssignedPorts)) =>
+             ProceduralBlock ports isCombinatorial finalProcAssignedPorts continuationContAssignedPorts retTy
+
+  Return : (exprWithPorts : (usedPorts : _ ** SVExpression expType ports usedPorts)) ->
+           expType `IsAssignableTo` retTy =>
+           ProceduralBlock ports isCombinatorial [] [] (Just retTy)
+
+  End : ProceduralBlock ports isCombinatorial [] [] Nothing
+
+export
+genProceduralBlock : Fuel ->
+                     (ports : PortsList) ->(isCombinatorial : Bool) ->
+                     (procAssignedPorts : ListOfPortsIndices ports) ->
+                     (contAssignedPorts : ListOfPortsIndices ports) ->
+                     (retTy : MaybeSVType) ->
+                     (Fuel -> (expressionType : SVType) -> (ports : PortsList) -> (usedPorts : ListOfPortsIndices ports) -> Gen MaybeEmpty (SVExpression expressionType ports usedPorts)) =>
+                     Gen MaybeEmpty (ProceduralBlock ports isCombinatorial procAssignedPorts contAssignedPorts retTy)
diff --git a/src/Test/Verilog/ProceduralBlock/Derived.idr b/src/Test/Verilog/ProceduralBlock/Derived.idr
new file mode 100644
index 0000000..6dec89c
--- /dev/null
+++ b/src/Test/Verilog/ProceduralBlock/Derived.idr
@@ -0,0 +1,9 @@
+module Test.Verilog.ProceduralBlock.Derived
+
+import Deriving.DepTyCheck.Gen
+
+import public Test.Verilog.Module
+
+%default total
+
+%logging "deptycheck" 20
diff --git a/verilog-model.ipkg b/verilog-model.ipkg
index 76e0d6c..c9e5354 100644
--- a/verilog-model.ipkg
+++ b/verilog-model.ipkg
@@ -32,3 +32,7 @@ modules = Test.Verilog.Module
         , Test.Verilog.Assign.Derived
         , Test.Verilog.Literal.Derived
         , Test.Verilog.Pretty
+        , Test.Verilog.Expression
+        , Test.Verilog.Expression.Derived
+        , Test.Verilog.ProceduralBlock
+        , Test.Verilog.ProceduralBlock.Derived