never executed always true always false

    1 {-# LANGUAGE DuplicateRecordFields #-}
    2 {-# LANGUAGE OverloadedStrings #-}
    3 {-# LANGUAGE QuasiQuotes #-}
    4 {-# LANGUAGE RecordWildCards #-}
    5 {-# LANGUAGE StandaloneDeriving #-}
    6 {-# LANGUAGE TypeFamilies #-}
    7 
    8 {- |
    9 Module      : NITTA.Model.ProcessorUnits.Broken
   10 Description : Process Unit for negative tests
   11 Copyright   : (c) Aleksandr Penskoi, 2020
   12 License     : BSD3
   13 Maintainer  : aleksandr.penskoi@gmail.com
   14 Stability   : experimental
   15 -}
   16 module NITTA.Model.ProcessorUnits.Broken (
   17     Broken (..),
   18     Ports (..),
   19     IOPorts (..),
   20 ) where
   21 
   22 import Control.Monad
   23 import Data.Default
   24 import Data.List (find, (\\))
   25 import Data.Set (elems, fromList, member)
   26 import Data.String.Interpolate
   27 import Data.String.ToString
   28 import Data.Text qualified as T
   29 import NITTA.Intermediate.Functions qualified as F
   30 import NITTA.Intermediate.Types
   31 import NITTA.Model.Problems
   32 import NITTA.Model.ProcessorUnits.Types
   33 import NITTA.Model.Time
   34 import NITTA.Project
   35 import NITTA.Utils
   36 import NITTA.Utils.ProcessDescription
   37 import Numeric.Interval.NonEmpty (sup, (...))
   38 import Numeric.Interval.NonEmpty qualified as I
   39 import Prettyprinter
   40 
   41 data Broken v x t = Broken
   42     { remain :: [F v x]
   43     , targets :: [v]
   44     , sources :: [v]
   45     , doneAt :: Maybe t
   46     , currentWork :: Maybe (t, F v x)
   47     , currentWorkEndpoints :: [ProcessStepID]
   48     , process_ :: Process t (StepInfo v x t)
   49     , brokeVerilog :: Bool
   50     -- ^ generate verilog code with syntax error
   51     , wrongVerilogSimulationValue :: Bool
   52     -- ^ use process unit HW implementation with error
   53     , wrongControlOnPush :: Bool
   54     -- ^ wrong control sequence for data push (receiving data to PU)
   55     , wrongControlOnPull :: Bool
   56     -- ^ wrong control sequence for data pull (sending data from PU)
   57     , lostEndpointTarget :: Bool
   58     -- ^ lost target endpoint due synthesis
   59     , lostEndpointSource :: Bool
   60     -- ^ lost source endpoint due synthesis
   61     , wrongAttr :: Bool
   62     , lostFunctionInVerticalRelation :: Bool
   63     , lostEndpointInVerticalRelation :: Bool
   64     , lostInstructionInVerticalRelation :: Bool
   65     , unknownDataOut :: Bool
   66     }
   67 
   68 instance VarValTime v x t => Pretty (Broken v x t) where
   69     pretty Broken{..} =
   70         [__i|
   71             Broken:
   72                 remain:#{ remain }
   73                 targets:#{ map toString targets }
   74                 sources:#{ map toString sources }
   75                 currentWork: #{ currentWork }
   76                 currentWorkEndpoints: #{ currentWorkEndpoints }
   77                 brokeVerilog: #{ brokeVerilog }
   78                 wrongVerilogSimulationValue: #{ wrongVerilogSimulationValue }
   79                 wrongControlOnPush: #{ wrongControlOnPush }
   80                 wrongControlOnPull: #{ wrongControlOnPull }
   81                 lostEndpointTarget: #{ lostEndpointTarget }
   82                 lostEndpointSource: #{ lostEndpointSource }
   83                 wrongAttr: #{ wrongAttr }
   84                 unknownDataOut: #{ unknownDataOut }
   85                 #{ indent 4 $ pretty $ process_ }
   86             |]
   87 
   88 instance Var v => Locks (Broken v x t) v where
   89     locks Broken{remain, sources, targets} =
   90         [ Lock{lockBy, locked}
   91         | locked <- sources
   92         , lockBy <- targets
   93         ]
   94             ++ [ Lock{lockBy, locked}
   95                | locked <- concatMap (elems . variables) remain
   96                , lockBy <- sources ++ targets
   97                ]
   98 
   99 instance BreakLoopProblem (Broken v x t) v x
  100 instance ConstantFoldingProblem (Broken v x t) v x
  101 instance OptimizeAccumProblem (Broken v x t) v x
  102 instance ResolveDeadlockProblem (Broken v x t) v x
  103 
  104 instance VarValTime v x t => ProcessorUnit (Broken v x t) v x t where
  105     tryBind f pu@Broken{remain}
  106         | Just F.BrokenBuffer{} <- castF f = Right pu{remain = f : remain}
  107         | otherwise = Left $ "The function is unsupported by Broken: " ++ show f
  108     process = process_
  109 
  110 execution pu@Broken{targets = [], sources = [], remain, process_} f
  111     | Just (F.BrokenBuffer (I x) (O y)) <- castF f =
  112         pu
  113             { targets = [x]
  114             , sources = elems y
  115             , currentWork = Just (nextTick process_, f)
  116             , remain = remain \\ [f]
  117             }
  118 execution _ _ = error "Broken: internal execution error."
  119 
  120 instance VarValTime v x t => EndpointProblem (Broken v x t) v t where
  121     endpointOptions Broken{targets = [_], lostEndpointTarget = True} = []
  122     endpointOptions pu@Broken{targets = [v]} =
  123         let start = nextTick pu `withShift` 1 ... maxBound
  124             dur = 1 ... maxBound
  125          in [EndpointSt (Target v) $ TimeConstraint start dur]
  126     endpointOptions Broken{doneAt = Just _, lostEndpointSource = True} = []
  127     endpointOptions pu@Broken{sources, doneAt = Just at}
  128         | not $ null sources =
  129             let start = max at (nextTick pu + 1) ... maxBound
  130                 dur = 1 ... maxBound
  131              in [EndpointSt (Source $ fromList sources) $ TimeConstraint start dur]
  132     endpointOptions pu@Broken{remain, lostEndpointTarget = True}
  133         | not $ null remain = concatMap (endpointOptions . execution pu) $ tail remain
  134     endpointOptions pu@Broken{remain} = concatMap (endpointOptions . execution pu) remain
  135 
  136     endpointDecision pu@Broken{targets = [v], currentWorkEndpoints, wrongControlOnPush} d@EndpointSt{epRole = Target v', epAt}
  137         | v == v' =
  138             let workAt = epAt + I.singleton (if wrongControlOnPush then 1 else 0)
  139                 (newEndpoints, process_') = runSchedule pu $ do
  140                     scheduleEndpoint d $ scheduleInstructionUnsafe workAt Load
  141              in pu
  142                     { process_ = process_'
  143                     , targets = []
  144                     , currentWorkEndpoints = newEndpoints ++ currentWorkEndpoints
  145                     , doneAt = Just $ sup epAt + 3
  146                     }
  147     endpointDecision
  148         pu@Broken
  149             { targets = [v]
  150             , currentWorkEndpoints
  151             , wrongControlOnPush
  152             , lostEndpointInVerticalRelation
  153             , lostInstructionInVerticalRelation
  154             }
  155         d@EndpointSt{epRole = Target v', epAt}
  156             | v == v'
  157             , let (newEndpoints, process_') = runSchedule pu $ do
  158                     let ins =
  159                             if lostInstructionInVerticalRelation
  160                                 then return []
  161                                 else scheduleInstructionUnsafe (shiftI (if wrongControlOnPush then 1 else 0) epAt) Load
  162 
  163                     if lostEndpointInVerticalRelation
  164                         then return []
  165                         else scheduleEndpoint d ins =
  166                 pu
  167                     { process_ = process_'
  168                     , targets = []
  169                     , currentWorkEndpoints = newEndpoints ++ currentWorkEndpoints
  170                     , doneAt = Just $ sup epAt + 3
  171                     }
  172     endpointDecision
  173         pu@Broken
  174             { targets = []
  175             , sources
  176             , doneAt
  177             , currentWork = Just (a, f)
  178             , currentWorkEndpoints
  179             , wrongControlOnPull
  180             , lostFunctionInVerticalRelation
  181             , lostEndpointInVerticalRelation
  182             , lostInstructionInVerticalRelation
  183             }
  184         EndpointSt{epRole = epRole@(Source v), epAt}
  185             | not $ null sources
  186             , let sources' = sources \\ elems v
  187             , sources' /= sources
  188             , let (newEndpoints, process_') = runSchedule pu $ do
  189                     let doAt = shiftI (if wrongControlOnPull then 0 else -1) epAt
  190                     -- Inlined: endpoints <- scheduleEndpoint d $ scheduleInstructionUnsafe doAt Out
  191                     endpoints <- do
  192                         high <- scheduleStep epAt $ EndpointRoleStep epRole
  193                         low <- scheduleInstructionUnsafe doAt Out
  194                         establishVerticalRelations
  195                             (if lostEndpointInVerticalRelation then [] else high)
  196                             (if lostInstructionInVerticalRelation then [] else low)
  197                         return high
  198                     when (null sources') $ do
  199                         high <- scheduleFunction (a ... sup epAt) f
  200                         let low = endpoints ++ currentWorkEndpoints
  201                         establishVerticalRelations
  202                             (if lostFunctionInVerticalRelation then [] else high)
  203                             (if lostEndpointInVerticalRelation then [] else low)
  204                     return endpoints =
  205                 pu
  206                     { process_ = process_'
  207                     , sources = sources'
  208                     , doneAt = if null sources' then Nothing else doneAt
  209                     , currentWork = if null sources' then Nothing else Just (a, f)
  210                     , currentWorkEndpoints = if null sources' then [] else newEndpoints ++ currentWorkEndpoints
  211                     }
  212     endpointDecision pu@Broken{targets = [], sources = [], remain} d
  213         | let v = oneOf $ variables d
  214         , Just f <- find (\f -> v `member` variables f) remain =
  215             endpointDecision (execution pu f) d
  216     endpointDecision pu d = error [i|incorrect decision #{ d } for #{ pretty pu }|]
  217 
  218 instance Controllable (Broken v x t) where
  219     data Instruction (Broken v x t)
  220         = Load
  221         | Out
  222         deriving (Show)
  223 
  224     data Microcode (Broken v x t) = Microcode
  225         { wrSignal :: Bool
  226         , oeSignal :: Bool
  227         }
  228         deriving (Show, Eq, Ord)
  229 
  230     zipSignalTagsAndValues BrokenPorts{..} Microcode{..} =
  231         [ (wr, Bool wrSignal)
  232         , (oe, Bool oeSignal)
  233         ]
  234 
  235     usedPortTags BrokenPorts{wr, oe} = [wr, oe]
  236 
  237     takePortTags (wr : oe : _) _ = BrokenPorts wr oe
  238     takePortTags _ _ = error "can not take port tags, tags are over"
  239 
  240 instance Default (Microcode (Broken v x t)) where
  241     def =
  242         Microcode
  243             { wrSignal = False
  244             , oeSignal = False
  245             }
  246 
  247 instance Time t => Default (Broken v x t) where
  248     def =
  249         Broken
  250             { remain = []
  251             , targets = []
  252             , sources = []
  253             , doneAt = Nothing
  254             , currentWork = Nothing
  255             , currentWorkEndpoints = []
  256             , process_ = def
  257             , brokeVerilog = False
  258             , wrongVerilogSimulationValue = False
  259             , wrongControlOnPush = False
  260             , wrongControlOnPull = False
  261             , lostEndpointTarget = False
  262             , lostEndpointSource = False
  263             , wrongAttr = False
  264             , lostFunctionInVerticalRelation = False
  265             , lostEndpointInVerticalRelation = False
  266             , lostInstructionInVerticalRelation = False
  267             , unknownDataOut = False
  268             }
  269 
  270 instance Default x => DefaultX (Broken v x t) x
  271 
  272 instance UnambiguouslyDecode (Broken v x t) where
  273     decodeInstruction Load = def{wrSignal = True}
  274     decodeInstruction Out = def{oeSignal = True}
  275 
  276 instance Connected (Broken v x t) where
  277     data Ports (Broken v x t) = BrokenPorts
  278         { wr :: SignalTag
  279         , oe :: SignalTag
  280         }
  281         deriving (Show)
  282 
  283 instance IOConnected (Broken v x t) where
  284     data IOPorts (Broken v x t) = BrokenIO
  285         deriving (Show)
  286 
  287 instance VarValTime v x t => TargetSystemComponent (Broken v x t) where
  288     moduleName _title _pu = "pu_broken"
  289     software _ _ = Empty
  290     hardware _tag _pu = Aggregate Nothing [FromLibrary "pu_broken.v"]
  291 
  292     hardwareInstance
  293         tag
  294         pu@Broken{brokeVerilog, wrongVerilogSimulationValue, wrongAttr, unknownDataOut}
  295         UnitEnv
  296             { sigClk
  297             , ctrlPorts = Just BrokenPorts{..}
  298             , valueIn = Just (dataIn, attrIn)
  299             , valueOut = Just (dataOut, attrOut)
  300             } =
  301             [__i|
  302                 /*
  303                 #{ pretty pu }
  304                 */
  305                 pu_broken \#
  306                         ( .DATA_WIDTH( #{ dataWidth (def :: x) } )
  307                         , .ATTR_WIDTH( #{ attrWidth (def :: x) } )
  308                         , .IS_BROKEN( #{ bool2verilog wrongVerilogSimulationValue } )
  309                         , .WRONG_ATTR( #{ bool2verilog wrongAttr } )
  310                         , .UNKNOWN_DATA_OUT( #{ bool2verilog unknownDataOut } )
  311                         ) #{ tag }
  312                     ( .clk( #{ sigClk } )
  313 
  314                     , .signal_wr( #{ wr } )
  315                     , .data_in( #{ dataIn } ), .attr_in( #{ attrIn } )
  316 
  317                     , .signal_oe( #{ oe } )
  318                     , .data_out( #{ dataOut } ), .attr_out( #{ attrOut } )
  319                     #{ if brokeVerilog then "WRONG VERILOG" else "" :: T.Text }
  320                     );
  321             |]
  322     hardwareInstance _title _pu _env = error "internal error"
  323 
  324 instance IOTestBench (Broken v x t) v x
  325 
  326 instance Ord t => WithFunctions (Broken v x t) (F v x) where
  327     functions Broken{process_, remain, currentWork} =
  328         functions process_
  329             ++ remain
  330             ++ case currentWork of
  331                 Just (_, f) -> [f]
  332                 Nothing -> []
  333 
  334 instance VarValTime v x t => Testable (Broken v x t) v x where
  335     testBenchImplementation prj@Project{pName, pUnit} =
  336         Immediate (toString $ moduleName pName pUnit <> "_tb.v") $
  337             snippetTestBench
  338                 prj
  339                 SnippetTestBenchConf
  340                     { tbcSignals = ["oe", "wr"]
  341                     , tbcPorts =
  342                         BrokenPorts
  343                             { oe = SignalTag "oe"
  344                             , wr = SignalTag "wr"
  345                             }
  346                     , tbcMC2verilogLiteral = \Microcode{oeSignal, wrSignal} ->
  347                         [i|oe <= #{ bool2verilog oeSignal }; wr <= #{ bool2verilog wrSignal };|]
  348                     }