2012-08-09

for による組み合わせ回路

Verilog

昨日の回路を少し改善してみた。
functionとforを組み合わせることで超シンプルな回路として書けた。
wireで実装するよりシミュレーション速度も速い。(仕方ないか。。。)
合成後の速度は分からないが、、、

なぜ自分がわざわざこんなことをやっているかというと、JavaRockがスゲー！って思ったからです。
JavaRock

module modexp1 ( e ,n,m, r);
  input[511:0] e,n,m;
  output[511:0] r;

  assign r = modexp(e,n,m);

  function [511:0] modexp;
    input [511:0] e,n,m;
    integer i;
    reg   [1023:0] m1;
    reg   [1023:0] r1;

    begin
      for(i=0;i<512;i=i+1) begin
        if ( i == 0) begin
          m1 = m;
          r1 = (e[0]? m : 1) % n;
        end
        else begin
          m1 = twice_mod(m1,n);
          r1 = mult_non_zero(r1, e[i],m1) % n;
        end
      end
      modexp = r1;
    end
  endfunction

  function [1023:0] mult;
    input [511:0] m,n;
    mult = m * n;
  endfunction

  function [1023:0] mult_non_zero;
    input [511:0] r;
    input [1:0]   b;
    input [511:0] m;
    mult_non_zero = mult(r , (b == 1'b1 ? m : 1) );
  endfunction

  function [511:0] twice_mod;
    input [511:0] m, n;
    twice_mod = mult(m,m) % n;
  endfunction

endmodule

2012-08-08

組み合わせ回路に挑戦

Verilog

自作回路を作ってみた。
使用したのはicarus-verilog。

このicarusシミュレータはWindowsでも動作するのだが、ためしてみるとシミュレーションにめっちゃ時間が掛かる。

実装してみたのは冪剰余演算。512bit整数で3回ほど回すシミュレーションをしてみたのだが、、、

0.000u 0.062s 3:06.88 0.0%      0+0k 0+0io 1313pf+0w

つらい。。。

ソースコード：
https://github.com/dec9ue/verilog-study/blob/master/modexp1.v

2012-08-07

はてな記法

いままで使ってなかった。。。。
ちょっとはてな固有でやだけど楽にハイライトできるから使ってみるかな。。。

-- Simple example for Bang-Patterns leak
import Control.Monad
import Data.Foldable ( foldr' )
import System.IO

main :: IO ()
main = do
    result <- takeStat (return 100) 10000000
    print $ "result is " ++ show result

takeStat :: IO Int -> Int -> IO Int
takeStat io count =
    foldr' (liftM2 (+)) (return 0) $ replicate count io

でも未だGist埋め込みと迷っている。。。。

2012-08-04

世界一難しい数独＠Alloy(cont'd)

Alloy 数独

下記のような記事を見つけた。

星11個の数独の問題をAlloyで

なんと以前の記事を見てdisktnkさんという方が「遅すぎる」と検証してくださったようだ。。。

Lets's Compare!

ぼくの実行結果

Executing "Run run$1 for 13"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   77305 vars. 2201 primary vars. 146903 clauses. 3635ms.
   . found. Predicate is consistent. 82243ms.

disktnkさんの実行結果

Executing "Run game"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   2725 vars. 729 primary vars. 3303 clauses. 508ms.
   . found. Predicate is consistent. 2681ms.

なんだこの複雑度の差は、、、、述語数が30～40倍くらいちがう。僕の実行環境がNetbookでバカ遅いという状況をはるかに超えている。。。たしかに余計な述語が多かったんだよな。

精進します。

2012-07-31

入門 Verilog

Verilog

長らく堪えていたが、耐え切れなくなってポチってしまった。夏休みの積ん読リスト入り。

【送料無料】入門Verilog　HDL記述改訂 [ 小林優 ]

2012-07-03

世界一難しい数独、Alloyで解いてみたよ(RocketNews24から)

Alloy 数独

RocketNews24さんで本当に解ける人いるの？　フィンランド人数学者が作った “世界一難しい数独” が発表されるという記事があったんで以前のAlloyの記事で使ったモデルを流用して解いてみた。

about alloy
Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks.

結論：: 実は自分は数独のルールをわかっていなかった。

前回より工夫したところ：

数字をOne,Twoといったような表記ではなく、C01とか数字が入った表現にした。
数独って、9x9の枠の中でカブっちゃいけない、ってルールがあったんだ。。。。ということに気づいてルールを追加した。orz

では、以前のモデルを一部流用して解いてみます。

↓9x9のグルーピングを追加

abstract sig Index {}
sig Col extends Index {
  cell : Index -> Index
}
abstract sig G01,G02,G03 extends Col {}
one sig C01,C02,C03 extends G01{}
one sig C04,C05,C06 extends G02{}
one sig C07,C08,C09 extends G03{}

縦、横の重複禁止ルールの他に9x9の重複禁止ルールを追加

// 縦横の禁止
fact{
  all c:Col, r1,r2:Index | (r1=r2)or(not(cell[c,r1]=cell[c,r2]))
}
fact{
  all c1,c2:Col, r:Index | (c1=c2)or(not(cell[c1,r]=cell[c2,r]))
}
// 9x9の重複禁止
fact{
  all c1,c2:G01, r1,r2:G01 | (r1=r2 and c1=c2)or(not(cell[c1,r1]=cell[c2,r2]))
}
fact{
  all c1,c2:G01, r1,r2:G02 | (r1=r2 and c1=c2)or(not(cell[c1,r1]=cell[c2,r2]))
}
:

実際に解かせてみると。。。。

Executing "Run run$1 for 13"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   77305 vars. 2201 primary vars. 146903 clauses. 3635ms.
   . found. Predicate is consistent. 82243ms.

82秒。

チェック結果掲載できてませんが、解答ページを見てみるとちゃんとあっていました。

f:id:dec9ue:20120704182506p:plain

ちなみに、標準的な問題を解かせてみると。。。

Executing "Run run$1 for 13"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   77309 vars. 2201 primary vars. 146933 clauses. 3712ms.
   . found. Predicate is consistent. 49608ms.

50秒。

つまり、世界一難しい問題は、SATソルバからみると60～70%程度難しい問題だってことがわかりました。

いずれにせよ、Alloyって戦略を明示しなくてもいいのにコレぐらいの時間で数独が解けてしまいます。数独はAlloyがとても良くハマる問題だといえるのではないかと思います。

コードはこちら

追記： 2012/07/04 回答の図をアップしました。あと、Alloyの説明をちょっと追加。

【送料無料】抽象によるソフトウェア設計 ALLOYではじめる形式手法 / ダニエル・ジャクソン【...

2012-06-25

Control.DeepSeqを使って正格評価(訂正版)

Haskell

何が酷いって、記事を見なおしてみたらfoldrとfoldlのロジックを間違えてる。コレは死ねる。。。ただ、Bangについてはそれでもちょっと怪しいので訂正版の記事を作り直したいと思います。

古い記事は自戒の意味も込めて残しておきます。(なんの意味があるのかは不明)

モンテカルロ法で円周率を計算するために多数のIOから取り出した結果の集計を行おうとした。

しかし未評価thunkによるメモリオーバーフローが発生し、インスタンス数を増やせなかった。途中でわざとprintを行なって未評価thunkを潰してメモリリークを防いでいたのだがもちろんこれは本質的な解決ではない。

また、Bang-Patternを使用して未評価thunkを潰そうとしたが、どうもthunkが潰れてくれない。

調べてみたところ、厳密な正格評価にはControl.DeepSeqが使用できることがわかったので試して見ることにした。

まず、リークを起こすコードの説明から。

main :: IO ()
main = do
    (count,total)  Int -> IO Stat
takeStat func count =
    foldLN1 sum_stat (liftM point_to_stat func) count (0,0)

foldLN1 :: (a->b->a) -> IO b -> Int -> a -> IO a
foldLN1 folder m count init =
    let foldLN_sub folder m count v = if count == 0
        then v
        else let v' = unsafePerformIO m
              in foldLN_sub folder m (count -1) $! folder v v'
    in return $ foldLN_sub folder m count init

だいぶ端折っているが、foldLN1という関数で$!の形でBang-Patternを使用している。にもかかわらず、実行するとメモリオーバーフローで落ちる。(どうやら、folder関数のthunkが潰れ切らないらしい) そこで、DeepSeqを使用したコードに修正する。

foldLN1 :: (NFData a) => (a->b->a) -> IO b -> Int -> a -> IO a
foldLN1 folder m count init =
    let foldLN_sub folder m count v = if count == 0
        then v
        else let v' = unsafePerformIO m
              in foldLN_sub folder m (count -1) $!! folder v v'
    in return $ foldLN_sub folder m count init

NFDataクラスはDeepSeqモジュールの正格評価を適用できるデータのクラス。$!!はBang-Patternsにおける$!に相当する。引数を(Bang PatternsにおけるWHNFではなく、)値になるまで評価する。

そもそも、unsafePerformIO使っているし、foldを自分で書くクソダサさと、無茶しまくっている、、、でも、確かにコレで落ちない。

ちなみに、DeepSeqを使用しなくても下記のように時々thunkを潰すような処理を入れてあげると上手く回る。

foldLN2 :: (Show a) =>(a->b->a) -> IO b -> Int -> a -> IO a
foldLN2 folder m count init =
    let foldLN_sub folder m count v = if count == 0
        then v
        else let v' = unsafePerformIO $ do
                 when (count `mod` 100000 == 0) $ print_stat v count
                 m
              in foldLN_sub folder m (count -1) $! folder v v'
    in return $ foldLN_sub folder m count init

コード： Recursion2.hs

参考：

【まとめ】Haskellでの正格評価とWHNF: http://kamonama.blogspot.jp/2011/04/haskellwhnf.html
shelarcyさんの説明: http://www.sampou.org/cgi-bin/haskell.cgi?shelarcy

補足：

$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.4.1
$ ghc -O Recursion.hs
[1 of 1] Compiling Main             ( Recursion.hs, Recursion.o )
Linking Recursion.exe ...