I am working on Formal Verification of Digital Design and i am aware of Symbolic Variable Technique to verify design by letting Formal tool to drive free signal.
I also come to know the term Non Deterministic Verification, so is that the same as Symbolic Variable Technique or it is something different?
Hi Peter,
The "symbolic variable" technique is according to me as follows:
--> It means we will take one signal(free variable) and let the formal tool drive it on its own and we will use that variable in our formal (sva) property In that way we can verify a block that has repetition or multiple instances and makes FV engineer work easy.
Why I am asking about Nondeterministic Verification:
I was discussing data integrity check for memory(FIFO) verification with one of my colleagues with specifications as follows:
(1) Two port Memory is 1k Deep with a 16-bit width of each location
(2) Simultaneous Read and Write is possible
(3) All addresses are accessible without requiring to read/write in order
(4) When data is read out, output data == 0.75*read_data
Port 1 --> Write Port
input valid_wr
input addr_wr
input data_wr
Port 2 --> Read Port
input valid_rd
input addr_rd
output data_rd
--> I proposed creating a local variable reg [1023:0] data_store[15:0], and when data is read out we can check as follows:
inside always block:
if(valid_wr)
data_store[addr_wr] data_rd == data_store[addr_rd]*0.75)
without storing any data to local variables(reg), can we verify the data integrity between read and write data?
So I came across the term Nondeterministic verification which can do this verification without storing the data in the FV testbench.
I am not sure how it can be done without storing the data locally, if it is possible then please help me understand how it can be done.
Thanks,
Regards,
Viraj Rawal
- Badges
- Science method
- Similar topics
- Biological Science
- Ecology