-- exhibiting hdl failure under clash 1.8.1. (works fine under 1.6.4) -- PTB Dec 2023 -- 1.6.4: -- time clash -XCPP -fconstraint-solver-iterations=0 -package silently \ -- -fclash-no-render-enums -fclash-spec-limit=80 -fclash-inline-limit=80 \ -- -freduction-depth=400 -fclash-clear --verilog Test.hs -- GHC: Setting up GHC took: 1.059s -- GHC: Compiling and loading modules took: 1.801s -- Clash: Parsing and compiling primitives took 0.305s -- GHC+Clash: Loading modules cumulatively took 3.626s -- Clash: Compiling Test.tacache_server32 -- Clash: Normalization took 0.507s -- Clash: Netlist generation took 0.015s -- Clash: Compiling Test.tacache_server32 took 0.653s -- Clash: Total compilation took 4.280s -- 3.458u 0.794s 0:04.57 92.7% 0+0k 528264+976io 677pf+0w -- 1.8.1: -- time clash -XCPP -fconstraint-solver-iterations=0 -package silently \ -- -fclash-no-render-enums -fclash-spec-limit=80 -fclash-inline-limit=80 \ -- -freduction-depth=400 -fclash-clear --verilog Test.hs -- GHC: Setting up GHC took: 0.989s -- GHC: Compiling and loading modules took: 1.895s -- Clash: Parsing and compiling primitives took 0.318s -- GHC+Clash: Loading modules cumulatively took 3.807s -- Clash: Compiling Test.tacache_server32 -- Clash: Normalization took 0.368s -- : error: -- Clash error call: -- Clash.Netlist(1041): Under-applied constructor Product -- "GHC.Tuple.(,)" Nothing [Vector 1 (SP "GHC.Maybe.Maybe" -- [("GHC.Maybe.Nothing",[]),("GHC.Maybe.Just",[ -- Product "GHC.Tuple.(,)" Nothing [Signed 126,SP "GHC.Maybe.Maybe" -- [("GHC.Maybe.Nothing",[]),("GHC.Maybe.Just",[Signed 32])]]])]),Signed 126] -- -- Applied args: -- [Identifier (RawIdentifier "result_7" Nothing []) (Just (Indexed -- (Product "GHC.Tuple.(,)" Nothing [Vector 1 (SP "GHC.Maybe.Maybe" -- [("GHC.Maybe.Nothing",[]), ("GHC.Maybe.Just",[Product "GHC.Tuple.(,)" -- Nothing [Signed 126,SP "GHC.Maybe.Maybe" [("GHC.Maybe.Nothing",[]), -- ("GHC.Maybe.Just",[Signed 32])]]])]),Sum "GHC.Maybe.Maybe" -- ["GHC.Maybe.Nothing","GHC.Maybe.Just"]],0,0)))] -- -- Function args: -- (Product "GHC.Tuple.(,)" Nothing [Vector 1 (SP "GHC.Maybe.Maybe" -- [("GHC.Maybe.Nothing",[]),("GHC.Maybe.Just",[Product -- "GHC.Tuple.(,)" Nothing [Signed 126,SP "GHC.Maybe.Maybe" -- [("GHC.Maybe.Nothing",[]),("GHC.Maybe.Just",[Signed 32])]]])]), -- Signed 126],Name {nameSort = User, nameOcc = "GHC.Tuple.(,)", ... -- ... -- CallStack (from HasCallStack): -- error, called at src/Clash/Netlist.hs:1041:17 in -- clash-lib-1.8.1-HGqecslfsXx3PEFezUYUbi:Clash.Netlist -- mkDcApplication, called at src/Clash/Netlist.hs:863:16 in -- clash-lib-1.8.1-HGqecslfsXx3PEFezUYUbi:Clash.Netlist -- mkExpr, called at src/Clash/Netlist.hs:508:31 in -- clash-lib-1.8.1-HGqecslfsXx3PEFezUYUbi:Clash.Netlist -- 3.913u 0.599s 0:04.52 99.5% 0+0k 0+896io 0pf+0w module Test where import Clash.Prelude import Control.Monad.State -- frontend part of a memoizing cache for a TLB (translation lookaside buffer) -- acting as three-way intermediate collating user and cache and TLB data -- -- inputs -- user port A for translation requests accessing memoized data -- user port B for invalidate memoized translation commands -- tlb port C for weak invalidate memoized translation commands from the TLB -- tlb port D for weak translation info to be memoized snooped from the TLB -- cache port A for cacheline from cache holding translate data for req A -- cache port B for cacheline from cache holding translate data for cmd B -- cache port C for cacheline from cache holding translate data for cmd C -- -- outputs -- user port A replying to translation requests A with translation data -- cache port A1 for returning a modified cacheline -- cache port A2 for returning a modified cacheline (may need 2 at once) -- cache port B requesting cacheline containing invalid data B -- cache port C requesting cacheline containing invalid data C -- cache port D requesting cacheline to hold translated data D {-# ANN tacache_server32 (Synthesize { t_name = "TACacheServer" , t_inputs = [ PortName "dx" -- user B , PortName "d_x" -- tlb C , PortName "dw" -- tlb D , PortName "outs2" -- cache B , PortName "outs3" -- cache C ] , t_output = PortProduct "" [ PortName "wins1" -- cache A1 , PortName "wins2" -- cache A2 ] }) #-} -- for definiteness type IDX = Signed 6 type TAG = Signed 126 -- 6+126 = 132 type Cxdr = Signed 132 type Addr = Signed 32 {-# NOINLINE tacache_server32 #-} tacache_server32 = exposeClockResetEnable tacache_server' where tacache_server' :: forall (dom::Domain) (m::Nat) (n::Nat) (p::Nat) (q::Nat) cxdr addr idx tag cacheline . ( HiddenClockResetEnable dom , KnownNat q, KnownNat n, KnownNat m, KnownNat p , n <= p , cxdr ~ Signed p , addr ~ Signed q , idx ~ Signed n , tag ~ Signed (p-n) , cacheline ~ CacheLine m tag addr , p ~ 132 , q ~ 32 , n ~ 6 , m ~ 0 , dom ~ System ) -- SNat n -- 2^n lines -- SNat m -- of 2^m entries each => Signal dom (Maybe cxdr) -- input frnt invalidate addr req to server -> Signal dom (Maybe cxdr) -- input back/weak invalidate req to server -> Signal dom (Maybe (cxdr,addr)) -- input back/weak write req to server -> Signal dom (Maybe (idx,cacheline)) -> Signal dom (Maybe (idx,cacheline)) -> ( Signal dom (Maybe(idx,cacheline)) , Signal dom (Maybe(idx,cacheline)) ) tacache_server' = tacache_server n m where n = SNat :: SNat n -- 2^n (64) lines m = SNat :: SNat m -- 2^m (1) tags per line -- idx cacheline entries are Just(tag,Just addr) to translate idx++tag->addr -- and Just(tag,Nothing) for invalidated idx++tag entry -- and Nothing for no entry there type CacheLine m tag addr -- 2^m tags per line, 2^n lines = Vec (2^m) (Maybe(tag,Maybe addr)) {-# NOINLINE tacache_server #-} tacache_server :: forall (dom::Domain) (m::Nat) (n::Nat) (p::Nat) (q::Nat) cxdr -- cache key addr -- cache data idx -- cacheline index (which cacheline) tag -- cacheline tag (identifier for search in cacheline) cacheline . ( HiddenClockResetEnable dom , KnownNat q, KnownNat n, KnownNat m, KnownNat p , n <= p , cxdr ~ Signed p , addr ~ Signed q , idx ~ Signed n , tag ~ Signed (p-n) , cacheline ~ CacheLine m tag addr -- , p ~ 132 -- , q ~ 32 ) => SNat n -- 2^n cachelines -> SNat m -- of 2^m entries each -> Signal dom (Maybe cxdr) -- input frnt invalidate addr req to server -> Signal dom (Maybe cxdr) -- input back/weak invalidate req to server -> Signal dom (Maybe (cxdr,addr)) -- input back/weak write req to server -> Signal dom (Maybe (idx,cacheline)) -- cacheline in from cache -> Signal dom (Maybe (idx,cacheline)) -- cacheline in from cache -> ( Signal dom (Maybe(idx,cacheline)) -- cacheline out to cache , Signal dom (Maybe(idx,cacheline)) -- cacheline out to cache ) tacache_server n m dx d_x dw outs1 outs2 = (wins1,wins2) where (wins1,wins2) = unbundle $ fmap (tacache_server_step n m) $ bundle(dx,d_x,dw,outs1,outs2) tacache_server_step :: forall (m::Nat) (n::Nat) (p::Nat) (q::Nat) cxdr addr idx tag cacheline . ( KnownNat q, KnownNat n, KnownNat m, KnownNat p , n <= p , cxdr ~ Signed p , addr ~ Signed q , idx ~ Signed n , tag ~ Signed (p-n) , cacheline ~ CacheLine m tag addr -- , p ~ 132 -- , q ~ 32 ) => SNat n -- 2^n lines -> SNat m -- of 2^m entries each -> ( Maybe cxdr -- input frnt invalidate addr req to server , Maybe cxdr -- input back/weak invalidate req to server , Maybe (cxdr,addr) -- input back/weak write req to server , Maybe (idx,cacheline) , Maybe (idx,cacheline) ) -> ( Maybe(idx,cacheline) , Maybe(idx,cacheline) ) tacache_server_step n m (dx,d_x,dw,out1,out2) = (win1,win2) where -- outs1 and outs2 are prev state -- (may need to write two lines in one cycle) win1,win2 :: Maybe(idx,CacheLine m tag addr) (win1,win2) = case (dx, d_x, dw, out1, out2) of -- !!! FIX for HDL from here on, replace (v,_) = with v = fst $ !!! -- (Just x1,Just x2,Nothing,Just (idx1,v1),Just (idx2,v2)) -> let (idx1',tag1) = tacache_split_cxdr x1 (idx2',tag2) = tacache_split_cxdr x2 in if idx1' /= idx2' then ( if idx1 == idx1' then Just(idx1',v1) else Nothing , if idx2 == idx2' then Just(idx2',v2) else Nothing ) else let (v1',_) = tazcache_line_inval_step v1 tag1 -- NEED (v2',_) = tazcache_line_weak_inval_step v1' tag2 -- NEED in ( if idx2 == idx2' then Just(idx2',v2') else Nothing , Nothing ) -- !!! FIX for HDL from here, as above, and make cases top level fns !!! --- (Nothing,Just x,Nothing,_,Just (idx,v)) -> let (v',_) = tazcache_line_weak_inval_step v tag -- NEED (idx',tag) = tacache_split_cxdr x in ( Nothing , if idx == idx' then Just(idx',v') else Nothing ) _ -> (Nothing,Nothing) -------------------- support ----------------------- -- split incoming addr for translation into a cacheline index and tag {-# NOINLINE tacache_split_cxdr #-} tacache_split_cxdr :: forall (n::Nat) (p::Nat) tag cxdr idx f . ( KnownNat n, KnownNat p , Resize f -- might as well be just Signed , n <= p, n + (p-n) ~ p, (p-n) + n ~ p , BitPack cxdr, p ~ BitSize cxdr, cxdr ~ f p , BitPack idx, n ~ BitSize idx, idx ~ f n , BitPack tag, (p-n) ~ BitSize tag, tag ~ f (p-n) ) => cxdr -> (idx,tag) tacache_split_cxdr x = (unpack (-1), unpack (-1)) -------------------- cacheline ops ----------------------- -- remove element with matching tag from cacheline, report position {-# NOINLINE tazcache_line_inval_step #-} tazcache_line_inval_step :: ( KnownNat m, KnownNat p_n, KnownNat q , BitPack tag, p_n ~ BitSize tag, Eq tag , BitPack addr, q ~ BitSize addr ) => CacheLine m tag addr -> tag -> (CacheLine m tag addr, Maybe(Index(2^m))) tazcache_line_inval_step v tag = (v,Nothing) -- add placeholder invalidated entry to cacheline, replace entry if was there {-# NOINLINE tazcache_line_weak_inval_step #-} tazcache_line_weak_inval_step :: ( KnownNat m, KnownNat p_n, KnownNat q , BitPack tag, p_n ~ BitSize tag, Eq tag , BitPack addr, q ~ BitSize addr ) => CacheLine m tag addr -> tag -> (CacheLine m tag addr, Maybe(Index(2^m))) tazcache_line_weak_inval_step v tag = (v,Nothing)