Assertion-Based Verification(ABV)
- capture the required temporal behavioral of the design in a formal an unambiguous way
- capture correct design behavior on a cycle-by-cycle basis
- detect an incorrect design behavior at the time and place it happens
- less dependent
- addresses and documents design decisions
- provides basises for design and verification review
- facilitate functional coverage
- guide test bench vectors for condition to be addressed
- static and dynamic static ver
Assertion Languages
PSL (property specification language):
- abstract, language independent, declarative
- not written as a part of any HDL language
- attached to HDL language using binding directives
- supported by Cadence incisive Verification platform & Mentor
SVA (system verilog assertions):
- SVA is part of system verilog language
- supported in VCS
- history: Intel developed proto language that became SuperLog, which became OVL (open verification language) after Synopsys acquired the company. OVA/OVL was then release to the Accellera standards body to become SVA.
- vcs comes with checkerlib assertion library of common assertions
- converters exist between languages
- formal verification tools often support all assertion languages
- (see http://www.systemverilog.org/products/products_solu.html)
Advantages of SVA
- Ease of adoption because built into Verilog instead of separate language, means the assertions can be unified with the design.
- less assertion code due to automatic contextual understanding
- simple hookup between assertions and test bench
- inherit expression language of system verilog language , including data type, syntax and semantic
- ability to interact with Verilog and C functions on pass/fail
- clearly defined scheduling semantics allow formal verification
- eliminates much of co-simulation overhead since the assertions are built into the internal scheduler
- ability to attach method calls to the detection of a temporal event within an assertion
- interaction with test bench components , e.g. action blocks to trigger a failure handling task
Property
- a property defines a behavior of design
- can be instantiated in module, interface, program, clocking block, package and compilation unit.
- properties can't contain other properties
- properties can contain local variables that remain valid for the life of the thread
property syntax
property property_identifier [([list_of_formals])];
[(asertion_variable_declaration)]
property_spec;
endproperty [:property_identifier]
property_spec::=
property expr
are built using sequences, other sub-level properties and simple Boolean expressions. The individual elements are combined using property operators.
- 7 types of properties: sequence, negation, conjunction, disjunction, if…else, implication
property_expr ::=
sequence_expr // sequence
| (property_expr)
| not property_expr // negation: property is never to occur
| property_expr or property_expr // conjunction: either of two properties satisfies the property
| property_expr and property_expr //disjunction: both of properties must be met for the property to be fulfilled
| property_expr |-> property_expr // implication overlapping
| property_expr |=> property_expr // implication non-overlapping
| if ( expression_or_dist) property_expr [else property_expr]
| property_instance
| clocking_event property_expr
clocking event
- posedge or negedge.
- it can be omitted when
· property defined within a clocking block.
clocking assertions @(posedge clk1);
property p_req2sen;
$rose(req_dat) |=> ##[0:3] ready;
endproperty : p_req2sen
endclocking : assertions
· property defined with a default clocking
module clocks(input clk1)
clocking sysclk @(posedge clk);
endclocking: sysclk
endmodule
module …
default clocking top.clocks.sysclk;
property p_regack;
$rose(req) |=> ##[0:3] ack;
endproperty : p_reqack
disable_iff
disableing condition: assertion terminated when iff expression is true, and any future obligations of the property are also cancelled as the disabling expression is true. When the expression becomes false, the property checking is then resumed.
o Nesting disable iff is not allowed , because is not allowed in property_expr
o don’t use disable iff in properties that are likely to be used by other properties.
o restrict the disable iff to the higher level properties
Implication operators
- to specify the sequence of events that must occur before checking for another sequence
o overlapped implication operator |->
o non-overlapped implication operator |=>
sequence_expr |-> property_expr
- Implication operators are property operators not sequence operators
- When antecedent fails, the property holds and is TRUE. This condition is referred to as vacuous success.
- When antecedent is TRUE, the property requires that the consequent must also be TRUE.
Overlapped implication operator
- If there is a match for the antecedent sequence_expr, then the end point of the match is the start point of the evaluation of the consequenr property_expr
Non-overlapped implication operator
- If there is a match for the antecedent sequence_expr, then the end point of the match is the clock tick after the endpoint of the antecedent
Property Examples
Basic Examples
Example 1.
Property with formal arguments: when a req is received within 0 to 5 cycles later acknowledge is to be received.
poprety ReqAck(ack,req);
@(posedge clk) disable iff(reset)
req |=> ##[0,5] ack; // when req is asserted, within 0 to 5 cycles
// later acknowledge is to be received
endproperty : ReqAck
Local Variable Examples
Example 1.
A network device requires that enqued packets must be dequed within 100 cycles. The dequeing order is non-deterministic and depends on target buffer availability and other factors.
property pDatain2dataout_OK;
logic [31:0] v_data; //store incoming data
int vpacket_id; //write packet ID
($rose(load),v_data=datain, vpacket_id=packet_id) |=>
##[0:100] dout==v_data && packet_id==vpacket_id |-> dataout==v_data;
endproperty : pDatain2dataout_OK
Example 2.
When an acknowledge to a DMA request is received, the DMA logic transfers one data word per cycle to/from the memory until a done or abort is received. The following assertion insures that the number of memory words written/read corresponds to the value of the DMA address, which counts in upward direction. For example if the dma_addr is onitially at address 10, and ends at address 15, then 5 words were read or written.
property pDMAcount;
int v_count; //word count
logic [31:0] v_dma_ddr; // initial starting address
@(posedge clk)($rose(dma_ack),v_count=1, v_dma_addr=dma_addr) |=>
(`true, v_count += 1)[*0:$] ##1
(done || abort) |-> v_count == (dma_addr - v_dma_addr);
endproperty : pDatain2dataout_OK
Example 3.
When a bus request is received, then within a user-defined number of cycles, acknowledge must be received. Thereafter, a transfer of data (indicated by xfr) occur for rep number of cycles, and then done occurs.
property pReqAckDone(req,ack,xfr,done, upper, lower,rep);
int v;
@(posedge clk)(req,v=1) |=> //if request, then initialize couter v.
(v < upper && !ack, v += 1)[*0:$]
##1 ((v >= lower) && ack, v=1) //reset variable v to count number
//of data tansfer
##1 (xfr && (v< = rep), v = v+1)[*0:$] // xfr control must be asserted
// vrep times
##1 v==rep //end the repeat
## done; // until done occurs. At that point, property completes.
endproperty : pDatain2dataout_OK
Sequences
- sequence of events that may last for one or more cycles to represent a design property.
- can be declared with optional arguments
- can be instantiated in properties
- can use local variables
- can define a clocking event for the sequence
- can be operated upon by sequence methods( ended, matches, or triggered)
Capturing temporal behavior
-A non-trivial design will have a behavior spanning across a number of cycles
simple delay
##n //n is natural number (0 to 231-1) of clock cycles
delay range
##[n:m] //n and m are natural number, epresenting a range of cycles
open-ended
##[n:$] //n is a natural number, $ represents infinity, representing a range n or more cycle
Using “not” with Implication operator
- Avoid using not when it is meant to express the notation of “the antecedent should never be followed by a consequent, and if the antecedent is FALSE then the property is vacuouslt TRUE”
o not (a |->b) is equivalent to a&& !b, not the same meaning as a |-> !b tht is equivalent to !(a &&b)
o an equivalent way to express sequence A occurs, then sequence B should never occur
Sequence A |-> Sequence B |-> `false
FIRST_MATCH Operator
- matches only the first of possibly multiple matches
- sequence_expr ::= …
first_match( sequence_expr(, sequence_match_item))
Methods supporting sequences
ended
- endpoint detection in single clock assertion
- it is true when instantiated sequence completes
- shall not be used in disable iff statement
- the validity of the result of the ended method of a sequence is a narrow window in the observe region
- the endpoint of a sequence is reached whenever the ending clock tick of a match of the sequence is reached, regardless of the starting clock tick of the match. For example:
sequence qReqAck: req ##[0:100] ack; endsequence: qReqAck
property p_prop1; go |=> qReqAck ##1 done; endproperty: p_prop1
property p_diff_than_prop1;
go |=> qReqAck.ended ##1 done;
endproperty: p_diff_than_prop1
p_prop1 fails when req is not asserted after go, yet property p_diff_than_prop1 can successfully be completed if ack occurs after go due to an earlier req
triggered
- returns the current end status of an instantiated sequence
- provides level sensitive controls of properties and procedural codes as a result of sequence termination
- the triggered method is an event for each declared sequence
matched
- In multiple clock sequences, the endpoint of a sub-sequence can happen in one clock domain while the start of the next sub-sequence can happen in another clock domain.
- The result of ended method need to be latched and synchronized till the destination clock. This is performed with matched method.
Repetittion operators
consecutive repetition
- Ito repeat a sequence, the [*range] format is used
[*n] repeats for n cycles
[*0:$] repeats for zero or any number of cycles
[*n:m] repeats for minimum of n to a maximum of m cycles
[*0:m] either skipped or repeats a maximum of m cycles
[*n:$] repeats for a minimum of n cycles
non-consecutive repetition
The sequemce non-consecutive operator [=n] is similar to o consecutive repetition operator with the expression is repeated either in consecutive or non-conseqcutive cycles. Thus, there are exactly n repetitions in a path of length m, where m can be greater than n.
goto repetition, non-consecutive exact repetition
The sequence goto[->n] repetition operator is similar to [=n] operator where the expression is repeated in either consecutive or non-consecutive cycles, but the Boolean expression must be hold on the last cycle of the expression being repeated.
Sequencescomposition operators
sequence fusion (##0)
sequence disjunction (or)
- constructs a sequence in which both sequences hold at the current cycle. The sequence (a ##[0:$] b) or ( c[*1:5] ##1 d) states that both sequence must start at the same time (i.e. a and c), but the sequences may complete at different cycles.
sequence non-length-matching (and)
- constructs a sequence in which both sequences are hold at the current cycle, regardless of wether they complete at the same cycle or different cycle. The sequence (a ##[0:$] b) and ( c[*1:5] ## d) states both the sequences must start at the same time, but the sequences may complete at different time.
sequence length matching (intersect)
- constructs a sequence in which one of the sequences are hold at the current cycle, and must complete at the same cycle. The sequence (a ##[0:$] b) intersect ( c[*1:5] ## d) states both the sequences must start at the same cycle, and must complete at the same cycle.
sequence contaminent (within)
- the composite sequence seq1 within seq2 matches along a finite interval of consequtive clock ticks provided seq2 matches along the interval and seq1 matches along some sub-interval of consecutive clock ticks.
o the start point of the match of seq1 must be no later than the start point of the match of seq2
o the end point of the match of seq1 must be no later than the end point of the match of seq2
condition over sequence (throughout)
[*n][=n][->n]
|
Repetition
| |||
##n
|
Left
|
Cycle delay operator
| ||
throughout
|
Right
|
A signal throughout a sequence
| ||
within
|
Left
|
An inner sequence within an outer sequence
| ||
intersect
|
Left
|
Sequences need to start and end at the same time
| ||
and
|
Left
|
Sequences need to start at te same time, but may end at different times
| ||
or
|
left
|
Either sequences satisfys the property
|
Basic Examples
Temporal
If a rose TRUE, then the sequence continues and will check for b ==1 at the second cycle and c==1 at the fourth cycle.
sequence qAB2C;
$rose(a) ##1 b ##2 c;
endsequence : qAB2C
If a rose TRUE, then the sequence continues and will check for b ==1 at the next cycle. The sequence requires c occurs 1 or 2 cycles after b.
sequence qDelayRange;
$rose(a) ##1 b ##[1:3] c;
endsequence : qDelayRange
If a rose TRUE, then the sequence continues and will check for b ==1 at the next cycle. Note that c can occur after b at any cycle between 0 cycle or at any future cycle..
sequence qOpenRange;
$rose(a) ##1 b ##[0:$] c;
endsequence : qOpenRange
Implication
A sequence bus_free followed in the next cycle by a request must have acknowledge in the same cycle that request is TRUE.
property pRequestAckOverlap;
bus_free ##1 request|-> acknowledge ##1 done;
endsequence : pRequestAckverlap
A sequence bus_free followed in the next cycle by a request is followed at the next cycle by an acknowledge and a cycle after that by done.
property pRequestAckNonOverlap;
bus_free ##1 request|=> acknowledge ## [1:100] done;
endsequence : pRequestAckNonOverlap
Methods supporting sequence
ended
The sequence WrDmaBlock256Words writes a block of 256 words into the memory. The writes to the memory need not to be consequtive, but the total number of words is 256.
sequence qWrDmaBlock256Words(rd_wrn,dma_enb,done);
$rose(dma_ack) ##1 (!rd_wrn && dma_enb) [=256] ##[0:100] done;
endsequence : qWrDmaBlock256Words
property p_dma_block_then_interrupt;
@(posedge clk)
qWrDmaBlock256Words(cpu_rd_wrn,dma_enb,dma_done).ended |->
##[1:5] cpu_interrupt[DMA]; // DMA=integer representing the DMA interrupt number
endproperty : p_dma_block_then_interrupt
The source sequence q_e1 is evaluated at clock clk, while destination sequence q_e2 is evaluated at sysclk. In q_e2, the endpoint of instance q_e1(a,b) is tested to occur sometimes after the occurance of c. Method matched only tests for the endpoint of q_e1(a,b) and has no bearing on the starting point of q_e1(a,b).
sequence q_e1(a,b);
@(posedge clk) $rose(a) ##[2:3] b;
endsequence : q_e1
sequence q_e2;
@(posedge sysclk) c ##1 q_e1(a,b).matched [->1] ##1 d;
endsequence : q_e2
A sequence may have several endpoints. For eample q_e1 has two matches, one match begin a ##2 b and the other match begin a ## b.
The always block in module check_req_ack_done waits for the endpoint (triggered) of the sequence qReq2send. When the condition evaluates to TRUE the wait statement unblock the process, which evaluate an immediate assertion, expecting done_xfr to be TRUE.
module check_req_ack_done(input req,ack, done_xfr,clk);
sequence qReq2send;
@(posedge clk) req ##[0:$] ack ##2 `true;
endsequence : qReq2send
always @(posedge clk) begin
wait(qReq2send.triggered);
wait(qassert_end_xfr: assert(done_xfr) else
$display(“Incorrect data transfer, done_xfr not received”);
end
endmodule: check_req_ack_done
A sequence may have several endpoints. For eample q_e1 has two matches, one match begin a ##2 b and the other match begin a ## b.
This property states that within the window of time starting with a GO signal (go) and ending by the slave asserting the done DMA flag (dma_done), the DMA controller must transfer 2 words of data using the handshake sequence data ready (dma_req) and data accepted (data_accepted) from a slave unit.
property pWITHIN;
@(posedge clk)
(##[0:$] $rose(dma_req) ##1 (##[0:3] ##1 data_accepted)[*2]) within (go ##[ 1:20] done_dma) ;
endproperty : assert property(pWITHIN);
A request is honored with an acknowledge sometime within the next cycle and up to 4 cycles later. The acknowledge is then followed at a later time by a done control signal. However there is one additional requirement that rhroughout the time between acknowledge and done an enable signal must be asserted to drive a tri-state bus.
property p_handshake;
@(posedge clk)
$rose(req) |-> ##[1:4] enable throughout (ack ##[1:$] done) ;
endproperty : p_handshake
The sequence :
(a ##1 b ##2 c)[*3] ;
is equivalent to the sequence:
(a ##1 b ##2 c) ##1 (a ##1 b ##2 c) ##1 (a ##1 b ##2 c) ;
The following sequence has an implicit until, because of the next concatenation expression ( the c) , meaning that if c is hold at the start of the sequence, then a check on b is skipped altoghether, as if it were not there. However, if c does not hold at the start of the sequence, then b needs to hold a maximum of three cycles until c occurs.
(b[*0:3] ##1 c ##1 d);
The [*:$] construct is similar to [*n:m] except that m is infinite. The ##[0:$] delay or `true[*0:$] repeat operators take several meaning in the consequent of a property by causing the property to never fail, but only complete.
(a) |=> (##[0:$] ##1 b[*0:$] ##1 c) ;
- In the consequent, the first element of the sequence ##[0:$] states that anything can happen for any number of cycles.There is no entry in the sequence following the ##[0:$] that can cause the assertion to fail.
- The second element in the consequent, b[*0:$], states b may happen for any number of samples. The sequence is satisfied if b is true followed by c, or if b is false followed by c.
(a) |=> (##[0:$] ##1 c) ; // same as :(a) |=> (##[0:$] ##1 b[*0:$] ##1 c);
If a then, starting from next cycle, there should be two occurance of b either consecutive or non-consecutive, and some time later ( next cycle or later) c occurs.
property p_repeat_equal;
@(posedge clk) (a) |=> (b[=2] ##1 c) ;
endproperty : p_repeat_equal
If a then, starting from next cycle, there should be two occurance of b either consecutive or non-consecutive, then c must occurs in the cycle following the last occurance of b.
property p_repeat_equal;
@(posedge clk) (a) |=> (b[=2] ##1 c) ;
endproperty : p_repeat_equal
*
* Usages: checkers, coverage measurement, assertions for formal proofs,
* constraints for DUT
*
* Typical usage
* - Design engineer: inline SVA code to check design, checkerlib often sufficient
* - Veriifcaction engineer: verify block interfaces, custom assertions often used
* for protocols, assertions typically kept in a separate file.
*
* Instatiating assertions
* 1. In-line: often used by designers for checking their designs.
* 2. As a module in a separate .sva file. Requires binding to DUT.
* Often used by verif engineers.
*
* Compiling and controlling
* SVA_OPTIONS = -sverilog +define+ASSERT_ON -cm assert -assert filter \
* -y $(VCS_HOME)/packages/sva \
* +incdir+$(VCS_HOME)/packages/sva
*
* Kinds of assertions
* 1. combinational (same clk)
* 2. sequential (multiple clks)
*
* Threads and assertions
* SVA checks every assert/cover/assume property every clk cycle.
* Typically, the property has a trigger event or antecedent that causes
* SVA to evaluate the consequent when true. A new thread starts every
* evaluation cycle when the antecedent is true and completes when the
* consequent has completed evaluation (pass or fail). If the antecedent
* is false, the property successed vacuously.
*
* SVA Checker Library is a collection of commonly used assertions in modules
* see $VCS_HOME/packages/sva
*
* Hierarchy of assertions
* - Boolean expressions (i.e. (b>4)), bind, declarative instatiation
* - Sequence: a sequence of boolean expressions with a temporal
* relationship between them
* - Property: consists of a clk signal and one or more sequences
* - properties can't contain other properties.
* - Assertion: consists of one or more proporties
* - only assertions are visible in viewers
* - Cover statement: consists of one or more proporties
* - Assume statement: used to constrain the inputs for formal verification
*
* Formal Syntax
* Request/Grant Example
*
*/
`timescale 1ns/1ns
`ifdef NOT_IN_VCS_YET
// global sequences or properties
sequence follows1(a,b);
a ##1 b;
endsequence
`endif
module sva;
reg clk;
initial clk = 0;
always clk = #5 ~clk;
reg rst_n;
initial begin
rst_n = 0;
repeat (3) @(posedge clk);
rst_n = 1;
end
wire req1,req2,ack1,ack2;
wire [7:0] a,b;
// --------------------------------------------------------------------------------
initial $ova_stop;
always @(posedge rst_n) $ova_start;
always @(negedge rst_n) $ova_stop;
// --------------------------------------------------------------------------------
/* sequences
* - vcs supports linear sequences (list of boolean expressions in
* a linear order of increasing time).
* - sequences are composed of boolean expressions concatenated
* together with the ## operator
* - sequences can be composed of other sequences (nested)
* - if no clock specified, the clk is inherited from the external
* source (property,assertion)
* - limitations: no implications (->) allowed
* - a new attempt to match the sequence is evaluated every clk tick
*/
// seqeuence concatenation (overlapping)
sequence req_imm_ack;
req1 ##0 ack1; // req1 immediately followed by ack1
endsequence
// seqeuence concatenation (non-overlapping)
sequence req_ack_13;
req1 ##[1:3] ack1; // req1 followed by ack1 after 1,2, or 3 clks
endsequence
// seqeuence concatenation (non-overlapping)
sequence req_ack_inf;
req1 ##[1:$] ack1; // req1 is eventually followed by ack1 (unbounded timelimit)
endsequence
// formal parameters generalizes property
sequence same_time(a,b);
a ##0 b; // a and b must be asserted at the same time
endsequence
// specifying a clk and nesting sequences
sequence no_frame_en(a,b,c);
@(posedge clk)
same_time(a,b) ##1 c; // sequence same_time followed by c one clk later
endsequence
// consecutive repetition
sequence cons(a,b);
a [*3] ##2 b; // a asserted for 3 clks followed by b 2clks later (a [*3] == a ##1 a ##1 a)
endsequence
// consecutive repetition range
sequence cons_range(a,b);
a [*1:3] ##1 b; // a asserted for 1 to 3 clks followed by b 1clk later
// alternatively use [*1:$] for 1 or more clks (unbounded)
endsequence
// Value change functions
sequence valchg1(a,b,c);
$rose(a) ##1 $stable(b && c); // b and c are stable on the rising edge of a
endsequence
// edge functions
sequence edge_seq(a,b,c);
$rose(a) ##1 $fell(b && c); // falling edge of b and c after the rising edge of a
endsequence
// looking into the past
wire valid = a;
wire clk_valid = clk & valid;
sequence counter;
@(posedge clk_valid)
(b != $past(b,1)); // no two consecutive valid values of b are the same
endsequence
// anding sequences: both sequences must occur, but not necessarily at the same time
sequence and1(a, b, c, d);
cons(a,b) and cons(c,d);
endsequence
// oring sequences: one of the sequences must occur
sequence or1(a, b, c, d);
cons(a,b) or cons(c,d);
endsequence
// throughout: a condition must be met throughout the sequence
sequence th1(a,b,c);
a throughout b ##[1:4] c; // a must be true for all the clks of the sequence b ##[1:4] c
endsequence
// --------------------------------------------------------------------------------
/* Properties: made up of sequences (either in-lined or referenced)
* - a clock must be specified either in the property or the referenced sequence
* - properties can't contain other properties
* - implication can only appear in properties
*/
property p1(a,b); // take formal args too
@(posedge clk) a ##1 b; // in-lined sequence
endproperty
property p2(a,b,c); // take formal args too
no_frame_en(a,b,c); // referenced sequence has it's own clock
endproperty
property p3(a,b,c,d);
@(posedge clk) cons(a,b); // referenced sequence doesn't have it's own clock, so we need to specify one
endproperty
// 7 kinds of properties
property kind1(a,b);
@(posedge clk) cons(a,b); // 1. sequence
endproperty
property kind2(a,b);
@(posedge clk) not cons(a,b); // 2. negation
endproperty
property kind3(a,b,c,d);
@(posedge clk) (cons(a,b) or cons(c,d)); // 3. disjunction (both must be true)
endproperty
property kind4(a,b,c,d);
@(posedge clk) (cons(a,b) and cons(c,d)); // 4. conjunction (only one needs to be true)
endproperty
`ifdef NOT_IN_VCS_YET
property kind5(en,a,b,c,d);
@(posedge clk) (if (en) cons(a,b) else cons(c,d)); // 5. if..else
endproperty
`endif
// note that |=> is equivalent to |-> ##1
property kind6(a,b);
@(posedge clk) (a |-> b); // 6. implication: if antecedent |-> consequent, over-lapping
endproperty
property kind6b(a,b);
@(posedge clk) (a |=> b); // 6. implication: if antecedent |=> consequent, non-over-lapping
endproperty
// --------------------------------------------------------------------------------
/* assert: checks a property or sequence
* - by default only failures reported
* - if no clock specified in assertion it is inherited from the property/sequence
*/
a_imp: assert property (kind6(a,b));
// immedate assertions
no_imm_ex: assert property ( @(posedge clk) (a==4) );
// vcs doesn't support pass blocks, only fail blocks
fail_blk_ex: assert property ( @(posedge clk) (a==4) ) else $display("fail block");
// --------------------------------------------------------------------------------
// cover: monitors a property or sequence (no checking for failure)
c1: cover property(p1(req1,ack1));
// --------------------------------------------------------------------------------
/*
* Formal syntax
* assert property (expression) action_block
*
* Expression features
* PSL SVA description
* ------- -------- -----------------
* {...} (...) sequence delimiter
* [*] [*] zero or more
* [+] [*1:$] one or more
* same [*count] [*range] consecutive repetition
* same [*=count] [*=range] arbitrary repetition (not in vcs)
* same [->count] [*->range] "goto" repetition (not in vcs)
* | or
* & and
* ! not
* && intersect length-matching sequence
* within within a occurs in some cycle(s) during b
* throughout a occurs in every cycle(s) during b
* ; ##1 seqeuence concatenation (non-overlapping, next cycle)
* ##N seqeuence concatenation (non-overlapping, N cycles later)
* : ##0 seqeuence concatenation (overlapping, same cycle)
* |-> |-> sequence same-cycle implication
* |=> |=> sequence next-cycle implication
* always always
* never always not (same as never)n
* abort disable iff interrupt (with sucecess)
*/
// --------------------------------------------------------------------------------
/* req/grant arbitor example
* assert never gnta&& !reqa; // a grant never occurs without a request
* assert always gnta -> !gntb; // if a receives a grant, then b does not
* assert never gnta&& next gnta; // A never receives a grant in two successive cycles
* assert always gnta || gntb -> next busy; // grant is always followed by a busy
* assert always reqa -> eventually gnta; // a request is eventually followed by a grant
*/
dut dut(/*AUTOINST*/
// Outputs
.clk (clk),
.a (a[7:0]),
.b (b[7:0]),
.req1 (req1),
.req2 (req2),
.ack1 (ack1),
.ack2 (ack2));
endmodule
/* The modular way to apply SVA is to have a separate module/file of
* properties/assertions that is bound to instances. This approach
* is espescially useful for verifying common interfaces or protocols
*
* syntax: bind dut_inst_path sva_module sva_instance_name (port_list)
* bind dut_module_name sva_module sva_instance_name(port_list)
* - the ports in the port_list can either be absolute paths to any
* signal in the design or relative paths to the dut.
* - the dut_inst_path format only applies the checker to one instance
* while the dut_module path applies to all instances of the dut module
*/
// --------------------------------------------------------------------------------
`ifdef BIND_INST
bind sva.dut ack_checker dut_ack_chkr
(
// req1 is a port,signal,reg within dut, while req is a port in the sva module
.clk(clk),
.req(req1),
.ack(ack1)
);
`else
bind dut ack_checker dut_ack_chkr
(
// req1 is a port,signal,reg within dut, while req is a port in the sva module
.clk(clk),
.req(req1),
.ack(ack1)
);
`endif
module ack_checker(/*AUTOARG*/
// Inputs
clk, req, ack
);
input clk;
input req;
input ack;
property ack_occurs_p;
@(posedge clk) req ##[1:4] ack;
endproperty
ackchk: assert property (ack_occurs_p);
endmodule
// design to test drives signals out for clarity. Normally the assertions would be with the code
module dut(/*AUTOARG*/
// Outputs
clk, a, b, req1, req2, ack1, ack2
);
input clk;
output [7:0] a;
output [7:0] b;
output req1,req2,ack1,ack2;
// some value changes
reg [7:0] a,b;
initial begin
a = 4;
@(posedge clk);
a = 3;
@(posedge clk);
a = 4;
end
// emualate an arbitor
reg req1, req2, ack1, ack2;
initial begin
req1=0; ack1=0; req2=0; ack2=0;
@(posedge clk);
req1=1; ack1=0; req2=0; ack2=0;
@(posedge clk);
req1=1; ack1=1; req2=0; ack2=0;
@(posedge clk);
req1=0; ack1=0; req2=0; ack2=0;
@(posedge clk);
req1=1; ack1=0; req2=1; ack2=0;
@(posedge clk);
req1=1; ack1=0; req2=1; ack2=1;
@(posedge clk);
req1=1; ack1=0; req2=0; ack2=0;
@(posedge clk);
req1=1; ack1=1; req2=0; ack2=0;
@(posedge clk);
req1=0; ack1=0; req2=0; ack2=0;
@(posedge clk);
$finish;
end
endmodule // dut
No comments:
Post a Comment