never executed always true always false
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE FunctionalDependencies #-}
3 {-# LANGUAGE KindSignatures #-}
4 {-# LANGUAGE OverloadedStrings #-}
5 {-# LANGUAGE QuasiQuotes #-}
6 {-# LANGUAGE TypeOperators #-}
7
8 {-# OPTIONS -Wall -Wcompat -Wredundant-constraints -fno-warn-missing-signatures #-}
9
10 {- |
11 Module : NITTA.Intermediate.Value
12 Description : Processed value representation
13 Copyright : (c) Aleksandr Penskoi, 2020
14 License : BSD3
15 Maintainer : aleksandr.penskoi@gmail.com
16 Stability : experimental
17 -}
18 module NITTA.Intermediate.Value (
19 -- * Type classes
20 Val (..),
21 DefaultX (..),
22 FixedPointCompatible (..),
23 scalingFactor,
24 minMaxRaw,
25
26 -- * Compositional type
27 Attr (..),
28
29 -- * Value types
30 IntX (..),
31 FX (..),
32 ) where
33
34 import Control.Applicative
35 import Data.Aeson
36 import Data.Bits
37 import Data.Default
38 import Data.Maybe
39 import Data.Proxy
40 import Data.Ratio
41 import Data.String.Interpolate
42 import Data.Text qualified as T
43 import Data.Typeable
44 import Data.Validity hiding (invalid)
45 import GHC.Generics
46 import GHC.TypeLits
47 import NITTA.Utils.Base
48 import Numeric
49 import Text.Printf
50 import Text.Regex
51
52 -- | Type class for representation of processing values. A value should include two parts: data and attribute.
53 class
54 ( Typeable x
55 , Show x
56 , Read x
57 , PrintfArg x
58 , Default x
59 , Integral x
60 , Enum x
61 , Eq x
62 , Num x
63 , Bits x
64 , Validity x
65 , FixedPointCompatible x
66 , ToJSON x
67 ) =>
68 Val x
69 where
70 -- | data bus width
71 dataWidth :: x -> Int
72
73 -- | attribute bus width
74 attrWidth :: x -> Int
75 attrWidth _ = 4
76
77 -- | raw representation of data (@Integer@)
78 rawData :: x -> Integer
79
80 -- | raw representation of attributes (@Integer@)
81 rawAttr :: x -> Integer
82
83 -- | construct a value from raw data and attributes
84 fromRaw :: Integer -> Integer -> x
85
86 -- | convert a value to Verilog literal with data
87 dataLiteral :: x -> T.Text
88
89 -- | convert a value to Verilog literal with attributes
90 attrLiteral :: x -> T.Text
91 attrLiteral x = showText (attrWidth x) <> "'d0000"
92
93 -- | helper functions to work with values in Verilog (trace and assert)
94 verilogHelper :: x -> T.Text
95 verilogHelper x =
96 [__i|
97 task traceWithAttr;
98 input integer cycle;
99 input integer tick;
100 input [#{ dataWidth x }-1:0] actualData;
101 input [#{ attrWidth x }-1:0] actualAttr;
102 begin
103 $write("%0d:%0d\t", cycle, tick);
104 $write("actual: %d %d\t", actualData, actualAttr);
105 $display();
106 end
107 endtask // traceWithAttr
108
109 task assertWithAttr;
110 input integer cycle;
111 input integer tick;
112 input [#{ dataWidth x }-1:0] actualData;
113 input [#{ attrWidth x }-1:0] actualAttr;
114 input [#{ dataWidth x }-1:0] expectData;
115 input [#{ attrWidth x }-1:0] expectAttr;
116 input [256*8-1:0] var; // string
117 begin
118 $write("%0d:%0d\t", cycle, tick);
119 $write("actual: %d %d\t", actualData, actualAttr);
120 $write("expect: %d %d\t", expectData, expectAttr);
121 $write("var: %0s\t", var);
122 if ( actualData != expectData || actualAttr != expectAttr
123 || ( actualData === 'dx && !actualAttr[0] )
124 ) $write("FAIL");
125 $display();
126 end
127 endtask // assertWithAttr
128 |]
129
130 -- | RE for extraction assertion data from a testbench log
131 verilogAssertRE :: x -> Regex
132 verilogAssertRE _ =
133 mkRegex $
134 concat
135 [ "([[:digit:]]+):([[:digit:]]+)[\t ]+"
136 , "actual:[\t ]+(-?[[:digit:]]+)[\t ]+[x[:digit:]]+[\t ]+"
137 , "expect:[\t ]+(-?[[:digit:]]+)[\t ]+[x[:digit:]]+[\t ]+"
138 , "var: ([^ \t\n]+)"
139 ]
140
141 -- | Minimal and maximal raw value.
142 minMaxRaw x =
143 let n = dataWidth x
144 in minMaxRaw' n
145
146 minMaxRaw' n =
147 let maxRaw = 2 ^ (n - 1) - 1
148 minRaw = negate (maxRaw + 1)
149 in (minRaw, maxRaw)
150
151 invalidRaw x = snd (minMaxRaw x) + 1
152
153 crop x
154 | abs x == x = x .&. valueMask x
155 | otherwise = x .|. complement (valueMask x)
156
157 valueMask :: Val x => x -> x
158 valueMask x = fromRaw (setBit (0 :: Integer) (dataWidth x - 1) - 1) 0
159
160 -- TODO: try to avoid this class
161 class Default x => DefaultX u x | u -> x where
162 defX :: u -> x
163 defX _ = def
164
165 {- | Type class for values, which contain information about fractional part of
166 value (for fixed point arithmetics).
167 -}
168 class FixedPointCompatible a where
169 scalingFactorPower :: a -> Integer
170 fractionalBitSize :: a -> Int
171
172 scalingFactor x = 2 ** fromIntegral (scalingFactorPower x)
173
174 -- | All values with attributes.
175 data Attr x = Attr {value :: x, invalid :: Bool} deriving (Eq, Ord)
176
177 instance Validity x => Validity (Attr x) where
178 validate Attr{value} = validate value
179
180 setInvalidAttr Attr{value, invalid} = Attr{value, invalid = invalid || isInvalid value}
181
182 instance Functor Attr where
183 fmap f Attr{value, invalid} = Attr{value = f value, invalid}
184
185 instance Applicative Attr where
186 pure x = Attr{value = x, invalid = False}
187
188 liftA2 f Attr{value = x, invalid = x'} Attr{value = y, invalid = y'} =
189 let value = f x y
190 in Attr{value, invalid = x' || y'}
191
192 instance Show x => Show (Attr x) where
193 show Attr{invalid = True} = "NaN"
194 show Attr{value, invalid = False} = show value
195
196 instance Read x => Read (Attr x) where
197 readsPrec d r = case readsPrec d r of
198 [(x, r')] -> [(pure x, r')]
199 _ -> error $ "can not read IntX from: " ++ r
200
201 instance PrintfArg x => PrintfArg (Attr x) where
202 formatArg Attr{value} = formatArg value
203
204 instance Default x => Default (Attr x) where
205 def = pure def
206
207 instance (Enum x, Validity x) => Enum (Attr x) where
208 toEnum = setInvalidAttr . pure . toEnum
209 fromEnum Attr{value} = fromEnum value
210
211 instance (Num x, Validity x) => Num (Attr x) where
212 a + b = setInvalidAttr $ liftA2 (+) a b
213 a * b = setInvalidAttr $ liftA2 (*) a b
214 abs = setInvalidAttr . fmap abs
215 signum = setInvalidAttr . fmap signum
216 fromInteger = setInvalidAttr . pure . fromInteger
217 negate = setInvalidAttr . fmap negate
218
219 instance (Real x, Validity x) => Real (Attr x) where
220 toRational Attr{value} = toRational value
221
222 instance Val x => Integral (Attr x) where
223 toInteger Attr{value} = toInteger value
224 Attr{value = a} `quotRem` Attr{value = b} =
225 let (minB, maxB) = minMaxRaw' (dataWidth b `shiftR` 1)
226 (a', b') =
227 if b == 0 || b < minB || maxB < b
228 then (fromRaw (invalidRaw b) def, fromRaw (invalidRaw b) def)
229 else a `quotRem` b
230 in (setInvalidAttr $ pure a', setInvalidAttr $ pure b')
231
232 instance (Bits x, Validity x) => Bits (Attr x) where
233 a .&. b = setInvalidAttr $ liftA2 (.&.) a b
234 a .|. b = setInvalidAttr $ liftA2 (.|.) a b
235 xor a b = setInvalidAttr $ liftA2 xor a b
236 complement = setInvalidAttr . fmap complement
237 shift Attr{value} ix = setInvalidAttr $ pure $ shift value ix
238 rotate Attr{value} ix = setInvalidAttr $ pure $ rotate value ix
239 bitSize Attr{value} = fromMaybe undefined $ bitSizeMaybe value
240 bitSizeMaybe Attr{value} = bitSizeMaybe value
241 isSigned Attr{value} = isSigned value
242 testBit Attr{value} = testBit value
243 bit ix = pure $ bit ix
244 popCount Attr{value} = popCount value
245
246 instance Val x => Val (Attr x) where
247 dataWidth Attr{value} = dataWidth value
248
249 rawData Attr{value} = rawData value
250 rawAttr Attr{invalid = True} = 1
251 rawAttr Attr{invalid = False} = 0
252
253 fromRaw x a = setInvalidAttr $ pure $ fromRaw x a
254
255 dataLiteral Attr{value, invalid = True} = showText (dataWidth value) <> "'dx"
256 dataLiteral Attr{value} = dataLiteral value
257 attrLiteral x@Attr{invalid} =
258 showText (attrWidth x) <> "'b000" <> if invalid then "1" else "0"
259
260 verilogHelper Attr{value} = verilogHelper value
261 verilogAssertRE Attr{value} = verilogAssertRE value
262
263 instance FixedPointCompatible x => FixedPointCompatible (Attr x) where
264 scalingFactorPower Attr{value} = scalingFactorPower value
265 fractionalBitSize Attr{value} = fractionalBitSize value
266
267 instance ToJSON x => ToJSON (Attr x) where
268 toJSON Attr{value} = toJSON value
269
270 -- * Integer
271
272 instance FixedPointCompatible Int where
273 scalingFactorPower _ = 0
274 fractionalBitSize _ = 0
275
276 instance Val Int where
277 dataWidth x = finiteBitSize x
278
279 rawData x = fromIntegral x
280 rawAttr _ = 0
281 fromRaw x _ = fromEnum x
282
283 dataLiteral = showText
284
285 -- | Integer number with specific bit width.
286 newtype IntX (w :: Nat) = IntX {intX :: Integer}
287 deriving (Show, Eq, Ord)
288
289 instance KnownNat m => Validity (IntX m) where
290 validate x@(IntX raw) =
291 let (minRaw, maxRaw) = minMaxRaw x
292 in check (minRaw <= raw && raw <= maxRaw) "value is not out of range"
293
294 instance Read (IntX w) where
295 readsPrec d r = case readsPrec d r of
296 [(x, r')] -> [(IntX x, r')]
297 _ -> error $ "can not read IntX from: " ++ r
298
299 instance PrintfArg (IntX w) where
300 formatArg (IntX x) = formatInteger x
301
302 instance Default (IntX w) where
303 def = IntX 0
304
305 instance Enum (IntX w) where
306 toEnum = IntX . toInteger
307 fromEnum (IntX x) = fromInteger x
308
309 instance Num (IntX w) where
310 (IntX a) + (IntX b) = IntX (a + b)
311 (IntX a) * (IntX b) = IntX (a * b)
312 abs (IntX a) = IntX $ abs a
313 signum (IntX a) = IntX $ signum a
314 fromInteger a = IntX $ fromInteger a
315 negate (IntX a) = IntX $ negate a
316
317 instance Real (IntX w) where
318 toRational (IntX x) = toRational x
319
320 instance Integral (IntX w) where
321 toInteger (IntX x) = toInteger x
322 (IntX a) `quotRem` (IntX b) =
323 let (a', b') = a `quotRem` b
324 in (IntX a', IntX b')
325
326 instance KnownNat w => Bits (IntX w) where
327 (IntX a) .&. (IntX b) = IntX (a .&. b)
328 (IntX a) .|. (IntX b) = IntX (a .|. b)
329 (IntX a) `xor` (IntX b) = IntX (a `xor` b)
330 complement (IntX a) = IntX $ complement a
331 shift (IntX a) ix = crop $ IntX $ shift a ix
332 rotate (IntX a) ix = crop $ IntX $ rotate a ix
333
334 bitSize (IntX a) = fromMaybe undefined $ bitSizeMaybe a
335 bitSizeMaybe (IntX a) = bitSizeMaybe a
336 isSigned (IntX a) = isSigned a
337 testBit (IntX a) = testBit a
338 bit ix = IntX $ bit ix
339 popCount (IntX a) = popCount a
340
341 instance KnownNat w => Val (IntX w) where
342 dataWidth _ = fromInteger $ natVal (Proxy :: Proxy w)
343
344 rawData (IntX x) = fromIntegral x
345 rawAttr x = if isInvalid x then 1 else 0
346
347 fromRaw x _ = IntX x
348
349 dataLiteral (IntX x) = showText x
350
351 instance FixedPointCompatible (IntX w) where
352 scalingFactorPower _ = 0
353 fractionalBitSize _ = 0
354
355 instance ToJSON (IntX w) where
356 toJSON (IntX x) = toJSON x
357
358 -- * Fixed point
359
360 {- | Number with fixed point. FX m b where
361
362 - m the number of magnitude or integer bits
363 - b the total number of bits
364
365 fxm.b: The "fx" prefix is similar to the above, but uses the word length as
366 the second item in the dotted pair. For example, fx1.16 describes a number
367 with 1 magnitude bit and 15 fractional bits in a 16 bit word.
368 -}
369 newtype FX (m :: Nat) (b :: Nat) = FX {rawFX :: Integer}
370 deriving (Eq, Ord, Generic)
371
372 instance (KnownNat b, KnownNat m) => Validity (FX m b) where
373 validate t@(FX raw) =
374 let (minRaw, maxRaw) = minMaxRaw t
375 in check (minRaw <= raw && raw <= maxRaw) "value is not out of range"
376
377 instance (KnownNat m, KnownNat b) => Read (FX m b) where
378 readsPrec d r =
379 let x = case readsPrec d r of
380 [(x' :: Double, "")] -> x'
381 _ -> error $ "can not read FX from: " ++ r
382 result = FX $ round (x * scalingFactor result)
383 in [(result, "")]
384
385 instance (KnownNat m, KnownNat b) => PrintfArg (FX m b) where
386 formatArg (FX x) = formatInteger x
387
388 instance (KnownNat m, KnownNat b) => Show (FX m b) where
389 show t@(FX x) = showFFloat (Just 6) (fromIntegral x / scalingFactor t :: Double) ""
390
391 instance Default (FX m b) where
392 def = FX 0
393
394 instance (KnownNat m, KnownNat b) => Enum (FX m b) where
395 toEnum x =
396 let res = FX $ toInteger (x * truncate (scalingFactor res :: Double))
397 in res
398 fromEnum t@(FX x) = truncate (fromIntegral x / scalingFactor t :: Double)
399
400 instance (KnownNat m, KnownNat b) => Num (FX m b) where
401 (FX a) + (FX b) = FX (a + b)
402 t@(FX a) * (FX b) = FX ((a * b) `shiftR` fromInteger (scalingFactorPower t))
403 abs (FX a) = FX $ abs a
404 signum (FX a) = fromInteger $ signum a
405 fromInteger x = FX $ shiftL x $ fromInteger $ scalingFactorPower (def :: FX m b)
406 negate (FX a) = FX $ negate a
407
408 instance (KnownNat m, KnownNat b) => Integral (FX m b) where
409 toInteger t = toInteger $ fromEnum t
410 t@(FX a) `quotRem` (FX b) =
411 let (a', b') = a `quotRem` b
412 sf = scalingFactor t
413 in (FX $ truncate (fromIntegral a' * sf :: Double), FX b')
414
415 instance (KnownNat m, KnownNat b) => Bits (FX m b) where
416 (FX a) .&. (FX b) = FX (a .&. b)
417 (FX a) .|. (FX b) = FX (a .|. b)
418 (FX a) `xor` (FX b) = FX (a `xor` b)
419 complement (FX a) = FX $ complement a
420 shift (FX a) ix = crop $ FX $ shift a ix
421 rotate (FX a) ix = crop $ FX $ rotate a ix
422 bitSize = dataWidth
423 bitSizeMaybe = Just . dataWidth
424 isSigned (FX a) = isSigned a
425 testBit (FX a) = testBit a
426 bit ix = FX $ bit ix
427 popCount (FX a) = popCount a
428
429 instance (KnownNat m, KnownNat b) => Val (FX m b) where
430 dataWidth _ = fromInteger $ natVal (Proxy :: Proxy b)
431
432 rawData (FX x) = x
433 rawAttr x = if isInvalid x then 1 else 0
434 fromRaw x _ = FX x
435
436 dataLiteral (FX x) = showText x
437 attrLiteral x = showText (attrWidth x) <> "'d000" <> showText (rawAttr x)
438
439 verilogHelper x =
440 [__i|
441 task traceWithAttr;
442 input integer cycle;
443 input integer tick;
444 input [#{ dataWidth x }-1:0] actualData;
445 input [#{ attrWidth x }-1:0] actualAttr;
446 begin
447 $write("%0d:%0d\t", cycle, tick);
448 $write("actual: %.3f %d\t", fxtor(actualData), actualAttr);
449 $display();
450 end
451 endtask // traceWithAttr
452
453 task assertWithAttr;
454 input integer cycle;
455 input integer tick;
456 input [#{ dataWidth x }-1:0] actualData;
457 input [#{ attrWidth x }-1:0] actualAttr;
458 input [#{ dataWidth x }-1:0] expectData;
459 input [#{ attrWidth x }-1:0] expectAttr;
460 input [256*8-1:0] var; // string
461 begin
462 $write("%0d:%0d\t", cycle, tick);
463 $write("actual: %.3f %d \t", fxtor(actualData), actualAttr);
464 $write("expect: %.3f %d \t", fxtor(expectData), expectAttr);
465 $write("var: %0s\t", var);
466 if ( actualData !== expectData || actualAttr != expectAttr ) $write("FAIL");
467 $display();
468 end
469 endtask // assertWithAttr
470
471 function real fxtor(input integer x);
472 begin
473 fxtor = $itor(x) / $itor(1 << #{ scalingFactorPower x });
474 end
475 endfunction // fxtor
476 |]
477
478 verilogAssertRE _ =
479 mkRegex $
480 concat
481 [ "([[:digit:]]+):([[:digit:]]+)[\t ]"
482 , "actual:[\t ](-?[[:digit:]]+\\.[[:digit:]]+)[\t ]+[x[:digit:]]+[\t ]+"
483 , "expect:[\t ](-?[[:digit:]]+\\.[[:digit:]]+)[\t ]+[x[:digit:]]+[\t ]+"
484 , "var: ([^ \t\n]+)"
485 ]
486
487 instance (KnownNat m, KnownNat b) => FixedPointCompatible (FX m b) where
488 fractionalBitSize x = dataWidth x - fromInteger (natVal (Proxy :: Proxy m))
489 scalingFactorPower _ =
490 let m = natVal (Proxy :: Proxy m)
491 b = natVal (Proxy :: Proxy b)
492 in b - m
493
494 instance (KnownNat m, KnownNat b) => Real (FX m b) where
495 toRational x@FX{rawFX} = rawFX % 2 ^ scalingFactorPower x
496
497 instance (KnownNat m, KnownNat b) => ToJSON (FX m b) where
498 toJSON x@FX{} = toJSON (read $ show x :: Double)