In reply to ben@SystemVerilog.us:
Hi ben,
I'm trying to understand the behavior of disable iff. so I make one another example.
`timescale 1 ns / 1 ns
module MUX
(
input wire CLOCK ,
input wire [3:0] IP1 ,
input wire [3:0] IP2 ,
input wire [3:0] IP3 ,
input wire SEL1 ,
input wire SEL2 ,
input wire SEL3 ,
output reg [3:0] MUX_OP
) ;
always @(posedge CLOCK)
if (SEL1 == 1)
MUX_OP <= IP1 ;
else if (SEL2 == 1)
MUX_OP <= IP2 ;
else if (SEL3 == 1)
MUX_OP <= IP3 ;
property mux_p1;
@(posedge CLOCK)
$rose(SEL1) |=> ( IP1==MUX_OP);
endproperty
property mux_p2;
@(posedge CLOCK)
if (!$isunknown(SEL1))
$rose(SEL1) |-> (IP1== MUX_OP);
endproperty
check00 : assert property (mux_p1);
check01 : assert property (mux_p2);
endmodule
`timescale 1 ns / 1 ns
module T_MUX ;
parameter PERIOD = 10 ;
reg CLOCK ;
reg [3:0] IP1 ;
reg [3:0] IP2 ;
reg [3:0] IP3 ;
reg [2:0] SEL ;
wire [3:0] MUX_OP ;
MUX MUX1
(
.CLOCK ( CLOCK ),
.IP1 ( IP1 ),
.IP2 ( IP2 ),
.IP3 ( IP3 ),
.SEL1 ( SEL[0] ),
.SEL2 ( SEL[1] ),
.SEL3 ( SEL[2] ),
.MUX_OP ( MUX_OP )
) ;
always
begin
CLOCK <= 0 ;
#(PERIOD/2) ;
CLOCK <= 1 ;
#(PERIOD/2) ;
end
initial
begin : TEST
integer i ;
@(posedge CLOCK);
#(PERIOD/4); // Keep changes away from clock edges
IP1 <= 4'b0001 ;
IP2 <= 4'b0010 ;
IP3 <= 4'b0100 ;
$display ("Starting 1st set of test vectors.");
for (i=0; i<=2; i=i+1)
begin
SEL <= 1<<i ;
#(PERIOD) ;
end
for (i=0; i<=7; i=i+1)
begin
SEL <= i ;
#(PERIOD) ;
end
$display ("Finished 2nd set of test vectors.");
$finish ;
end
endmodule
I want to check MUX_OP has the same value of IP1 after unknown period.
So I generate 2 property.
property mux_p1;
@(posedge CLOCK)
$rose(SEL1) |=> ( IP1==MUX_OP);
endproperty
mux_p1 is pass but mux_p2 does not.
property mux_p2;
@(posedge CLOCK)
if (!$isunknown(SEL1))
$rose(SEL1) |-> (IP1== MUX_OP);
endproperty
this Assertion has failed at time 15NS, How do I approach "disable iff" correctly?