In reply to bmorris:
*In reply to ben@SystemVerilog.us:*Ben,
I am going through your papers. First, my methodology question…
- From what is dissolving into my understanding, it appears that assertions are good at targeting lower-level/temporal level requirements.
[Ben] Yes, they do best over here.
Below is a link from my SVA 4th Edition book that addresses this topic of SystemVerilog Assertions in the design process http://SystemVerilog.us/svabk4_process.pdf
My main point are:
SystemVerilog properties can be used to capture system/subsystem level requirements, and those properties can then be reused in a testbench environment, later in the design cycle. System-level requirements can have the following classifications:
Functional: This represents the purpose of the design.
Performance: That consists of items such as baud-rate, frequency, capacity, speed, throughput, and latencies.
Interface: Since the design under consideration may interface to existing busses, and connections to other subsystems, the requirements document needs to include software, hardware, and communications interfaces. That should also include expected modes of operations and restrictions (e.g., parity type, frame size, master, slave).
Safety: Many designs are subject to security and safety issues to insure safe operations under certain conditions or failures (e.g., during reset, power down, power-up, hot plugging, bus or unit failure).
Operational: Some designs are subject to user interfaces for commands, configurations, or maintenance.
Resource: Resources are requirements that are critical to a design, and include items such as power, memory, form-fit factor (i.e., size), etc.
The performance, interface, and safety classifications can be expressed in SystemVerilog Assertions using libraries defined in checkers or in modules. It is important to note that requirements are independent of the architecture and implementation. However, the architecture and implementations are a result of the requirements.
Generally, our “requirements” are higher level. Example “The DUT shall support transmission of IGMP Query”. In my testbench, I use a packet monitor connected to a coverage collector, and simply sample the queries that come out. I’m not sure how I would parse, and detect these packets using assertions (probably because I’ve not tried!) These requirements don’t appear to easily map to assertions. Agree/Disagree/thoughts?
[Ben] There are many cases where SVA needs to be supported by auxiliary code. Looking at Internet Group Management Protocol - Wikipedia
You have GMPv2 messages
IGMPv2 packet structure[8]
+ Bits 0–7 8–15 16–31
0 Type Max Resp Time Checksum
32 Group Address
My point is that one could use supporting logic to parse these fields, and then use assertions to determine if the correct path was taken by the RTL. Note that an “assertion” is a “a confident and forceful statement of fact”, and that can be checked in a variety of ways:
- Visual (looking at waveforms, did that BTW)
- Code
- scoreboard
- formal verification (if meaningful)
- simulation with assertions (if meaningful)
- I could see a list of derived requirements, I.e. requirements generated because of the designers chosen implementation of the higher level requirements being perfect for assertions. Basically all the nuts and bolts of the design, and the interface protocols. Agree/Disagree/thoughts?
[Ben] It is important to note that requirements are independent of the architecture and implementation. However, the architecture and implementations are a result of the requirements.
- Assertions based on requirements are portable because they are independent of the implementation.
- An implementer of the requirements does write assertions for several reasons:
- - Expresses design directives taken, which can be challenged during design reviews
- Documents assumptions, which can be challenged during design reviews
- Puts a check on things that need to be taken care of when assertions are written prior to implementation.
- Expresses an understanding (or misunderstanding) of the requirements in a clearer manner
We don’t write down any implementation specific requirements. Should we, and then generate assertions to target those? Alternatively, should we NOT write them down, and let the assertions BE the documentation?
[Ben] See my above answer. Implementation specific requirements, but may be needed in some cases when a specific technology or reuse is a requirement; a fact of practical life!
Should the assertions BE the documentation? Good question.
I have not been in a real working environment for many years now; however, I keep in touch with some colleagues, and my son is a sw guru. Not all projects write down requirements, and in any form! Many create them on the fly, using just very high level requirements. In our hardware design world, not many people can read SVA, and intermixing SVA with English requirements can be confusing. In my books, I recommend the intermixing of English with SVA.
Here is a link to a sample requirement doc http://SystemVerilog.us/svabk4_req.pdf
In addition, can/should the assertions also target higher level requirements (which are of more importance in the grand scheme of things)? E.g. I just to know queries were produced, but I do not care how the designer does it)
[Ben] Yes. Keep in mind what an Assertion IS: It is not necessarily an SVA assertion, but more a verification that the statements or requirements of your design are met. If SVA is easier, do that. SVA is really a shorter notation that IMHO, is much easier to read, and can be used for coverage.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115