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 )
33 where
34
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 (diff(actualData, expectData) > 1 || 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 function automatic diff;
478 input [31:0] a;
479 input [31:0] b;
480 begin
481 diff = (a > b) ? a - b : b - a;
482 end
483 endfunction
484 |]
485
486 verilogAssertRE _ =
487 mkRegex $
488 concat
489 [ "([[:digit:]]+):([[:digit:]]+)[\t ]"
490 , "actual:[\t ](-?[[:digit:]]+\\.[[:digit:]]+)[\t ]+[x[:digit:]]+[\t ]+"
491 , "expect:[\t ](-?[[:digit:]]+\\.[[:digit:]]+)[\t ]+[x[:digit:]]+[\t ]+"
492 , "var: ([^ \t\n]+)"
493 ]
494
495 instance (KnownNat m, KnownNat b) => FixedPointCompatible (FX m b) where
496 fractionalBitSize x = dataWidth x - fromInteger (natVal (Proxy :: Proxy m))
497 scalingFactorPower _ =
498 let m = natVal (Proxy :: Proxy m)
499 b = natVal (Proxy :: Proxy b)
500 in b - m
501
502 instance (KnownNat m, KnownNat b) => Real (FX m b) where
503 toRational x@FX{rawFX} = rawFX % 2 ^ scalingFactorPower x
504
505 instance (KnownNat m, KnownNat b) => ToJSON (FX m b) where
506 toJSON x@FX{} = toJSON (read $ show x :: Double)