断言

module taa ();
reg clk1, clk2, clk3;
reg a,b,c,d,e,f,g,h;
initial begin
    fork
        begin
            clk1=0;
            forever #2 clk1=~clk1;
        end
        begin
            clk2=0;
            forever #3 clk2=~clk2;
        end
        begin
            clk3=0;
            forever #5 clk3=~clk3;
        end
    join
    end

    property p1;
        @(posedge clk1) disable iff(a) $rose(b) |-> c[=2] ##1 d[=2] ##1 !d;
    endproperty
    a1: assert property(p1);

    property p2;
        @(posedge clk1) disable iff(a) $rose(b) |=> c[=2] ##1 d[=2] ##1 !d;
    endproperty
    a2: assert property(p2);

    let p3=(d && b && c);
    property p4;
        @(posedge clk1) disable iff(a) p3 |-> e[=2] ##1 f[=2] ##1 !g;
    endproperty
    a4: assert property(p4);

    property p5;
        @(posedge clk1) disable iff(a) p3 |-> not(e[=2] ##1 f[=2] ##1 !g);
    endproperty
    a5: assert property(p5);

    property p6;
        @(posedge clk1) 
        disable iff(a) 
        $rose(b) |-> (c[=2] ##1 d[=2] ##1 !d) and ((e ##1 f) or (g ##1 h));
    endproperty
    a6: assert property(p6);

    property p7;
        @(posedge clk1) 
        disable iff(a) 
        $rose(b) |-> (c[=2] ##1 d[=2] ##1 !d) intersect ((e ##1 f) or (g ##1 h));
    endproperty
    a7: assert property(p7);

    property p9(x,y);
        x |-> ##1 x && y;
    endproperty

    property p8;
        @(posedge clk1) 
            a ##1 (b||c)[->1] |->
                if(d) (##1 e |-> f)
                else p9(g ,h);
        endproperty
    a8: assert property(p8);

//    property p10(p);
//        p and (1'b1 |=> p10(p));
//    endproperty
//    a10: assert property(p10(h));

    property p10;
        @(posedge clk1) a ##1 @(posedge clk2) b ;
    endproperty
    a10: assert property(p10);  

    property p11;
        @(posedge clk1) a |=> @(posedge clk2) b ;
    endproperty
    a11: assert property(p11);

    property p12;
        @(posedge clk1) a |-> @(posedge clk2) b ##1 @(posedge clk3) c; //illegal but can pass
        //@(posedge clk1) a |-> @(posedge clk1) b ##1 @(posedge clk2) c;
    endproperty
    a12: assert property(p12);

    //a13: assume property @(clk1) b dist{0:=40, 1:=60};
    //property proto
    //    @(posedge clk1) b |-> b[*1:$] ##0 c;
    //endproperty

    a15: assume property(p1);
    a14: cover property(p1);

    initial begin
        forever #1 {a,b,c,d,e,f,g,h}=$urandom;
    end

    initial begin
        #10 assign a=1;
        #20 assign a=0;
        #10000 $finish;
    end
endmodule

　　

说明

p1，$rose(b) |-> c[=2] ##1 d[=2] ##1 !d    |||||||||a为0表示生效，在b的上升沿出现后，同样的时钟周期开始计算，出现两个c以后，等1时钟周期，出现两个d以后，等一个时钟周期d为0.

p2， |=>表示下一周期开始计算。

p4，进行了嵌套

p5，进行了取反

p6，p7的and、or、intersect

p8，的分支if else

p10，p11，p12的跨时钟、a为1，

p10 @(posedge clk1) a ##1 @(posedge clk2) b，在clk1位上升沿判断a为1后，经过不到1个时间单位，clk2上升沿后判断b为1，成立》》？

p11和p10结果相同

p12的，，，在clk1位上升沿判断a为1后，经过不到1个时间单位，clk2上升沿后判断b为1，经过不到（或者等于）1个时间单位，clk3上升沿后判断c为1，成立。

 和理论的时钟偏移，然后过渡到下一个时钟单位，经过一个周期的结果输出，有出入