| Login | | Don't have an account yet? You can create one. As a registered user you have some advantages like theme manager, comments configuration and post comments with your name. | |
| Who's Online | There are currently, 52 guest(s) and 2 member(s) that are online.
You are Anonymous user. You can register for free by clicking here | |
 | |
|
Verification Guild: Forums |
|
| View previous topic :: View next topic |
| Author |
Message |
Gareth
Senior
Joined: Jan 12, 2004
Posts: 21
Location: Edinburgh, Scotland
|
 Posted: Wed Oct 20, 2004 5:21 am Post subject: ABV of serial protocols |
 |
|
I'm a bit of a noob to ABV so this may be a stupid question ("there is no such thing as a stupid question, only a stupid questioner").
What would be the be best way to verify a serial based protocol using ABV? For example, I2C or MDIO from the Ethernet standard? In these cases, the state of the system at any particular moment is a function of all the previous bits on the wire in that particular serial word or transaction.
Property specification languages seem to be good as specifying the correct behaviour of parallel interfaces with control or handshaking signals. However, serial protocols frequently embed this information into the data stream itself in one way or another, and on the face of it property specification appears to be operating at the wrong level of abstraction.
I've seen a verification methodology in a Synopsys seminar for a simple UART design that used an HDL behavioural process to count from the start of the serial word (say, when a start bit is detected), and the value of that counter used as a state variable in the assertions layered on top of the HDL testbench.
However, it's my feeling that this hybrid HDL/Assertion language approach to building the property will not transfer well, say, to any of the formal or hybrid tools (I have had no experience with this kind of software so I can't say for definite).
The issues becomes even more severe in the higher speed serial protocols, that may be munged by an 8B10B encoder in the case of 1-Gigabit Ethernet or a shift-register scrambler in the case of 10-Gigabit Ethernet? How could one go about building a property specification for this kind of protocol? Or do you just forget it and only verify "behind" the scrambler or encoder?
Cheers
Gareth |
|
| Back to top |
|
 |
Gadi
Newbie
Joined: Oct 24, 2004
Posts: 2
|
| Posted: Tue Oct 26, 2004 5:37 am Post subject: |
|
|
Control-path verification is similar in serial protocols and other protocols. PSL sequences are useful.
| Code: |
-- start and stop are predefined auxiliary signals.
-- between start and stop,
-- after every eight bits of data transfer datain is received.
assert always {{start; [*8]; {datain; [*8]}[*]} && !stop}|=> {datain};
|
Endpoints and the before operator may be used to refer to the past.
| Code: |
-- if stop occurs than start occurred somewhere in the past.
endpoint after_start := {start; [+]};
assert always (stop -> after_start);
-- datain must be received between start and stop.
assert always (start -> next (datain before stop));
|
Data-path verification can be done with few data bits only. So, there is no need to monitor all data bits on the serial bus.
If a serial protocol is checked together with neighbor components, you can access buffers that store data before and after it was transferred on the bus.
The forall construct is useful to gather bits directly from a serial bus.
| Code: |
assert forall d(0..4) in boolean: always {start; data=write; data=d(0); data=d(1); data=d(2); data=d(3); [*]; start; data=read} |=>
{data=d(0); data=d(1); data=d(2); data=d(3)};
|
| Quote: |
The issues becomes even more severe in the higher speed serial protocols, that may be munged by an 8B10B encoder in the case of 1-Gigabit Ethernet or a shift-register scrambler in the case of 10-Gigabit Ethernet? How could one go about building a property specification for this kind of protocol? Or do you just forget it and only verify "behind" the scrambler or encoder?
|
It's easier to check the data behind the encoder or the scrambler, that is, to check the data before it was encoded or after it was decoded.
In order to check the encoded bits you will have to write some kind of decoder/descrambler that fits your needs. The implementation of the decoder that is used by the protocol can help. |
|
| Back to top |
|
|
alexg
Senior
![]()
Joined: Jan 07, 2004
Posts: 586
Location: Ottawa
|
| Posted: Tue Oct 26, 2004 8:48 pm Post subject: |
|
|
| Gadi wrote: | Data-path verification can be done with few data bits only. So, there is no need to monitor all data bits on the serial bus.
|
Does in mean that with few data bits we can formally validate the datapath function?
And another question: can we use 8/10 encoders/decoders or shift-reg scramblers in formal verification?
Regards,
Alexander Gnusin |
|
| Back to top |
|
|
Gadi
Newbie
Joined: Oct 24, 2004
Posts: 2
|
| Posted: Wed Oct 27, 2004 9:06 am Post subject: |
|
|
| Quote: | | Does in mean that with few data bits we can formally validate the datapath function? |
It's better to check all data bits but often the model becomes to big for formal verification. It is enough to check few data bits in case a data path merely transfers some data buffer across the design. If some part of the bits get corrupted and others are transferred correctly, simulation should discover it.
In case data paths involve more complex functionality, such as arithmetic and data-integrity operations, all bits must be examined.
The decision between data paths and control path is not clear cut, for example, a packet address determines the packet destination and then being treated as a part of the data.
| Quote: | | can we use 8/10 encoders/decoders or shift-reg scramblers in formal verification? |
I don't understand the question. |
|
| Back to top |
|
|
alexg
Senior
![]()
Joined: Jan 07, 2004
Posts: 586
Location: Ottawa
|
| Posted: Wed Oct 27, 2004 8:54 pm Post subject: |
|
|
| Quote: | | alexg wrote: | | can we use 8/10 encoders/decoders or shift-reg scramblers in formal verification? |
I don't understand the question. |
I think, it is impossible to develop the set of assertions (aka bus checker) for the formal verification of serial protocol interfaces (pci express, gigE). First, there is no clock: it is buried within data. Second, formal tools will have problems with LFSR-based data scramblers /descrambles (the same as they have problems with CRC validation). So, formal strategy for serial protocol verification have to be different from the one used for the parallel protocol. Assertions have to be more chip-specific, being applied to internal nodes of design, and not to the protocol interface.
| Quote: | | It's better to check all data bits but often the model becomes to big for formal verification. It is enough to check few data bits in case a data path merely transfers some data buffer across the design. If some part of the bits get corrupted and others are transferred correctly, simulation should discover it. |
I would be more interested to formally verify data transfer not across the design, but across the protocol interface. It means that formal verification environment has to include both sender and transmitter devices.
The idea of verifyng few data bits sounds interesting to me. If these belong to the the packet CRC, then the probablility that whole packets match if checkums partially match is still high. Here, we also have to assume that CRC function works correctly for both transmitter and receiver.
Regards,
Alexander Gnusin |
|
| Back to top |
|
|
|
|
You can post new topics in this forum
You can reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
|
| |
|
|
Forum FAQ
Search
Usergroups
Profile
Digest
Log in
