pslいじってみた
今までいじってなかったアサーション検証。懐疑的というわけではないけどめんっどくっせー、とか思っていた。折角fibやってたので、無意味なfib回路でもこさえて、それにアサーション振り掛けてみる。ソッコう書き。
module fib ( clk, rst, start, in, busy, ack, out ); input clk, rst; // clk and reset signal input start; // kick signal input [ 4:0] in; // parameter for function output busy; // busy signal output ack; // redundant (for psl check purpose) output [21:0] out; // resulting value (valid if ack is true) reg [21:0] out; reg [21:0] prev; // previous value (for fib) reg [ 4:0] counter; reg start_r, start_2r; reg busy_r, busy_2r; wire continue; wire start_pulse; // make start signal always @(posedge clk or negedge rst) begin if (!rst) begin start_r <= 1'b0; start_2r <= 1'b0; end else begin start_r <= start; start_2r <= start_r; end end assign start_pulse = !start_2r & start_r; always @(posedge clk or negedge rst) begin if (!rst) counter <= 5'b00000; else if (start_pulse) counter <= in; else if (continue) counter <= counter - 1'b1; else counter <= counter; end assign continue = (counter > 5'b00000); // main logic for fibonatti always @(posedge clk or negedge rst) begin if (!rst) out <= 22'h00000; else if (start_pulse) out <= 22'h00000; else if (continue) out <= out + prev; else out <= out; end always @(posedge clk or negedge rst) begin if (!rst) prev <= 22'h00000; else if (start_pulse) prev <= 22'h00001; else if (continue) prev <= out; else prev <= prev; end // control signals always @(posedge clk or negedge rst) begin if (!rst) begin busy_r <= 1'b0; busy_2r <= 1'b0; end else begin busy_r <= continue; busy_2r <= busy; end end assign ack = !busy_r & busy_2r; assign busy = busy_r; endmodule
一応正しく動いているっぽい。
PSL入れる
PSLは基本的にはコメント部の頭に 'psl'のキーワードを書いて構文を書き下す。Verilog-flavourとVHDL-flavourがあるんだけど、どうせ仕事では verilogしか使わないので VHDLは頭からパージしておくことにする*1。
// psl ASERTNAME : assert // always (rst & (en_a != en_b)) @(posedge clk);
のように入れておいて、clk立ち上がりでこの条件にあっていないとエラーが出る。まあ基本的には Cとかの assert()と同じなんだけど、ちょっと違うのが時間の概念が入れれること
// psl ASSERTNAME : assert // always (req -> next ack) @(posedge clk);
のようにある信号(req)の次のサイクルでackが上がる、のような記述ができる。で、まあ後は普通にスティミラス流して、、、というほかに形式検証にも利用できる。めっさ重いが。
さて今回は、continue信号の立下りで作っているのを間違えてackがおかしなタイミングで出るようにして、遊んでみる。
というか「後でやる」というか明日から実家帰ってしまうので、「だいぶ後でやる」
