ECE 598 SV

Formal Hardware/SoC Verification

Assignment

(due on November 2nd, Monday)

Assignment.pdf

Files:

cache.pdf

gccp.txt (SMV)

nsl.txt (Promela)

You are allowed to use any of the following language + tool combinations:

1) Verilog +Cadence IFV

2) SMV language + Cadence SMV

3) Promela + SPIN

4) C language + MurΦ

For Questions 2 and 3, you are allowed to rewrite the given files as one of these four combinations.

Using Cadence IFV:

Once you have reached a Linux prompt on any one of the EWS servers, type ece598sv

This creates and directs you to an ece598sv working directory. All the necessary scripts are automatically sourced to set the enivornment variables.

The command to launch Cadence IFV is ifv –f filename.v

The other 3 tools can be downloaded from the Web.