Skip to content

Introduce shape-centered representation of the arrays #161

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

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

Introduce shape-centered representation of the arrays #161

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 19 additions & 19 deletions src/Test/Verilog/Connections.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,11 +87,11 @@ totalOutputs = length . allOutputs

public export
basicIntegral : SVType -> Bool
basicIntegral (RVar x) = False
basicIntegral (AVar x) = True
basicIntegral (VVar x) = True
basicIntegral (PackedArr t _ _) = True
basicIntegral (UnpackedArr x _ _) = basicIntegral x
basicIntegral (RVar x) = False
basicIntegral (AVar x) = True
basicIntegral (VVar x) = True
basicIntegral (PackedArr t _) = True
basicIntegral (UnpackedArr x _) = basicIntegral x

||| 6.22.2 Equivalent types
||| c) Packed arrays, packed structures, packed unions, and built-in integral types are equivalent if they
Expand All @@ -115,7 +115,8 @@ data EquivalentSVT : SVType -> SVType -> Type where
public export
data EqSuperBasic : SVType -> SVType -> Type where
VV : VarOrPacked t -> VarOrPacked t' -> EquivalentSVT t t' -> EqSuperBasic t t'
UU : EqSuperBasic t t' -> EqSuperBasic (UnpackedArr t s e) (UnpackedArr t' s' e')
UU : EqSuperBasic t t' ->
EqSuperBasic (UnpackedArr t {p} shape) (UnpackedArr t' {p = p'} shape')

||| Checks if two unpacked arrays have the same size.
|||
Expand All @@ -128,9 +129,8 @@ data EqSuperBasic : SVType -> SVType -> Type where
||| endmodule: b
public export
data EqUnpackedArrSig : SVType -> SVType -> Type where
Other : VarOrPacked t -> VarOrPacked t' -> EqUnpackedArrSig t t'
EqUArr : EqUnpackedArrSig t t' -> So ((max s e + min s' e') == (max s' e' + min s e)) ->
EqUnpackedArrSig (UnpackedArr t s e) (UnpackedArr t' s' e')
EqUArr : EqUnpackedArrSig t t' -> So (shape `isDimensionCompatibleWith` shape') ->
EqUnpackedArrSig (UnpackedArr t {p} shape) (UnpackedArr t' {p = p'} shape')

public export
data CanConnect : SVType -> SVType -> Type where
Expand Down Expand Up @@ -211,7 +211,7 @@ isMD (Net Wor' t) = True
isMD _ = False

||| 10.3.2 The continuous assignment statement
||| Variables can only be driven by one continuous assignment or by one primitive output or module output.
||| Variables can only be driven by one continuous assignment or by one primitive output or module output.
||| IEEE 1800-2023
public export
data SingleDriven : SVObject -> Type where
Expand All @@ -220,7 +220,7 @@ data SingleDriven : SVObject -> Type where

public export
isSD : SVObject -> Bool
isSD (Var st) = True
isSD (Var st) = True
isSD (Net Uwire' st) = True
isSD _ = False

Expand Down Expand Up @@ -267,7 +267,7 @@ namespace MultiConnection
findUnpNet (s :: sv) = if isUnpacked s && isMD s then Just s else findUnpNet sv

public export
resolveConnType : {ms : _} -> {m : _} -> {subMs : _} ->
resolveConnType : {ms : _} -> {m : _} -> {subMs : _} ->
(ssk : FinsList $ subSnks' ms m subMs) -> (ssc : FinsList $ subSrcs' ms m subMs) -> SVObject
resolveConnType ssk ssc = let allSubPorts = types (subSnks ms m subMs) ssk ++ types (subSrcs ms m subMs) ssc in
mOrElse (findUnpNet allSubPorts) $ mOrElse (mtype allSubPorts) defaultNetType
Expand Down Expand Up @@ -352,10 +352,10 @@ ultraSuperReplace SSC = superReplaceSC

public export
typeOfPort : (ms : ModuleSigsList) -> (m : ModuleSig) -> (subMs : FinsList ms.length) -> FillMode ms m subMs n -> Fin n -> SVObject
typeOfPort ms m subMs TSK = typeOf (topSnks m)
typeOfPort ms m subMs TSK = typeOf (topSnks m)
typeOfPort ms m subMs SSK = typeOf (subSnks ms m subMs)
typeOfPort ms m subMs TSC = typeOf (topSrcs m)
typeOfPort ms m subMs SSC = typeOf (subSrcs ms m subMs)
typeOfPort ms m subMs TSC = typeOf (topSrcs m)
typeOfPort ms m subMs SSC = typeOf (subSrcs ms m subMs)

public export
noSource : MultiConnection ms m subMs -> Bool
Expand All @@ -378,7 +378,7 @@ data FitAny : {ms : ModuleSigsList} -> {m : ModuleSig} -> {subMs : FinsList ms.l
ExistingAny : (f : Fin $ length rest) ->
(cap : CanAddPort {ms} {m} {subMs} mode $ index rest f) ->
(jmc : JustMC (ultraSuperReplace {ms} {m} {subMs} mode i $ index rest f) newMC) ->
(cc : CanConnect (valueOf $ typeOf $ index rest f) (valueOf $ typeOfPort ms m subMs mode i)) ->
(cc : CanConnect (valueOf $ typeOf $ index rest f) (valueOf $ typeOfPort ms m subMs mode i)) ->
FitAny {ms} {m} {subMs} rest i mode $ replaceAt rest f newMC

public export
Expand All @@ -398,7 +398,7 @@ data FillAny : {ms : ModuleSigsList} -> {m : ModuleSig} -> {subMs : FinsList ms.
(pre : MultiConnectionsList ms m subMs) -> {n : _} -> (i : Nat) ->
FillMode ms m subMs n -> (aft : MultiConnectionsList ms m subMs) -> Type where
FANil : FillAny pre Z mode pre
FACons : {jf : JustFin (natToFin' i n) f} -> (fit : FitAny {ms} {m} {subMs} {n} mid f mode aft) ->
FACons : {jf : JustFin (natToFin' i n) f} -> (fit : FitAny {ms} {m} {subMs} {n} mid f mode aft) ->
(rest : FillAny {ms} {m} {subMs} pre {n} i mode mid) ->
FillAny {ms} {m} {subMs} pre {n} (S i) mode aft

Expand Down Expand Up @@ -434,7 +434,7 @@ genJF : Fuel -> {n : _} -> (mf : MFin n) -> Gen MaybeEmpty (f : Fin n ** JustFin

export
genFillAny : Fuel -> {ms : ModuleSigsList} -> {m : ModuleSig} -> {subMs : FinsList ms.length} ->
(pre : MultiConnectionsList ms m subMs) -> {n : _} -> (i : Nat) -> (mode : FillMode ms m subMs n) ->
(pre : MultiConnectionsList ms m subMs) -> {n : _} -> (i : Nat) -> (mode : FillMode ms m subMs n) ->
Gen MaybeEmpty (aft : MultiConnectionsList ms m subMs ** FillAny {ms} {m} {subMs} {n} pre i mode aft)
genFillAny x pre Z mode = pure (pre ** FANil)
genFillAny x pre (S i) mode = do
Expand All @@ -446,6 +446,6 @@ genFillAny x pre (S i) mode = do
export
genModules : Fuel -> (ms : ModuleSigsList) ->
(Fuel -> {ms' : ModuleSigsList} -> {m' : ModuleSig} -> {subMs' : FinsList ms'.length} ->
(pre' : MultiConnectionsList ms' m' subMs') -> {n' : _} -> (i' : Nat) -> (mode' : FillMode ms' m' subMs' n') ->
(pre' : MultiConnectionsList ms' m' subMs') -> {n' : _} -> (i' : Nat) -> (mode' : FillMode ms' m' subMs' n') ->
Gen MaybeEmpty (aft' : MultiConnectionsList ms' m' subMs' ** FillAny {ms=ms'} {m=m'} {subMs=subMs'} {n=n'} pre' i' mode' aft')) =>
Gen MaybeEmpty $ Modules ms
18 changes: 11 additions & 7 deletions src/Test/Verilog/Literal.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,22 +30,26 @@ namespace BinaryList
namespace TypeLiteralVect

public export
data TypeLiteral : SVType -> Type
data TypeLiteral : SVType -> Type

public export
data TypeLiteralVect : Nat -> SVType-> Type where
Nil : TypeLiteralVect 0 t
(::) : TypeLiteral t -> TypeLiteralVect n t -> TypeLiteralVect (S n) t

export
toList : TypeLiteralVect l t -> List $ TypeLiteral t
toList [] = []
toList (x::xs) = x :: toList xs

public export
data TypeLiteral : SVType -> Type where
RL : BinaryList S4 -> TypeLiteral $ RVar t
AL : BinaryList (states t) -> TypeLiteral $ AVar t
VL : BinaryList (states t) -> TypeLiteral $ VVar t
PAL : {t : SVType} -> (p : PABasic t) => TypeLiteralVect (S $ max s e `minus` min s e) t -> TypeLiteral $ PackedArr t s e
UAL : TypeLiteralVect (S $ max s e `minus` min s e) t -> TypeLiteral $ UnpackedArr t s e
RL : BinaryList S4 -> TypeLiteral $ RVar t
AL : BinaryList (states t) -> TypeLiteral $ AVar t
VL : BinaryList (states t) -> TypeLiteral $ VVar t
PALF : (p : PABasic t) => TypeLiteralVect (S $ max s e `minus` min s e) t -> TypeLiteral $ PackedArr t (One $ MkPair s e)
PALM : (p : PABasic t) => TypeLiteralVect (S $ max s e `minus` min s e) (PackedArr t shape) ->
TypeLiteral $ PackedArr t (MkPair s e `More` shape)
UALF : (p : VarOrPacked t) => TypeLiteralVect (S $ max s e `minus` min s e) t -> TypeLiteral $ UnpackedArr t (One $ MkPair s e)
UALM : {shape : ArrayShape} -> (p : VarOrPacked t) => TypeLiteralVect (S $ max s e `minus` min s e) (UnpackedArr t shape) ->
TypeLiteral $ UnpackedArr t (MkPair s e `More` shape)
72 changes: 32 additions & 40 deletions src/Test/Verilog/Pretty.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,19 +101,17 @@ Show (TypeLiteralVect l t)
||| assign m = 'b1;
||| TODO: print the length of literal sometimes
|||
||| UAL x example:
||| Array example:
||| logic m [1:0][4:0];
||| assign m = '{'{'b1,'b0,'b1,'b0,'b1},'{'b0,'b1,'b0,'b1,'b0}};
|||
||| PAL x example:
||| logic [1:0][4:0] m;
||| assign m = 'b01010101;
Show (TypeLiteral sv) where
show (RL x) = show x
show (AL x) = show x
show (VL x) = show x
show (PAL x) = show x
show (UAL x) = show x
show (RL x) = show x
show (AL x) = show x
show (VL x) = show x
show (PALF x) = show x
show (PALM x) = show x
show (UALF x) = show x
show (UALM x) = show x

Show (TypeLiteralVect l t) where
show x = "'{\{joinBy "," $ map show $ toList x}}"
Expand All @@ -124,21 +122,22 @@ pn "" = ""
pn a = " \{a}"

showBasic : SVType -> String
showBasic (RVar x) = show x
showBasic (AVar x) = show x
showBasic (VVar x) = show x
showBasic (PackedArr t k j) = showBasic t
showBasic (UnpackedArr t k j) = showBasic t
showBasic (RVar x) = show x
showBasic (AVar x) = show x
showBasic (VVar x) = show x
showBasic (PackedArr t _) = showBasic t
showBasic (UnpackedArr t _) = showBasic t

showArrayDims : ArrayShape -> String
showArrayDims (One (MkPair s e)) = "[\{show s}:\{show e}]"
showArrayDims (MkPair s e `More` t) = "[\{show s}:\{show e}]" ++ showArrayDims t

showPackedSVT : SVType -> String
showPackedSVT (RVar x) = show x
showPackedSVT (AVar x) = show x
showPackedSVT (VVar x) = show x
showPackedSVT (PackedArr t {p} s e) = "\{showBasic t} [\{show s}:\{show e}]\{packDims t}" where
packDims : SVType -> String
packDims (PackedArr t s e) = "[\{show s}:\{show e}]" ++ packDims t
packDims _ = ""
showPackedSVT (UnpackedArr t s e) = ""
showPackedSVT (RVar x) = show x
showPackedSVT (AVar x) = show x
showPackedSVT (VVar x) = show x
showPackedSVT (PackedArr t {p} shape) = "\{showBasic t} \{showArrayDims shape}" where
Copy link
Collaborator

@L3odr0id L3odr0id Nov 6, 2025

Choose a reason for hiding this comment

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

I like array dimensions printing refactoring! Although there is a redundant keyword where left here and in the showSVType

showPackedSVT (UnpackedArr t _) = ""

||| examples:
||| bit uP [3:0]; //1-D unpacked
Expand All @@ -152,18 +151,11 @@ showPackedSVT (UnpackedArr t s e) = ""
||| int Array[0:7][0:31]; // array declaration using ranges
||| int Array[8][32]; // array declaration using sizes
showSVType : SVType -> (name : String) -> String
showSVType rv@(RVar x) name = "\{show x}\{pn name}"
showSVType sv@(AVar x) name = "\{show x}\{pn name}"
showSVType vv@(VVar x) name = "\{show x}\{pn name}"
showSVType pa@(PackedArr t {p} s e) name = "\{showPackedSVT pa} \{pn name}"
showSVType ua@(UnpackedArr t s e) name = "\{showPackedSVT $ basic t} \{name} [\{show s}:\{show e}]\{unpDimensions t}" where
basic : SVType -> SVType
basic (UnpackedArr t _ _) = basic t
basic t = t

unpDimensions : SVType -> String
unpDimensions (UnpackedArr t s e) = "[\{show s}:\{show e}]" ++ unpDimensions t
unpDimensions _ = ""
showSVType rv@(RVar x) name = "\{show x}\{pn name}"
showSVType sv@(AVar x) name = "\{show x}\{pn name}"
showSVType vv@(VVar x) name = "\{show x}\{pn name}"
showSVType pa@(PackedArr t {p} _) name = "\{showPackedSVT pa} \{pn name}"
showSVType ua@(UnpackedArr t s) name = "\{showPackedSVT t} \{name} \{showArrayDims s}" where

showSVObj : SVObject -> (name : String) -> String
showSVObj (Net nt t) name = "\{show nt} \{showSVType t name}"
Expand Down Expand Up @@ -264,7 +256,7 @@ iMcsByF mcs func fin = findIndex resolve $ toVect mcs where
resolve : MultiConnection ms m subMs -> Bool
resolve sc = isElem fin $ func sc

findMcsNameByF : (extractField : MultiConnection ms m subMs -> List $ Fin iport) ->
findMcsNameByF : (extractField : MultiConnection ms m subMs -> List $ Fin iport) ->
(mcs : MultiConnectionsList ms m subMs) -> Vect (length mcs) String -> Fin iport -> String
findMcsNameByF extract mcs mcsNames fin = case iMcsByF mcs extract fin of
Just mcsFin => index mcsFin mcsNames
Expand Down Expand Up @@ -319,8 +311,8 @@ parameters {opts : LayoutOpts} (m : ModuleSig) (ms: ModuleSigsList) (subMs : Fi
(ctxInps : List SVObject) -> (ctxOuts : List SVObject) -> (exInps : List String) -> (exOuts : List String) -> List (Doc opts)
printSubm' pre siNames soNames exM ctxInps ctxOuts exInps exOuts = do
let warningsSubOuts = printAllImplicitCasts showSVObj (toList exM.outputs) exOuts ctxOuts soNames
let warningsSubInps = printAllImplicitCasts showSVObj ctxInps siNames (toList exM.inputs) exInps
let warnings = if isNil warningsSubOuts ||
let warningsSubInps = printAllImplicitCasts showSVObj ctxInps siNames (toList exM.inputs) exInps
let warnings = if isNil warningsSubOuts ||
isNil warningsSubInps then warningsSubOuts ++ warningsSubInps else warningsSubOuts ++ [ "//" ] ++ warningsSubInps
case isNil warnings of
True => [ pre, line "" ]
Expand Down Expand Up @@ -388,8 +380,8 @@ resolveOutputNames mcs mcsNames = map (findTOName mcs mcsNames) $ allFins (m.out
||| Net types aren't compatible with unpacked arrays. So connections to unpacked array ports must be declared explicitly.
unpackedDecls : (mcs : MultiConnectionsList ms m subMs) -> Vect (length mcs) String -> List String
unpackedDecls [] _ = []
unpackedDecls (mc@(MkMC Nothing ssk Nothing ssc) :: mcs) (name::names) = if (isUnpacked $ typeOf mc)
then (showSVObj (typeOf mc) name) :: unpackedDecls mcs names
unpackedDecls (mc@(MkMC Nothing ssk Nothing ssc) :: mcs) (name::names) = if (isUnpacked $ typeOf mc)
then (showSVObj (typeOf mc) name) :: unpackedDecls mcs names
else unpackedDecls mcs names
unpackedDecls (mc :: mcs) (name::names) = unpackedDecls mcs names

Expand Down
Loading
Loading