Add an entry for Bluespec's other syntax (#6476)
* Add support for the BH variant of Bluespec, alongside BSV * Renamed Bluespec BSV to Bluespec so it can be the head of the group * Generate a new unique ID for Bluespec BH * Update heuristics for .bs to include Bluespec BH * Add a fourth Bluespec BH sample * Add Bluespec BH to the grammar index --------- Co-authored-by: quark <quark@ubuntu2204.local>
This commit is contained in:
Julie Schwartz
GitHub
Родитель
e236e97e27
Коммит
e3020112db
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
)
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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)
|
||||
|
||||
|
|
@ -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)
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче