2014年11月20日木曜日

isimをcliで呼んでみた

ISEについているisimは実はcommand line interfaceがある。これを使ってguiを使わずにシミュレーションしようぜっていう話。ISim User GuideとかISim In-Depth Tutorialとかを参考にしている。

isimはGUI modeとCLI modeがあって、CLI modeだとtclの対話環境があってそれを使う。走らせるtestが事前にあるならbatch scriptを走らせることもできる。そうじゃなくても短ければ標準入力からpipeとかで与えると動く。何も考えなければ

 
  run all
とか
 
  run 10ms
とか与えればよい。終わったらexitで抜けられる。

これだと波形が見れないが、debugするのであれば波形を見たい。vcdファイルを吐けば良いが、isimのvcd出力はverilog用っぽくて情報が欠けているようだ。そこでisimの波形のフォーマット(?)のwcfgとwdbを使うと良い。

こういうtclのbatchを書いて、(fadd_sim.tclとする)

  $ ./fadd_sim -wdb fadd.wdb -tclbatch fadd_sim.tcl
のようなことをするとfadd_sim.wcfgとfadd.wdbが生成される。波形を見たいときはこんな感じで見ることができる。

  $ isimgui -open fadd.wdb -view fadd_sim.wcfg

isimで自動テストを回してみた

ハードウェアでも自動テストをやると捗るので自動テストを回してみた。自動テストをやるのにいちいち波形を見る方法は取りづらいので、想定される出力と一致するかのみを判定して、一致しなければsimulationを止める方法で正誤判定を行った。まず、isimの実行ファイルをcliで作るのには依存関係を記述した,prjファイルが必要である。

下記のようなprjファイル(fadd_sim.prjとする)を作る。この例だと、fadd_simを作るのにwork libraryのfadd.vhd,fadd_sim.vhd,fadd_stage1.vhd,fadd_stage2.vhd,fadd_stage3.vhd,right_shift.vhd,ZLC.vhdが必要だという意味である。

次にMakefileを書く。これは普通に書けば良い。


fadd_isim: fadd_sim.prj fadd.vhd fadd_sim.vhd fadd_stage1.vhd fadd_stage2.vhd fadd_stage3.vhd right_shift.vhd ZLC.vhd
        fuse -incremental -prj $< -o $@ fadd_sim
test: fadd_isim
        ./run.sh

最後にtestを回す次のようなスクリプトを書く(run.shとする)。

これを実行すると次のようになる。

[==========] Running 2 tests
[ RUN      ] fadd_isim
[  PASSED  ] fadd_isim
[ RUN      ] i2f_isim
[  PASSED  ] i2f_isim
[==========]
[  PASSED  ] 2 tests.

2014年9月22日月曜日

sizeがよくわかんないarrayの受け渡しをやってみた

Cで


void foo(int* xs,int length)
みたいなことやってる関数をC++11のstd::arrayを使って書き換えようとしたらどうなるのかと思ってやってみた.

とりあえず

  • まあtemplate使えばできるね
  • 呼び出し側もstd::arrayに変更する必要がある.
位のことは気がついた.

2014年9月9日火曜日

jenkinsをpowerpcのgentooにinstallした.

jenkinsをpowerpcのgentooにinstallしました.emergeだけで済まなかったので書きます.ibmのjreをinstallするところまではemergeの言うとおりにやっていればいいので省きます.まず,http://mirrors.jenkins-ci.org/war/latest/jenkins.warからjenkins.warをダウンロードします.これをとりあえずjava -jar jenkins.warで実行します.jreが正しくinstallされていればこれで127.0.0.1:8080につなぐとjenkinsのページにアクセスできます.

次にInstall Jenkins as a Unix daemonのshell scriptの部分のshell scriptを適当にpathの通っている場所に置きます.最後に

# useradd jenkins -m -U
# mkdir /usr/share/java/jenkins
# mv jenkins.war /usr/share/java/jenkins
# mkdir -p /var/lib/jenkins
# mv .jenkins/* /var/lib/jenkins
# chown jenkins:jenkins -R /var/lib/jenkins
# mkdir -p /var/log/jenkins
# chown jenkins:jenkins /var/log/jenkins
で終わりです.起動は作ったscriptをroot権限で実行すればいいです.停止はそれっぽいprocessをkill止めるしかないです.

これでjenkinsのinstallは終わりです.自動で起動したりとかproxyとかで80番ポートに飛ばしたりできます.

2014年8月17日日曜日

mac mini(初代)にgentoo linuxをinstallしてみた

家にあるmac miniをlinuxマシンにしようということでgentooを入れてみた.debianでも良かったがローリング・リリースが良かったのでgentooにした.

基本的にGentoo Linux PPC ハンドブックを読めばなんとかなるが時々原文と比べて古いので原文も参照した.実は今までpowerpcにlinuxをinstallしたことはなかったので色々と手こずった.

詰まったのは主にboot周り.yabootconfigで設定したままではbootできなかった. まずdriveが読めなかった.

filesystem unknown or corrupted
というerrorが出た.http://archives.gentoo.org/gentoo-ppc-user/msg_765cf3c4fac4c22c5130ae98cc4630b6.xmlなどを参考にして
device=/pci@f4000000/ata-6@d/disk@0:
device=hd:
に変更したところまずyabootでデバイスが読めるようになった.

が今度はhda3がないと言われた.kernel optionでPATA_MACIOを使うとhdaではなくsdaになるらしい.(というか今時ideがhdaになるほうのドライバを使っているlive cdにびっくりしたが)おとなしくrootをsda3に変更したところ無事bootできるようになりました.

2014年7月16日水曜日

lpr in ECCS2012

MacOSXはUnixなのでlprは動くと思うが,ECCS2012のシステムでlprをつかって印刷したという話を聞いたことがなかったのでやってみた.

PostScript

まずはPostScriptだろうと思ってPostScriptを印刷してみた.日本語が混ざっているtexをplatexでdviにして,dvipsでPostScriptを生成した.無事MainMonoと思われるプリンタに送られたようだが,日本語の部分が文字化けしてさっぱり読めない.多分フォントがないのが原因だと思われる.

PDF

フォントがないならと思って今度はPDFに変換して印刷してみた.同様のファイルをdvipdfmxを使ってPDFに変換してみた.今度は普通に印刷できた.previewでも印刷してみたが差はない.さすがPDF.

最後に

ECCS2012の環境でlprで印刷しようと思う人はそもそもまれだろうが,まあやっぱりちゃんと動くのでパイプをつないで直接印刷したかったりしたら便利なのではないだろうか.(註:今回は標準入力からの印刷ではなくファイルからの印刷しか試していません.)

2014年7月7日月曜日

短冊shell芸

七夕なのでshell one linerで短冊を作ってみた.

echo "sedですね" | sed -e 's/\(.\)/┃\1┃\n/g;s/^/┏┷┓\n┃ ┃\n/;s/$/┃ ┃\n┗━┛/' 
まあ単発ネタなので大して面白くもない.

2014年1月24日金曜日

arch linuxでcrosstool-ngを使ってppc64bitのクロスコンパイラを作る

yaourtが入っていることを前提とする.

yaourt -S crosstool-ng
mkdir -p ~/cross/bin
cd ~/cross/bin
ct-ng list-samples
ct-ng <選んだsample>
ct-ng menuconfig

ここで設定するわけだが要点は以下の様になる

  • いらないものは削る
    • gcjとか普通のひとはいらない.
  • ライブラリはできるだけ新しいものを選択する.
    • バージョンが古いとarchのgccではあたらしすぎてコンパイルできなかったりする
  • C-Libraryの Force unwind supportはcheckする
    • しなかったらコンパイルエラーがでた
  • gdbでpython scriptingをenableにしない
    • archのpythonは3系だが,python2系を前提としているらしく,どうせgdbでpythonを使わないので面倒だから無効にしてしまった

次に

ct-ng build

でコンパイルを始めるが,make4.0だとあたらしすぎてglibcのコンパイルが通らない.そこで http://lfsbookja.sourceforge.jp/svn.ja/chapter06/glibc.html にもあるように

sed -r -i 's/(3..89..)/\1 | 4.*/' configure

でglibcのconfigureを変更する必要がある.一回ダウンロードが済んだあとで止めて修正すればいいはず.

これで

ct-ng build

でコンパイルが通って~/xtools以下にそれらしきものが入った.

2014年1月15日水曜日

bashでtestを使うと遅いよ

bashでは


if [ $a -eq 0 ] ...

と書く代わりに


if [[ $a -eq 0 ]] ...

と書ける。test([,])は外部コマンドだから評価のときに毎回forkして遅いような気がする。一方[[,]]は内部コマンドだからforkしなくて速いのではないかと思ったのでベンチマークを取ってみた。

ベンチマーク


for a in $(seq 1 100000) ; do [ 0 -eq 100 ] ; done
for a in $(seq 1 100000) ; do [[ 0 -eq 100 ]] ; done

結果

real    0m0.535s
user    0m0.517s
sys     0m0.017s

real    0m0.353s
user    0m0.347s
sys     0m0.007s

予想通り[[,]]の方がまあまあ速かった。因みに[[,]]の方では正規表現マッチなど機能が追加されている。互換性を追求するなどの理由がない限り[[,]]を使った方が良さそう。

2014年1月2日木曜日

ひとり正月Coq勉強会

以前も若干勝手にCoqを勉強したことはありましたが,その時は直感主義論理の簡単な証明を書いたくらいで時間がなくなってしまいました.今回は非常に簡単ながら証明駆動っぽい開発をやってみました.なお,Coqはほぼ書いたことがないので証明とかアレかもしれない.

  • やってみたかったこと : 非常に簡単な証明駆動開発
  • 題材 : cons
    • sortとかマジな証明だとちゃんと小1時間で終わらなくなってしまうので,本当に簡単なものをやってみた

consしたら

  • head $ cons x xs = x になる
  • tail $ cons x xs = xs になる

の2つの性質が満たされる.ということで命題を書いてみた

Definition is_head_x (A : Type)( x :option A) ( xs : list A) : Prop := (head xs) = x.
Definition is_tail_ys (A : Type)( ys :list A) ( xs : list A) : Prop := (tail xs) = ys.

そして consを定義

Definition cons ( A : Type) ( x : A) ( xs : list A) : list A := cons x xs.

証明はdefinitionより明らかなのでunfoldするだけで,わざわざ書く価値もないが,とりあえず.適当に証明して.

Extraction Language Haskell.
Extraction cons.

でHaskellのconsを適用するだけの関数が出てきた.

非常に簡単すぎてこれでいいのかよくわからないが,多分証明駆動開発の最も短い実例になったと思う.