Behavior-Interaction-Priority (BIP) is a layered embedded system design and verification framework that provides separation of functionality, synchronization, and priority concerns to simplify system design and to establish correctness by construction. BIP framework comes with a runtime engine and a suite of verification tools that use D-Finder and NuSMV as model checkers.

In this paper, we provide a method and a supporting tool that take a BIP system and a set of invariants and compute a reduced sequential circuit with a system-specific scheduler and a designated output that is true when the invariants hold. Our method uses ABC, a sequential circuit synthesis and verification framework, to (1) generate an efficient circuit implementation of the system that can be readily translated into FPGA or ASIC implementations, and to (2) verify the system and debug it in case a counterexample is found. Moreover, we generate a concurrent C implementation of the circuit that can be directly used for runtime verification.

We evaluated our method with two benchmark systems, and our results show that, compared to existing techniques, our method is faster and scales to larger sizes.

The implementation of the translation is available in the online bip-to-abc.jar file.

The interface to ABC is available online SA.

The traffic example is also available online traffic.bip.

java -jar bip-to-abc.jar [options] input.bip output.abc [property.txt]

where:

    input.bip    = input BIP file name (required)
    ouput.abc    = ABC file name to be generated (required)
    property.txt = Pre and Post condition written in two different lines (optional)

and options are:

    -?                prints usage to stdout; exits (optional)  
    -emulator <s>     Generate emulation code output.abc.cpp (optional)  
                          - guide.txt: indices of interactions assigned to selector (e.g., -emulator=guide.txt) 
                          - integer <= 0: infinite exection (e.g., -emulator=0)
                          - integer > 0: number of cycles to be executed (e.g., -emulator=30)
    -h                prints usage to stdout; exits (optional) 
    -help             displays verbose help information (optional)
    -initialize-vars  Initialize free variables (optional)
    -optimized        Generate one cycle-based code (optional)
    -version          displays command's version (optional)

java -jar bip-to-abc.jar -optimized -initialize-vars -emulator=guide input.bip output.abc property.txt
java -jar bip-to-abc.jar -o -i -e=guide input.bip output.abc property.txt
java -jar bip-to-abc.jar -o -i -e=0 input.bip output.abc property.txt
java -jar bip-to-abc.jar -o -i -e=30 input.bip output.abc property.txt
java -jar bip-to-abc.jar -o -e=guide input.bip output.abc

Option tags are not case sensitive, and may be truncated as long as they remain unambiguous. Option tags must be separated from their corresponding values by whitespace, or by an equal sign. Boolean options (options that require no associated value) may be specified alone (=true), or as 'tag=value' where value is 'true' or 'false'.