标签：断言 ## 29 assert endproperty posedge clk1 property

断言

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，成立。

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

标签：断言,##,29,assert,endproperty,posedge,clk1,property
来源： https://www.cnblogs.com/bai2022/p/15759344.html

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。