gistfile1.txt

// Example SVA properties

// Strobe must be high when CYC rises--true of many (but not all) bus masters
property INITIATE_REQUEST
	@(posedge i_clk)
	(!CYC) ##1 (CYC) |-> STB
endproperty

assert property(INITIATE_REQUEST);

// Some peripherals, such as a flash, might only ever accept a single
// request, and be stalled until it that request a response
property SINGLE_ACK
	@(posedge i_clk)
	disable iff ((i_reset)||(!i_wb_cyc))
	(STB)&&(!STALL) ##[*0:N] (STALL)&&(!ERR) ##1 ((ACK)||(ERR));
endproperty

assert	property(SINGLE_ACK);

// Other peripherals will *never* stall the bus.  These peripherals have a
// fixed pipeline length, and will *always* acknowledge (or error) a request
// within N clock cycles
property NEVER_STALL(N)
	@(posedge i_clk)
	disable iff ((i_reset)||(!i_wb_cyc))
	((STB) ##[*N] ((ACK)||(ERR)))
	and (!STALL);
endproperty

// Some peripherals I've seen will ACK on the same clock they
// receive a request
assert	property(NEVER_STALL(0));

// Most of my peripherals will ACK in one clock
assert	property(NEVER_STALL(1));

// Some of my peripherals will ACK in two clocks
assert	property(NEVER_STALL(2));


// Once a REQUEST is placed on the bus, it shouldn't change until
// it is accepted by STALL dropping
sequence HOLDREQUEST
	@(posedge i_clk)
	disable iff ((RESET)||(!CYC))
	(STB)&&($stable(request))&&(STALL) [*0:$]
		(STB)&&($stable(request))&&(!STALL);
endsequence

assert property( @(posedge i_clk) (STB)&&(STALL) |=> HOLDREQUEST);

// Many of my bus masters will not initiate a bus cycle without also
// initiating a bus request
property INITIATE_REQUEST
	@(posedge i_clk)
	(!CYC) ##1 (CYC) |-> STB;
endproperty

// Many (not all) of my bus masters will never issue a discontinuous request
// Counter examples would be an atomic Read-Modify-Write cycle, or a
// prefetch that makes further read requests if the bus is still open.  Still,
// this is a useful property.
property CONTINUOUS_REQUEST
	@(posedge i_clk)
	(CYC)&&(!STB) |=> !STB
endproperty

assert property(CONTINUOUS_REQUEST);

// A slave may only ever stall the bus for N cycles
property LIMITED_STALLS(N)
	@(posedge i_clk)
	disable iff ((i_reset)||(!CYC))
	(STB)&&(STALL) ##[*0:N] (STB)&&(!STALL)
endproperty

assert property (STB |-> LIMITED_STALLS(MAX_STALLS);

// Following a bus error, the cycle should be aborted
assert property((CYC)&&(ERR) |=> (!CYC));

// Strobe can only be asserted if CYC is also true
assert property(STB |-> CYC);

// The bus direction cannot change without a pause in the request cycle
property MAINTAIN_DIRECTION
	@(posedge i_clk)
	disable iff ((i_reset)||(!CYC))
	STB ##1 STB |-> $stable(WE));
endproperty

assert property(MAINTAIN_DIRECTION);

// Cannot have both an acknowledgement and an error response on the same
// cycle
property ONE_TYPE_OF_RESPONSE
	(!CYC)||(!ACK)||(!ERR);
endproperty

assert property(ONE_TYPE_OF_RESPONSE);

// No responses should come back from the bus following a reset or abort.
// Or ... not quite, there should be at least a clock and then no responses
property NO_RESPONSES_WHILE_IDLE
	@(posedge i_clk)
	((i_reset)||(!CYC)) ##1 (!CYC) |-> ((!ACK)&&(!ERR));
endproperty

assert property (NO_RESPONSES_WHILE_IDLE);