ChibiOS/RT上で動作するアプリケーションをVeriFastで検証します。
以下をインストールしてください。
この時、各ツールにはPATHを通してください。また、以下のcygwinパッケージをインストールしてください。
- cmake
- gcc-core (5.3.0)
- libusb1.0-devel
- make
cygwinターミナルを開き、stlinkをダウンロードしてビルドしてください。
$ git clone https://github.com/texane/stlink.git
$ (cd stlink && make)
$ (cd stlink/build/Release && make install)
$ cp /usr/local/lib/cygstlink-shared-1.dll /usr/local/bin/
VeriFastの最新版をダウンロードし、展開して verifast-XXXXXXX\bin
ディレクトリにPATHを通してください。
cygwinターミナルを開き、本ソースコードをダウンロードして、ツールチェーンを設定してください。
$ git clone https://github.com/fpiot/chibios-verifast.git
cygwinターミナルを開き、ソースコードをビルドしてください。
$ cd chibios-verifast/verifast_demo/STM32/RT-STM32F091RC-NUCLEO
$ make
ボードとWindows PCをUSBケーブルで接続した後、cygwinターミナルを開き、ファームウェアを書き込んでください。
$ cd chibios-verifast/verifast_demo/STM32/RT-STM32F091RC-NUCLEO
$ make flash
TeraTermを使ってシリアルポート"STMicroelectronics STLink Virtual COM Port"をボーレート9600で開いた後、ボードのUSER
スイッチを押下してください。以下のようなログが表示されます。
*** ChibiOS/RT test suite
***
*** Kernel: 3.1.5
*** Compiled: Jan 15 2017 - 20:38:01
*** Compiler: GCC 4.8.4 20140725 (release) [ARM/embedded-4_8-branch revision 213147]
*** Architecture: ARMv6-M
*** Core Variant: Cortex-M0
*** Port Info: Preemption through NMI
*** Platform: STM32F091xC Entry Level Access Line devices
*** Test Board: STMicroelectronics NUCLEO-F091RC
--snip--
VeriFastでソースコードを検証するには、cygwinターミナルを開き、以下のようにしてVeriFast IDEを起動してください。
$ cd chibios-verifast/verifast_demo/STM32/RT-STM32F091RC-NUCLEO
$ make vfide