146 lines
4.1 KiB
Haskell
146 lines
4.1 KiB
Haskell
module Voter where
|
|
|
|
-- Can't produce verilog/vhdl: Blackbox error
|
|
-- https://groups.google.com/g/clash-language/c/fqzkxyY5eAw?pli=1
|
|
-- Probably because of `list' usage. Got to try vector. ✓
|
|
|
|
{-
|
|
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
|
|
|
|
-- | Representation of a sensor
|
|
data Sensor = Sensor {
|
|
out :: Int -- ^ Output value
|
|
, valid :: Bool -- ^ Output validity
|
|
}
|
|
|
|
-- | Possible states of system
|
|
data State
|
|
= VAll
|
|
| V2NoMis Int Int -- ^ valid sensor ids
|
|
| V2Mis Int Int -- ^ valid sensor ids
|
|
| V1 Int -- ^ valid sensor id
|
|
| VNone
|
|
deriving (Generic, NFDataX)
|
|
|
|
-- | Count number of valid sensors
|
|
countValidSens
|
|
:: Vec 3 Sensor -- ^ Sensors
|
|
-> Int -- ^ Valid sensor count
|
|
countValidSens sens = foldr (\s n -> if valid s then n+1 else n) 0 sens
|
|
|
|
-- | Find if a range is beyond a limit
|
|
tooMuch
|
|
:: Int -- ^ Maximum tolerance limit
|
|
-> Int -- ^ Range boundary
|
|
-> Int -- ^ Range boundary
|
|
-> Bool -- ^ Tell if range is within acceptable bounds
|
|
tooMuch limit a b =
|
|
let val = abs $ a - b in
|
|
val > limit
|
|
|
|
-- | Find if there is a miscomparing sensor when there are 3 valid sensors
|
|
isMiscomp3
|
|
:: Vec 3 Sensor -- ^ Sensors
|
|
-> Maybe Int -- ^ Tell if there is an odd sensor
|
|
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
|
|
|
|
-- | Find next state of system
|
|
nextState
|
|
:: State -- ^ Current state
|
|
-> Vec 3 Sensor -- ^ Sensor data
|
|
-> State -- ^ Next state
|
|
nextState VAll sens =
|
|
if countValidSens sens < 3 then
|
|
-- 1 sensor newly invalidated.
|
|
-- 2 valid sensors available. No miscompare.
|
|
-- (Assumption: No simultaneous failures)
|
|
let s12 = if (valid $ sens !! 0) && (valid $ sens !! 1) then (0, 1)
|
|
else if (valid $ sens !! 0) && (valid $ sens !! 2) then (0, 2)
|
|
else (1, 2) in
|
|
V2NoMis (fst s12) (snd s12)
|
|
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 =
|
|
if countValidSens sens < 2 then
|
|
-- 1 sensor newly invalidated.
|
|
-- 1 valid sensor available
|
|
let sid = if (valid $ sens !! 0) then 0
|
|
else if (valid $ sens !! 1) then 1
|
|
else 2 in
|
|
V1 sid
|
|
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 =
|
|
if countValidSens sens < 2 then
|
|
let sid = if (valid $ sens !! 0) then 0
|
|
else if (valid $ sens !! 1) then 1
|
|
else 2 in
|
|
V1 sid
|
|
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 =
|
|
if countValidSens sens < 1 then VNone
|
|
else V1 sid
|
|
|
|
nextState VNone sens = VNone
|
|
|
|
-- | Find next output upon given next state
|
|
-- Output is purely dependent on state
|
|
nextOut
|
|
:: State -- ^ Next state
|
|
-> Vec 3 Sensor -- ^ Sensor data
|
|
-> Sensor -- ^ Next output
|
|
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
|