BusMOP Syntax

From FSL

Contents 1 Modifiers 2 Language Syntax 3 Supported Logics 4 Examples

[edit] 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.

[edit] 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".

[edit] Supported Logics

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

• FSM Syntax -- Finite State Machine Descriptions
• ERE Syntax -- Extended Regular Expressions
• PTLTL Syntax -- Past Time Linear Temporal Logic

[edit] 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";
}