BusMOP Syntax

From FSL
Jump to: navigation, search

Contents

Modifiers

BusMOP has no modifiers at this time. Currently we support only the standard PCI bus, possible modifiers could specify for which bus to generate code.

Language Syntax

We use conventional VHDL syntax with some special wrappers:

<LANGUAGE Declarations>  ::= "declarations {" <VHDL Declarations> "}"
<LANGUAGE Parameters> ::= //BusMOP specifications are not parametric
<LANGUAGE Statement> ::= <VHDL statements>
<LANGUAGE Other> ::= <BusMOP Event Syntax>
<BusMOP Event Syntax> ::= "event" <ID> ":" <Expression>
<Expression> ::= <MemoryOrIO> <ReadOrWrite> "address" "="
<ArithmeticOp> "value" ["not"] "in"
<Range> ["{" <Action> "}"]
| <MemoryOrIO> <ReadOrWrite> "address" "in"
<Range> ["{" <Action> "}"]
| "interrupt" ["{" <Action> "}"]
<MemoryOrIO> ::= "memory" | "io"
<ReadOrWrite> ::= "read" | "write"
<Action> ::= <Arbitrary VHDL code>
<Range> ::= <ArithmeticOp> ["," <ArithmeticOp>]
<ArithmeticOp> ::= <Number> | <ID>
| <ArithmeticOp> "+" <ArithmeticOp>
| <ArithmeticOp> "&" <ArithmeticOp>
| <ArithmeticOp> "-" <ArithmeticOp>
| "(" <ArithmeticOP> ")"
<Number> ::= <VHDL number or bitstring>
<ID> ::= <Letter> {<LetterOrDigit>}
<LetterOrDigit> ::= <Capital or lower case letter> | <Digit>

Address ranges can be used only when no values are specified, because alignment must be known if values are checked, and the alignment of a range of addresses would be undefined. We allow range of addresses, by themselves, because some properties may wish to have an event such as "memory access anywhere in a buffer".

Supported Logics

Note that, currently, BusMOP only supports the following logics:

Examples

The following example ensures that a safe speed is used for conversion by the ADC board we used for testing (i.e., that the time specified is long enough for the computation to reach a steady state):

declarations { 
signal clkSrc : STD_LOGIC_VECTOR(15 downto 0) := 0;
signal src : STD_LOGIC_VECTOR(15 downto 0) := 0;
}
 
event divrBad: memory write address = base1 + X"228"
dbyte value in 0,44
event divrGood: memory write address = base1 + X"228"
dbyte value in 45,65535
event countEnable : memory write address = base1 + X"220"
dbyte value in "---------------1"
event clkSrcSet : memory write address in base1 + X"300"
{ clkSrc <= value; }
event srcSet : memory write address in base1 + X"220"
{ src <= value; }
 
ere : (divrBad (clkSrcSet + srcSet)* countEnable)*
 
@validation {
if (clkSrc(2 downto 1) = "01") and (src(2 downto 1) = "00") then
mem_reg <= '1';
address_reg <= base1 + X"228";
--set cntr_divr2 to 45
value_reg(15 downto 0) <= X"2D";
enable_reg <= "0011";
end if;
}

The following example ensures that the ADC board is not disabled while it is in the process of converting from analog to digital:

declarations {
signal cntrlCurrent : STD_LOGIC_VECTOR(15 downto 0) := X"0000";
signal cntrlOld : STD_LOGIC_VECTOR(15 downto 0) := X"0000";
}
 
event countEnable : memory write address = base1 + X"220"
dbyte value in "---------------1"
{
cntrlOld <= cntlCurrent;
cntrlCurrent <= value;
}
event countDisable : memory write address = base1 + X"220"
dbyte value in "---------------0"
{
cntrlOld <= cntlCurrent;
cntrlCurrent <= value;
}
event clkSrc2Good : memory write address = base1 + X"300"
dbyte value in "-------------01-"
event clkSrc2Bad : memory write address = base1 + X"300"
dbyte value not in "-------------01-"
event adcEnable : memory write address = base1 + X"300"
dbyte value in "---------------1"
event adcDisable : memory write address = base1 + X"300"
dbyte value in "---------------0"
 
ptltl : ( ((not adcDisable) S adcEnable) and
((not clkSrc2Bad) S clkSrc2Good) )
implies
((not countDisable) S countEnable)
 
@violation {
mem_reg <= '1';
address_reg <= base1 + X"220";
-- roll back to the previous cntr_cntrl2 value
value_reg(15 downto 0) <= cntrlOld;
cntrlCurrent <= cntrlOld;
enable_reg <= "0011";
}
Personal tools
Namespaces

Variants
Actions
Navigation