Implication |-> và |=>: mỗi tick một attempt

`timescale 1ns/1ps// Six ticks. Generic a&&!b at2/3, bnevertrue ->failures3/4(mask24),4vacuouspasses. Separate false|->false passes6.module tb_implication_attempts; bit clk=0,a=0,b=0; int tag=1,samples=0,passes=0,failures=0,failure_mask=0,vacuous_pass=0,vacuous_fail=0; always #5 clk=~clk; always @(posedge clk)samples++; A_step:assert property(@(posedge clk)(a&&!b)|=>(a&&b))passes++;else begin failures++;failure_mask|=1<<tag;end A_vacuous:assert property(@(posedge clk)1'b0|->1'b0)vacuous_pass++;else vacuous_fail++; initial begin  for(int cycle=1;cycle<=6;cycle++)begin   if(cycle>1)@(negedge clk);   tag=cycle;a=(cycle==2||cycle==3);b=0;  end  @(negedge clk);  if($time!=60||samples!=6||passes!=4||failures!=2||failure_mask!=24||vacuous_pass!=6||vacuous_fail!=0)$fatal(1,"implication attempt identity oracle");  $display("IMPLICATION ATTEMPT CHECK samples=6 passes=4 failures=2 failure_mask=24 vacuous_pass=6 time_ns=%0d",$time);$finish; endendmodule

`timescale 1ns/1ps// Expected before execution: 10 samples, two antecedent endpoints (2/6).// gnt at2/7: overlap fails at6 (mask64); non-overlap fails at3 (mask8).module tb_implication_endpoints; bit clk=0,a=0,mid=0,gnt=0; int tick=1,samples=0,starts=0,over_fail=0,next_fail=0,over_mask=0,next_mask=0; always #5 clk=~clk; always @(posedge clk) begin  samples++;  if(a)starts++; end A_overlap:assert property(@(posedge clk)(a ##1 mid)|->gnt)  begin end else begin over_fail++;over_mask|=1<<tick;end A_next:assert property(@(posedge clk)(a ##1 mid)|=>gnt)  begin end else begin next_fail++;next_mask|=1<<tick;end initial begin  for(int cycle=1;cycle<=10;cycle++)begin   if(cycle>1)@(negedge clk);   tick=cycle;a=(cycle==1||cycle==5);mid=(cycle==2||cycle==6);gnt=(cycle==2||cycle==7);  end  @(negedge clk);  if($time!=100||samples!=10||starts!=2||over_fail!=1||next_fail!=1||over_mask!=64||next_mask!=8)   $fatal(1,"implication endpoint oracle");  $display("IMPLICATION ENDPOINT CHECK samples=10 starts=2 overlap_failures=1 next_failures=1 overlap_mask=64 next_mask=8 time_ns=%0d",$time);  $finish; endendmodule

// Kiểm ngữ nghĩa SVA với kết quả tính tay (đếm attempt fail, không đếm vacuous).// Stimulus theo cycle (đổi ở negedge, sample ở posedge). Cycle k = posedge thứ k (k=1..).//  a: 1 tại cycle 1 và 6;  b: 1 tại cycle 3;  d: 5 tại cycle 6, 0 nơi khác (d sample tại cycle 6 = 5)//  P1: a |-> ##[1:3] b      : attempt@1 thấy b@3 → pass; attempt@6: b không lên ở 7..9 → FAIL ×1//  P2: a |-> b[->1]         : attempt@1 b@3 → pass; attempt@6 không có b trước khi kết thúc mô phỏng → chưa kết luận (0 fail)//  P3: (a, v=d) |=> (d == v): attempt@1 v=0, d@2=0 → pass; attempt@6 v=5, d@7=0 → FAIL ×1module tb;  logic clk = 0, a = 0, b = 0; logic [3:0] d = 0; int f1 = 0, f2 = 0, f3 = 0;  always #5 clk = ~clk;  property p3; logic [3:0] v; @(posedge clk) (a, v = d) |=> (d == v); endproperty  A1: assert property (@(posedge clk) a |-> ##[1:3] b) else f1++;  A2: assert property (@(posedge clk) a |-> b[->1]) else f2++;  A3: assert property (p3) else f3++;  initial begin    // negedge thứ n chuẩn bị giá trị cho posedge thứ n+1; posedge 1 ở t=5 thấy giá trị khởi tạo.    // Đặt trực tiếp trước posedge tương ứng:    a = 1;                                   // posedge1 (t=5): a=1    @(negedge clk) a = 0;                    // posedge2    @(negedge clk) b = 1;                    // posedge3: b=1    @(negedge clk) b = 0;                    // posedge4    @(negedge clk);                          // posedge5    @(negedge clk) begin a = 1; d = 5; end   // posedge6    @(negedge clk) begin a = 0; d = 0; end   // posedge7    repeat (4) @(negedge clk);    $display("SVA RESULT f1=%0d f2=%0d f3=%0d (expect 1 0 1)", f1, f2, f3); $finish;  endendmodule

// Functional coverage: coverpoint, bins, cross; đọc get_coverage().module tb;  bit [1:0] kind; bit wr;  covergroup cg; cp_k: coverpoint kind { bins k[] = {[0:3]}; } cp_w: coverpoint wr; x: cross cp_k, cp_w; endgroup  cg c = new;  initial begin    for (int i = 0; i < 4; i++) begin kind = 2'(i); wr = 1; c.sample(); end    $display("C08 RESULT cov=%0.1f (LRM expect 66.7 = avg(cp_k 100, cp_w 50, cross 50))", c.get_coverage());    $finish;  endendmodule