diff --git a/lib/linguist/heuristics.yml b/lib/linguist/heuristics.yml index ae016448f..773974ac1 100644 --- a/lib/linguist/heuristics.yml +++ b/lib/linguist/heuristics.yml @@ -130,6 +130,8 @@ disambiguations: - (?i:^\s*(end\ssub)$) - (?i:^\s*(?=^function\s)(?:function\s*\w+\(.*?\)\s*as\s*\w*)|(?::\s*function\(.*?\)\s*as\s*\w*)$) - (?i:^\s*(end\sfunction)$) + - language: Bluespec BH + pattern: '^package\s+[A-Za-z_][A-Za-z0-9_'']*(?:\s*\(|\s+where)' - extensions: ['.builds'] rules: - language: XML diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml index aa41b38bf..cd3332d14 100644 --- a/lib/linguist/languages.yml +++ b/lib/linguist/languages.yml @@ -641,9 +641,28 @@ Bluespec: color: "#12223c" extensions: - ".bsv" + aliases: + - bluespec bsv + - bsv tm_scope: source.bsv ace_mode: verilog + codemirror_mode: verilog + codemirror_mime_type: text/x-systemverilog language_id: 36 +Bluespec BH: + type: programming + group: Bluespec + color: "#12223c" + extensions: + - ".bs" + aliases: + - bh + - bluespec classic + tm_scope: source.haskell + ace_mode: haskell + codemirror_mode: haskell + codemirror_mime_type: text/x-haskell + language_id: 641580358 Boo: type: programming color: "#d4bec1" diff --git a/samples/Bluespec BH/CGetPut.bs b/samples/Bluespec BH/CGetPut.bs new file mode 100644 index 000000000..34e394457 --- /dev/null +++ b/samples/Bluespec BH/CGetPut.bs @@ -0,0 +1,373 @@ +-- Copyright (c) 2020 Bluespec, Inc. All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- 1. Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- +-- 2. Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the +-- distribution. +-- +-- 3. Neither the name of the copyright holder nor the names of its +-- contributors may be used to endorse or promote products derived +-- from this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +-- "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +-- LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +-- A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +-- HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +-- SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +-- LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +-- DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +-- THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +-- (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +-- OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +package CGetPut(CGet, CPut, CGetS, CPutS, + CGetPut, GetCPut, mkCGetPut, mkGetCPut, mkCGetCPut, CClientServer, ClientCServer, + CClient, CServer, CClientS(..), CServerS(..), mkCClientServer, mkClientCServer) where +import FIFOF +import ConfigReg +import Connectable +import GetPut +import ClientServer +import Vector +import RegTwo + +--@ \subsubsection{CGetPut} +--@ \index{CGetPut@\te{CGetPut} (package)|textbf} +--@ +--@ The interfaces \te{CGet} and \te{CPut} are similar to +--@ \te{Get} and \te{Put}, but the interconnection of them +--@ (via \te{Connectable}) is implemented with a credit based +--@ FIFO. This means that the \te{CGet} and \te{CPut} interfaces +--@ have completely registered input and outputs, and furthermore +--@ that additional register buffers can be introduced in the connection path +--@ without any ill effect (except an increase in latency, of course). + +interface (CGetS :: # -> * -> # -> *) n a sa = + gvalue :: Bit sa + gpresent :: Bool + gcredit :: Bool -> Action + +interface (CPutS :: # -> * -> # -> *) n a sa = + pvalue :: Bit sa -> Action + ppresent :: Bool -> Action + pcredit :: Bool + +--@ The interface types are abstract (to avoid any non-proper use of +--@ the credit signaling protocol). +--@ +--@ In the absence of additional register buffers, the round-trip time for communication +--@ between the two interfaces is 4 clock cycles. Call this number $r$. The first argument +--@ to the type, $n$, specifies that transfers will occur for a fraction $n/r$ of clock +--@ cycles (note that the used cycles will not necessarily be evenly spaced). $n$ also +--@ specifies the depth of the buffer used in the receiving interface (the transmitter side +--@ always has only a single buffer). So (in the absence of additional buffers) use $n=4$ +--@ to allow full-bandwidth transmission, at the cost of sufficient registers for quadruple +--@ buffering at one end; use $n=1$ for minimal use of registers, at the cost of reducing +--@ the bandwidth to one quarter; use intermediate values to select the optimal trade-off if +--@ appropriate. +--@ +--@ \note{For compiler reasons the actual interfaces are called \te{CGetS} and \te{CPutS} +--@ with \te{CGet} and \te{CPut} being type abbreviations. Hopefully this will +--@ be fixed soon.} +--@ \begin{libverbatim} +--@ typedef CGetS#(n, a, SizeOf#(a)) CGet #(type n, type a); +--@ \end{libverbatim} +type CGet n a = CGetS n a (SizeOf a) + +--@ \lineup +--@ \begin{libverbatim} +--@ typedef CPutS#(n, a, SizeOf#(a)) CPut #(type n, type a); +--@ \end{libverbatim} +type CPut n a = CPutS n a (SizeOf a) + +type CGetPut n a = (CGet n a, Put a) +type GetCPut n a = (Get a, CPut n a) + +--@ Create one end of the credit based FIFO. Access to it is via a \te{Put} interface. +--@ \index{mkCGetPut@\te{mkCGetPut} (function)|textbf} +--@ \begin{libverbatim} +--@ module mkCGetPut(Tuple2 #(CGetS#(n, a, sa), Put#(a))) +--@ provisos (Bits#(a, sa), Add#(1, k, n), Add#(n, 1, n1), Log#(n1, ln)); +--@ \end{libverbatim} +mkCGetPut :: (IsModule m c, Bits a sa, Add 1 k n, Add n 1 n1, Log n1 ln) => m (CGetS n a sa, Put a) +mkCGetPut = + module + putbuf :: FIFOF (Bit sa) <- mkUGLFIFOF + credits :: FIFOF () <- mkUGLSizedFIFOF (valueOf n - 1) + free :: Reg Bool <- mkConfigReg False + let hasData = putbuf.notEmpty + rules + {-# ASSERT no implicit conditions #-} + {-# ASSERT fire when enabled #-} + "deq": + when hasData + ==> putbuf.deq + {-# ASSERT no implicit conditions #-} + {-# ASSERT fire when enabled #-} + "free": + when free + ==> credits.deq + interface -- Pair + (interface CGetS + gvalue = putbuf.first + gpresent = hasData + gcredit b = free := b + , + interface Put + put x = action + putbuf.enq (pack x) + credits.enq () + when (credits.notFull || free) + ) +--@ Create the other end of the credit based FIFO. Access to it is via a \te{Get} interface. +--@ \index{mkGetCPut@\te{mkGetCPut} (function)|textbf} +--@ \begin{libverbatim} +--@ module mkGetCPut(Tuple2 #(Get#(a), CPutS#(n, a, sa))) +--@ provisos (Bits#(a, sa), Add#(1, k, n), Log#(n, ln)); +--@ \end{libverbatim} +mkGetCPut :: (IsModule m c, Bits a sa, Add 1 k n, Log n ln) => m (Get a, CPutS n a sa) +mkGetCPut = + if valueOf n > 1 then + module + buff :: Vector n (Reg (Bit sa)) <- genWithM $ const mkConfigRegU + gotPresent :: Reg Bool <- mkConfigReg False + present :: Vector n (Reg Bool) <- genWithM $ const $ mkConfigReg False + ptr :: Reg (Bit ln) <- mkConfigReg 0 + crd :: FIFOF () <- mkUGLFIFOF + let + presentEffective :: Vector n Bool + presentEffective = zipWith (\idx p -> if idx == 0 then gotPresent || p else p) genList (map readReg present) + +-- allAheadTrue :: Vector n Bool -> Vector n Bool +-- allAheadTrue bs = let (_, result) = mapAccumR (\aat b -> (aat && b, aat && b)) True bs + + + + bubble :: (Action, Vector n Bool) + bubble = let f :: (Integer, Bool, Action) -> (Reg Bool, Bool, Reg (Bit sa)) -> ((Integer, Bool, Action), Bool) + f (idx, filled, upds) (p, pe, b) = + ( + (idx-1 + , + filled && pe + , + action {upds; if not (filled && pe) then (if idx /= 0 then action {p := presentEffective !! (idx-1); b := (buff !! (idx-1))._read} else action {p := False}) else action {}} + ) + , + if not (filled && pe) then (if idx /= 0 then presentEffective !! (idx-1) else False) else pe + ) + ((_, _, b_updates), b_presentNext) = mapAccumR f (valueOf n - 1, True, action {}) (zip3 present presentEffective buff) + in (b_updates, b_presentNext) + presentNext :: Vector n Bool + presentNext = bubble.snd + updates :: Action + updates = bubble.fst +-- updates :: Vector n Bool -> (Vector n Bool, Vector n Action) +-- updates bs = let f idx (pag, aap, b) = case idx of +-- 0 -> if not aap then (False, noAction) else (pag, noAction) +-- _ -> if not aap then (select presentAfterGet (idx-1), b := (select buff (idx-1))._read) else (pag, noAction) +-- in unzip $ zipWith f genList (zip3 presentAfterGet allAheadPresent buff) + + clearLastTrue :: Vector n Bool -> Vector n Bool + clearLastTrue bs = let (_, result) = mapAccumR (\found b -> if (not found && b) then (True, False) else (found, b)) False bs + in result + lastTrueIdx :: Vector n Bool -> Bit ln + lastTrueIdx bs = let f (idx, h) b = if b then (idx+1, idx) else (idx+1, h) + (_, result) = foldl f (0, 0) bs + in result + + rw :: RWire () + rw <- mkRWire + + rules + {-# ASSERT no implicit conditions #-} + "update": + when rw.wget == Nothing + ==> action updates + ptr := lastTrueIdx presentNext + {-# ASSERT no implicit conditions #-} + {-# ASSERT fire when enabled #-} + "deq-crd": + when crd.notEmpty + ==> crd.deq + interface -- Pair + (interface Get + get = do rw.wset() + crd.enq () + joinActions $ zipWith writeReg present (cons False (init $ clearLastTrue presentEffective)) + joinActions $ zipWith writeReg (tail buff) (init $ map readReg buff) + ptr._write $ lastTrueIdx $ cons False (init $ clearLastTrue presentEffective) + return $ unpack (select buff ptr)._read + when (fold (||) presentEffective) + , + interface CPutS + pvalue v = (head buff)._write v + ppresent p = gotPresent := p + pcredit = crd.notEmpty + ) + else + module + buff :: Reg (Bit sa) <- mkConfigRegU + present :: RegTwo Bool <- mkRegTwo False + gotPresent :: Reg Bool <- mkConfigReg False + crd :: FIFOF () <- mkUGLFIFOF + rules + {-# ASSERT no implicit conditions #-} + {-# ASSERT fire when enabled #-} + "deq-crd": + when crd.notEmpty ==> crd.deq + {-# ASSERT no implicit conditions #-} + {-# ASSERT fire when enabled #-} + "save": + when gotPresent ==> present.setB True + interface -- Pair + (interface Get + get = do crd.enq () + present.setA False + return $ unpack buff + when (gotPresent || present.get) + , + interface CPutS + pvalue v = buff := v + ppresent p = gotPresent := p + pcredit = crd.notEmpty + ) + +--@ Create a buffer that can be inserted along a connection path. +--@ \index{mkCGetCPut@\te{mkCGetCPut} (function)|textbf} +--@ \begin{libverbatim} +--@ module mkCGetCPut(Tuple2 #(CGetS#(n, a, sa), CPutS#(n, a, sa))) +--@ provisos (Bits#(a, sa)); +--@ \end{libverbatim} +mkCGetCPut :: (IsModule m c, Bits a sa) => m (CGetS n a sa, CPutS n a sa) +mkCGetCPut = + module + val :: Reg (Bit sa) <- mkConfigRegU + prs :: Reg Bool <- mkConfigReg False + crd :: Reg Bool <- mkConfigReg False + interface -- Pair + (interface CGetS + gvalue = val + gpresent = prs + gcredit b = crd := b + , + interface CPutS + pvalue v = val := v + ppresent p = prs := p + pcredit = crd + ) + +--@ The \te{CGet} and \te{CPut} interface are connectable. +--@ \begin{libverbatim} +--@ instance Connectable #(CGetS#(n, a, sa), CPutS#(n, a, sa)); +--@ \end{libverbatim} +instance Connectable (CGetS n a sa) (CPutS n a sa) + where + mkConnection :: (IsModule m c) => CGetS n a sa -> CPutS n a sa -> m Empty + mkConnection g p = + module + rules + {-# ASSERT no implicit conditions #-} + {-# ASSERT fire when enabled #-} + "moveCGetPut": + when True + ==> action + p.pvalue g.gvalue + p.ppresent g.gpresent + g.gcredit p.pcredit + +--@ \lineup +--@ \begin{libverbatim} +--@ instance Connectable #(CPutS#(n, a, sa), CGetS#(n, a, sa)); +--@ \end{libverbatim} +instance Connectable (CPutS n a sa) (CGetS n a sa) + where + mkConnection p g = mkConnection g p + +--@ The same idea may be extended to clients and servers. + +interface CClientS n a sa b sb = + request :: CGetS n a sa + response:: CPutS n b sb + +interface CServerS n a sa b sb = + request :: CPutS n a sa + response :: CGetS n b sb + +--@ \begin{libverbatim} +--@ typedef CClientS#(n, a, SizeOf#(a), b, SizeOf#(b)) +--@ CClient #(type n, type a, type b); +--@ typedef CServerS#(n, a, SizeOf#(a), b, SizeOf#(b)) +--@ CServer #(type n, type a, type b); +--@ \end{libverbatim} +type CClient n a b = CClientS n a (SizeOf a) b (SizeOf b) +type CServer n a b = CServerS n a (SizeOf a) b (SizeOf b) + +type CClientServer n a b = (CClient n a b, Server a b) +type ClientCServer n a b = (Client a b, CServer n a b) + +instance Connectable (CClientS n a sa b sb) + (CServerS n a sa b sb) + where + mkConnection :: (IsModule m c) => + (CClientS n a sa b sb) -> + (CServerS n a sa b sb) -> m Empty + mkConnection cc cs = + module + cc.request <-> cs.request + cc.response <-> cs.response + +instance Connectable (CServerS n a sa b sb) + (CClientS n a sa b sb) + where + mkConnection cs cc = mkConnection cc cs + +--@ \index{mkClientCServer@\te{mkClientCServer} (function)|textbf} +--@ \begin{libverbatim} +--@ module mkClientCServer(Tuple2 #(Client#(a, b), CServerS#(n, a, sa, b, sb))) +--@ provisos (Bits#(a, sa), Bits#(b, sb), Add#(1, k, n)); +--@ \end{libverbatim} +mkClientCServer :: (IsModule m c, Bits a sa, Bits b sb, Add 1 k n) => + m (Client a b, CServerS n a sa b sb) +mkClientCServer = + module + (g, cp) <- mkGetCPut + (cg, p) <- mkCGetPut + interface + (interface Client + request = g + response = p + , + interface CServerS + request = cp + response = cg + ) + +--@ \index{mkCClientServer@\te{mkCClientServer} (function)|textbf} +--@ \begin{libverbatim} +--@ module mkCClientServer(Tuple2 #(CClientS#(n, a, sa, b, sb), Server#(a, b))) +--@ provisos (Bits#(a, sa), Bits#(b, sb), Add#(1, k, n)); +--@ \end{libverbatim} +mkCClientServer :: (IsModule m c, Bits a sa, Bits b sb, Add 1 k n) => + m (CClientS n a sa b sb, Server a b) +mkCClientServer = + module + (g, cp) <- mkGetCPut + (cg, p) <- mkCGetPut + interface + (interface CClientS + request = cg + response = cp + , + interface Server + request = p + response = g + ) diff --git a/samples/Bluespec BH/COBS.bs b/samples/Bluespec BH/COBS.bs new file mode 100644 index 000000000..4a3e677c5 --- /dev/null +++ b/samples/Bluespec BH/COBS.bs @@ -0,0 +1,123 @@ +-- This file is copied from https://github.com/B-Lang-org/bsc-contrib +-- SPDX-License-Identifier: BSD-3-Clause + +package COBS where + +import FIFO +import GetPut +import Vector + +-- Implementation of Consistent Overhead Byte Stuffing (COBS) encoding of messages into a byte stream. +-- See https://en.wikipedia.org/wiki/Consistent_Overhead_Byte_Stuffing + +interface (COBSEncoder :: # -> *) n = + msg :: Put (UInt (TLog (TAdd 1 n)), Vector n (Bit 8)) + byte :: Get (Bit 8) + +mkCOBSEncoder :: (Log (TAdd 1 n) sizeWidth) => Module (COBSEncoder n) +mkCOBSEncoder = module + msgs :: FIFO (UInt sizeWidth, Vector n (Bit 8)) <- mkFIFO + bytes :: FIFO (Bit 8) <- mkFIFO + + let size :: UInt (TMax sizeWidth 8) = zeroExtend msgs.first.fst + let msg :: Vector n (Bit 8) = msgs.first.snd + + -- Index of the next byte to encode + i :: Reg (UInt (TMax sizeWidth 8)) <- mkReg 0 + -- Distance from i to the next zero / overhead / end of message byte + j :: Reg (UInt 8) <- mkReg 0 + -- Index of the next overhead byte to be inserted + nextOverhead :: Reg (Maybe (UInt (TMax sizeWidth 8))) <- mkReg $ Just 0 + + let byteI = select msg i + let foundNextZero = + j == (if nextOverhead == Just i then 0xfe else 0xff) || + i + zeroExtend j >= size || select msg (i + zeroExtend j) == 0 + + rules + "next_msg": when i >= size ==> do + -- $display "next_msg" + msgs.deq + bytes.enq 0 + i := 0 + j := 0 + nextOverhead := Just 0 + + "find_next_zero": when i < size && not foundNextZero ==> j := j + 1 + + "encode_overhead": when nextOverhead == Just i && i < size && foundNextZero ==> do + -- $display "encode_overhead %x" (j + 1) + bytes.enq $ pack (j + 1) + nextOverhead := if j == 0xfe then Just (i + 0xfe) else Nothing + j := 1 + + "encode_zero": when nextOverhead /= Just i && i < size && byteI == 0 && foundNextZero ==> do + -- $display "encode_zero %x" j + bytes.enq $ pack j + nextOverhead := if j == 0xfe then Just (i + 0xfe) else Nothing + i := i + 1 + j := 1 + + "encode_nonzero": when nextOverhead /= Just i && i < size && byteI /= 0 && foundNextZero ==> do + -- $display "encode_nonzero %x" byteI + bytes.enq byteI + i := i + 1 + j := if j > 1 || nextOverhead == Just (i + 1) then j - 1 else 1 -- Ensure that j > 0 if the next byte is not an overhead byte + + interface + msg = toPut msgs + byte = toGet bytes + + +interface (COBSDecoder :: # -> *) n = + msg :: Get (UInt (TLog (TAdd 1 n)), Vector n (Bit 8)) + byte :: Put (Bit 8) + +mkCOBSDecoder :: (Log (TAdd 1 n) sizeWidth) => Module (COBSDecoder n) +mkCOBSDecoder = module + msgs :: FIFO (UInt sizeWidth, Vector n (Bit 8)) <- mkFIFO + bytes :: FIFO (Bit 8) <- mkFIFO + + -- Index of the next result byte to be decoded + i :: Reg (UInt sizeWidth) <- mkReg 0 + -- Distance to the next zero / overhead / end of message byte + j :: Reg (UInt 8) <- mkReg 0 + -- Is the next zero / overhead / end of message byte an overhead byte? + isOverhead :: Reg Bool <- mkReg True + -- Vector of registers containing partially-decoded message + msg :: Vector n (Reg (Bit 8)) <- replicateM $ mkReg 0 + + rules + "next_msg": when bytes.first == 0 ==> do + -- $display "next_msg" + bytes.deq + msgs.enq (i, map readReg msg) + i := 0 + j := 0 + isOverhead := True + writeVReg msg $ replicate 0 + + "decode_overhead": when bytes.first /= 0 && j == 0 && isOverhead ==> do + -- $display "decode_overhead %x" bytes.first + j := unpack bytes.first - 1 + isOverhead := bytes.first == 0xff + bytes.deq + + "decode_zero": when bytes.first /= 0 && j == 0 && not isOverhead ==> do + -- $display "decode_zero %x" bytes.first + select msg i := 0 + i := i + 1 + j := if bytes.first == 0xff then 0xff else unpack bytes.first - 1 + isOverhead := bytes.first == 0xff + bytes.deq + + "decode_nonzero": when bytes.first /= 0 && j > 0 ==> do + -- $display "decode_nonzero %x" bytes.first + select msg i := bytes.first + i := i + 1 + j := j - 1 + bytes.deq + + interface + msg = toGet msgs + byte = toPut bytes diff --git a/samples/Bluespec BH/TL.bs b/samples/Bluespec BH/TL.bs new file mode 100644 index 000000000..45d0b0b42 --- /dev/null +++ b/samples/Bluespec BH/TL.bs @@ -0,0 +1,168 @@ +package TL (TL(..), sysTL) where + +import Vector + +interface TL = + ped_button_push :: Prelude.Action + + set_car_state_N :: Bool -> Prelude.Action {-# always_enabled #-} + set_car_state_S :: Bool -> Prelude.Action {-# always_enabled #-} + set_car_state_E :: Bool -> Prelude.Action {-# always_enabled #-} + set_car_state_W :: Bool -> Prelude.Action {-# always_enabled #-} + + lampRedNS :: Bool + lampAmberNS :: Bool + lampGreenNS :: Bool + + lampRedE :: Bool + lampAmberE :: Bool + lampGreenE :: Bool + + lampRedW :: Bool + lampAmberW :: Bool + lampGreenW :: Bool + + lampRedPed :: Bool + lampAmberPed :: Bool + lampGreenPed :: Bool + +data TLstates = AllRed + | GreenNS | AmberNS + | GreenE | AmberE + | GreenW | AmberW + | GreenPed | AmberPed + deriving (Eq, Bits) + +type Time32 = UInt 5 +type CtrSize = UInt 20 + +{-# properties sysTL = { verilog } #-} +sysTL :: Module TL +sysTL = + module + let allRedDelay :: Time32 = 2 + amberDelay :: Time32 = 4 + nsGreenDelay :: Time32 = 20 + ewGreenDelay :: Time32 = 10 + pedGreenDelay :: Time32 = 10 + pedAmberDelay :: Time32 = 6 + + clocks_per_sec :: CtrSize = 100 + + state :: Reg TLstates <- mkReg AllRed + next_green :: Reg TLstates <- mkReg GreenNS + secs :: Reg Time32 <- mkReg 0 + ped_button_pushed :: Reg Bool <- mkReg False + car_present_N :: Reg Bool <- mkReg True + car_present_S :: Reg Bool <- mkReg True + car_present_E :: Reg Bool <- mkReg True + car_present_W :: Reg Bool <- mkReg True + let car_present_NS :: Bool + car_present_NS = car_present_N || car_present_S + cycle_ctr :: Reg CtrSize <- mkReg 0 + + rules + "dec_cycle_ctr": when cycle_ctr /= 0 + ==> + cycle_ctr := cycle_ctr - 1 + + let low_priority_rule :: Rules + low_priority_rule = + rules + "inc_sec": when cycle_ctr == 0 + ==> + action + secs := secs + 1 + cycle_ctr := clocks_per_sec + + next_state :: TLstates -> Prelude.Action + next_state ns = action { state := ns; secs := 0; } + + green_seq :: TLstates -> TLstates + green_seq GreenNS = GreenE + green_seq GreenE = GreenW + green_seq GreenW = GreenNS + + car_present :: TLstates -> Bool + car_present GreenNS = car_present_NS + car_present GreenE = car_present_E + car_present GreenW = car_present_W + + make_from_green_rule :: TLstates -> Time32 -> Bool -> TLstates -> Rules + make_from_green_rule green_state delay car_is_present ns = + rules + "from_green": when (state == green_state) && + ((secs >= delay) || (not car_is_present)) + ==> + next_state ns + + make_from_amber_rule :: TLstates -> TLstates -> Rules + make_from_amber_rule amber_state ng = + rules + "from_amber": when (state == amber_state) && + (secs >= amberDelay) + ==> + action + next_state AllRed + next_green := ng + + hpr0 :: Rules + hpr0 = rules + "fromAllRed": when (state == AllRed) && + (secs >= allRedDelay) + ==> + if ped_button_pushed then + action + ped_button_pushed := False + next_state GreenPed + else if car_present next_green then + next_state next_green + else if car_present (green_seq next_green) then + next_state (green_seq next_green) + else if car_present (green_seq (green_seq next_green)) then + next_state (green_seq (green_seq next_green)) + else + noAction + + hpr1 :: Rules = make_from_green_rule GreenNS nsGreenDelay car_present_NS AmberNS + hpr2 :: Rules = make_from_amber_rule AmberNS GreenE + hpr3 :: Rules = make_from_green_rule GreenE ewGreenDelay car_present_E AmberE + hpr4 :: Rules = make_from_amber_rule AmberE GreenW + hpr5 :: Rules = make_from_green_rule GreenW ewGreenDelay car_present_W AmberW + hpr6 :: Rules = make_from_amber_rule AmberW GreenNS + + hprs :: Vector 7 Rules + hprs = Vector.cons hpr0 + (Vector.cons hpr1 + (Vector.cons hpr2 + (Vector.cons hpr3 + (Vector.cons hpr4 + (Vector.cons hpr5 + (Vector.cons hpr6 + Vector.nil)))))) + + high_priority_rules :: Rules + high_priority_rules = Vector.foldl1 rJoin hprs + + addRules (preempts high_priority_rules low_priority_rule) + + interface + ped_button_push = ped_button_pushed := True + + set_car_state_N b = car_present_N := b + set_car_state_S b = car_present_S := b + set_car_state_E b = car_present_E := b + set_car_state_W b = car_present_W := b + + lampRedNS = not (state == GreenNS || state == AmberNS) + lampAmberNS = state == AmberNS + lampGreenNS = state == GreenNS + lampRedE = not (state == GreenE || state == AmberE) + lampAmberE = state == AmberE + lampGreenE = state == GreenE + lampRedW = not (state == GreenW || state == AmberW) + lampAmberW = state == AmberW + lampGreenW = state == GreenW + lampRedPed = not (state == GreenPed || state == AmberPed) + lampAmberPed = state == AmberPed + lampGreenPed = state == GreenPed diff --git a/samples/Bluespec BH/TbTL.bs b/samples/Bluespec BH/TbTL.bs new file mode 100644 index 000000000..379fe0ee0 --- /dev/null +++ b/samples/Bluespec BH/TbTL.bs @@ -0,0 +1,122 @@ +package TbTL where + +import Vector + +import TL + + +interface Lamp = + changed :: Bool + show_offs :: Action + show_ons :: Action + reset :: Action + +mkLamp :: String -> Bool -> Module Lamp +mkLamp name lamp = + module + prev :: Reg Bool <- mkReg False + interface + changed = prev /= lamp + + show_offs = + if prev && not lamp then + $write (name + " off, ") + else + noAction + + show_ons = + if not prev && lamp then + $write (name + " on, ") + else + noAction + + reset = prev := lamp + + +{-# properties mkTest = { verilog } #-} +mkTest :: Module Empty +mkTest = + module + dut <- sysTL + + ctr :: Reg (Bit 16) <- mkReg 0 + + carN :: Reg Bool <- mkReg False + carS :: Reg Bool <- mkReg False + carE :: Reg Bool <- mkReg False + carW :: Reg Bool <- mkReg False + + lamp0 :: Lamp <- mkLamp "0: NS red " dut.lampRedNS + lamp1 :: Lamp <- mkLamp "1: NS amber" dut.lampAmberNS + lamp2 :: Lamp <- mkLamp "2: NS green" dut.lampGreenNS + lamp3 :: Lamp <- mkLamp "3: E red " dut.lampRedE + lamp4 :: Lamp <- mkLamp "4: E amber" dut.lampAmberE + lamp5 :: Lamp <- mkLamp "5: E green" dut.lampGreenE + lamp6 :: Lamp <- mkLamp "6: W red " dut.lampRedW + lamp7 :: Lamp <- mkLamp "7: W amber" dut.lampAmberW + lamp8 :: Lamp <- mkLamp "8: W green" dut.lampGreenW + + lamp9 :: Lamp <- mkLamp "9: Ped red " dut.lampRedPed + lamp10 :: Lamp <- mkLamp "10: Ped amber" dut.lampAmberPed + lamp11 :: Lamp <- mkLamp "11: Ped green" dut.lampGreenPed + + let lamps :: Vector 12 Lamp + lamps = Vector.cons lamp0 + (Vector.cons lamp1 + (Vector.cons lamp2 + (Vector.cons lamp3 + (Vector.cons lamp4 + (Vector.cons lamp5 + (Vector.cons lamp6 + (Vector.cons lamp7 + (Vector.cons lamp8 + (Vector.cons lamp9 + (Vector.cons lamp10 + (Vector.cons lamp11 nil))))))))))) + + rules + "start": when ctr == 0 ==> $dumpvars + + "detect_cars": when True + ==> + action + dut.set_car_state_N carN + dut.set_car_state_S carS + dut.set_car_state_E carE + dut.set_car_state_W carW + + "go": when True + ==> + action + ctr := (ctr + 1) + if ctr == 5000 then + carN := True + else if ctr == 6500 then + carN := False + else if ctr == 12000 then + dut.ped_button_push + else + noAction + + "stop": when ctr > 32768 ==> action + $display "TESTS FINISHED" + $finish 0 + + let do_offs l = l.show_offs + do_ons l = l.show_ons + do_reset l = l.reset + changed l = l.changed + + do_it f = Vector.mapM_ f lamps + + any_changes = Vector.any changed lamps + + rules + "show": when any_changes + ==> + action + do_it do_offs + do_it do_ons + do_it do_reset + $display "(at time %d)" ($time) + diff --git a/vendor/README.md b/vendor/README.md index 3834626fc..6f7742896 100644 --- a/vendor/README.md +++ b/vendor/README.md @@ -61,6 +61,7 @@ This is a list of grammars that Linguist selects to provide syntax highlighting - **BlitzBasic:** [textmate/blitzmax.tmbundle](https://github.com/textmate/blitzmax.tmbundle) - **BlitzMax:** [textmate/blitzmax.tmbundle](https://github.com/textmate/blitzmax.tmbundle) - **Bluespec:** [thotypous/sublime-bsv](https://github.com/thotypous/sublime-bsv) +- **Bluespec BH:** [atom-haskell/language-haskell](https://github.com/atom-haskell/language-haskell) - **Boo:** [drslump/sublime-boo](https://github.com/drslump/sublime-boo) - **Boogie:** [boogie-org/boogie-vscode](https://github.com/boogie-org/boogie-vscode) - **Brainfuck:** [Drako/SublimeBrainfuck](https://github.com/Drako/SublimeBrainfuck)