From 0b1d4a05e9e4b8685f74a0e38cd139a319358e40 Mon Sep 17 00:00:00 2001
From: Julin S <famubu@rawtext.club>
Date: Wed, 20 Sep 2023 23:08:04 +0530
Subject: [PATCH] [clash] include haskell/Voter.hs

---
 haskell/Voter.hs | 117 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 117 insertions(+)
 create mode 100644 haskell/Voter.hs

diff --git a/haskell/Voter.hs b/haskell/Voter.hs
new file mode 100644
index 0000000..d59831a
--- /dev/null
+++ b/haskell/Voter.hs
@@ -0,0 +1,117 @@
+module Voter where
+
+{-
+Formal Modeling and Analysis of an Avionics Triplex Sensor Voter
+ - Samar Dajani-Brown, Darren Cofer, Gary Hartmann & Steve Pratt 
+ - 2003
+
+https://link.springer.com/chapter/10.1007/3-540-44829-2_3
+ -}
+
+import Clash.Prelude
+import qualified Data.List as L
+
+data Sensor = Sensor {
+    out :: Int     -- ^ Output value
+  , valid :: Bool  -- ^ Output validity
+}
+
+data State
+  = VAll
+  | V2NoMis Int Int -- ^ valid sensor ids
+  | V2Mis Int Int   -- ^ valid sensor ids
+  | V1 Int          -- ^ valid sensor id
+  | VNone
+  deriving (Generic, NFDataX)
+
+tooMuch :: Int -> Int -> Int -> Bool
+tooMuch limit a b =
+  let val = abs $ a - b in
+  val > limit
+
+isMiscomp3 :: Vec 3 Sensor -> Maybe Int
+isMiscomp3 sens =
+  let v01 = tooMuch 0 (out $ sens !! 0) (out $ sens !! 1) in
+  let v02 = tooMuch 0 (out $ sens !! 0) (out $ sens !! 2) in
+  let v12 = tooMuch 0 (out $ sens !! 1) (out $ sens !! 2) in
+  if v01 && v02 then Just 0
+  else if v01 && v12 then Just 1
+  else if v02 && v12 then Just 2
+  else Nothing
+
+validSensors :: Vec 3 Sensor -> [Int]
+validSensors sens = 
+  fst $ foldr (\s (res, curidx) ->
+                 (if valid s then curidx:res else res, curidx+1))
+        ([], 0) sens 
+
+nextState :: State -> Vec 3 Sensor -> State
+nextState VAll sens = 
+  let vsens = validSensors sens in
+  if L.length vsens < 3 then
+    -- 1 sensor newly invalidated.
+    -- 2 valid sensors available. No miscompare.
+    -- (Assumption: No simultaneous failures)
+    V2NoMis (vsens L.!! 1) (vsens L.!! 0)
+  else
+    -- No new invalid sensor
+    case isMiscomp3 sens of
+      Nothing -> VAll          -- No miscompare
+      Just sid -> case sid of  -- Miscompare. Cut off odd one.
+        0 -> V2NoMis 1 2
+        1 -> V2NoMis 0 2
+        2 -> V2NoMis 1 2
+
+nextState (V2NoMis sid1 sid2) sens =
+  let vsens = validSensors sens in
+  if L.length vsens < 2 then
+    -- 1 sensor newly invalidated.
+    -- 1 valid sensor available
+    V1 (vsens L.!! 0)
+  else
+    -- No new invalid sensor
+    case tooMuch 0 (out $ sens !! sid1) (out $ sens !! sid2) of
+      -- No miscompare
+      False -> V2NoMis sid1 sid2
+      -- Miscompare
+      True -> V2Mis sid1 sid2
+
+nextState (V2Mis sid1 sid2) sens =
+  let vsens = validSensors sens in
+  if L.length vsens < 2 then
+    V1 (vsens L.!! 0)
+  else
+    case tooMuch 0 (out $ sens !! sid1) (out $ sens !! sid2) of
+      -- Miscompare over!
+      False -> V2NoMis sid1 sid2
+      -- Still miscomparing..
+      True -> V2Mis sid1 sid2
+      
+nextState (V1 sid) sens =
+  let vsens = validSensors sens in
+  if vsens == [] then VNone
+  else V1 sid
+
+nextState VNone sens = VNone
+
+nextOut :: State -> Vec 3 Sensor -> Sensor
+nextOut st sens = case st of
+  VAll -> sens !! 0
+  V2NoMis sid1 _ -> sens !! sid1
+  V2Mis sid1 _ -> Sensor (out $ sens !! sid1) False
+  V1 sid -> sens !! sid
+  VNone -> Sensor (out $ sens !! 0) False
+
+topFn :: State -> Vec 3 Sensor -> (State, Sensor)
+topFn st sens =
+  let nst = nextState st sens in
+  let nout = nextOut nst sens in
+  (nst, nout)
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Vec 3 Sensor)
+  -> Signal System Sensor
+topEntity = exposeClockResetEnable $ mealy topFn VAll