Common Verilog Mistakes by SystemVerilog Newbies

As part of my HDL Digital Design course at the University of Wyoming, I have to implement various modules using Verilog. Interestingly, the course textbook (Digital Design and Computer Architecture) uses SystemVerilog. This leaves an HDL newbie like me in an interesting spot since I tend to make assumptions about Verilog based on what I’ve seen in SystemVerilog, even though the latter is newer. Some common newbie issues I ran into (that were easily resolved by finding examples of Verilog modules):

  1. Declaring inputs as “input xyz[3:0]” instead of “input [3:0]xyz”.
  2. Trying to use assertions. It was quite surprising to me that assertions as explained in SystemVerilog weren’t “a thing” in Verilog. Some digging around led me to this article discussing assertions (and implying there wasn’t a direct way to assert facts in Verilog).
  3. Concatenating values
  4. No assertions? What… oh, I guess I already mentioned that, but I’m new to this HDL arena.

I guess I could have been more diligent in my search for Verilog tutorials for beginners (like this one) to alleviate all the annoyances I ran into assuming that learning SystemVerilog would translate in a completely seamless transition into writing Verilog code. Oh well, I guess learning a new language doesn’t always involve taking the most efficient path from A to B.


Resolving iverilog __gxx_personality_v0 errors

I ran into a strange error while trying to compile a Verilog module using the Icarus Verilog compiler:

iverilog DLL error

A quick lookup of the __gxx_personality_v0 error on StackOverflow revealed to me that the cause of this strange error is a mismatched/missing libstdc++-6.dll, fixable with a simple command:

copy C:\dev\tools\iverilog\bin\libstdc++-6.dll C:\dev\tools\iverilog\lib\ivl

I still need to investigate exactly why this libstdc++-6.dll problem occurs. It might be related to my Git environment (Git Bash?)


Categories: Theorem Proving

Installing Isabelle 2011

I’ve spent the past few days making a few skills strides – I finally buckled down and learned how to use Emacs. The tutorial felt somewhat long but was worthwhile. Having discovered how easily I can set margins and have my text automatically wrap at 80 characters has made me a convert! Interesting since Emacs is a program I simply never thought was worth the time until I decided to try out the Isabelle theorem prover. I grabbed the 32-bit Linux bundle, ran the simple commands listed on the download page, and was up and running.

tar -xzf Isabelle2011-1_bundle_x86-linux.tar.gz
Isabelle2011-1/bin/isabelle emacs

Having completed my Emacs tutorial, I then worked through the Basic Script Management portion of the Proof General User Manual. These tasks were sufficient to prepare me for my task of analysing some proofs from The Archive of Formal Proofs.


Simple Regex for Finding C++ Blocks

Not particularly accurate (obviously) but sufficient for what I needed:

(?s:\{[^{]+\})

Enables single line matching mode (that matches line termination characters as well), followed by the left curly brace, followed by all subsequent characters that aren’t the right curly brace, and finally ending with a curly brace.


My Resolved Mozilla Bugs

Before starting my masters, I worked on a couple of Mozilla/Gecko items on Bugzilla. Here is a list of all tasks I tackled.


Categories: Valgrind

Quick Introduction to Valgrind

For my Computer Aided Geometric Design course, a simple program called CPLOT is used for some of the project work. Its documentation is on the course website. After my initial draft of my project 1 implementation crashed, I was inspired to try out Valgrind on CPLOT (even though I was able to find the bugs using my debugger). All that’s needed to install Valgrind on Ubuntu is sudo apt-get install valgrind. The CPLOT code supplied needed a minor change in order to compile, so I changed

#include <string.h>;

into

#include <string.h>;

and all was well with the world again. The updated CPLOT code is available in my public repo. Line 1 below compiles the code. The Valgrind Quick Start Guide recommends using the -g flag to produce debugging information so that Memcheck’s error messages include exact line numbers.

g++ -g -o cplot.out cplot.cpp
valgrind --leak-check=yes ./cplot.out eg1.dat eg1.eps

The eg1.dat file I used is the one on page 3 of the CPLOT documentation. Below is the output from valgrind:

==1594== Memcheck, a memory error detector
==1594== Copyright (C) 2002-2010, and GNU GPL'd, by Julian Seward et al.
==1594== Using Valgrind-3.6.1 and LibVEX; rerun with -h for copyright info
==1594== Command: ./cplot.out eg1.dat eg1.eps
==1594==
In initps: eg1.eps
File processed successfully!
==1594==
==1594== HEAP SUMMARY:
==1594==     in use at exit: 120 bytes in 6 blocks
==1594==   total heap usage: 8 allocs, 2 frees, 824 bytes allocated
==1594==
==1594== 120 (8 direct, 112 indirect) bytes in 1 blocks are definitely lost in loss record 3 of 3
==1594==    at 0x402641D: operator new(unsigned int) (vg_replace_malloc.c:255)
==1594==    by 0x8049224: readCurve() (cplot.cpp:182)
==1594==    by 0x8048D89: main (cplot.cpp:127)
==1594==
==1594== LEAK SUMMARY:
==1594==    definitely lost: 8 bytes in 1 blocks
==1594==    indirectly lost: 112 bytes in 5 blocks
==1594==      possibly lost: 0 bytes in 0 blocks
==1594==    still reachable: 0 bytes in 0 blocks
==1594==         suppressed: 0 bytes in 0 blocks
==1594==
==1594== For counts of detected and suppressed errors, rerun with: -v
==1594== ERROR SUMMARY: 1 errors from 1 contexts (suppressed: 17 from 6)

This program can be improved by changing the return statements in the body of the main for(;;) loop into break statements. By so doing, all the cleanup code can be placed after that loop, just before the program exits. This also prevents the duplication of the cleanup code. The code after the for(;;) loop then becomes:

    // Deallocate all allocated memory
    for (int i=0; i < NCURVES; i++) {
        delete curves[i];
    }

    // Close the file resources
    fclose(in);
    fclose(ps);
    return 0;

The Curve class destructor then becomes:

Curve::~Curve() {
    for (int j=0; j <= degree; j++)
        delete points[j];

    delete [] points;
};

Running Valgrind on the updated program then gives the following output.

==6539== Memcheck, a memory error detector
==6539== Copyright (C) 2002-2010, and GNU GPL'd, by Julian Seward et al.
==6539== Using Valgrind-3.6.1 and LibVEX; rerun with -h for copyright info
==6539== Command: ./cplot.out eg1.dat eg1.eps
==6539==
In initps: eg1.eps
File processed successfully!
==6539==
==6539== HEAP SUMMARY:
==6539==     in use at exit: 0 bytes in 0 blocks
==6539==   total heap usage: 8 allocs, 8 frees, 824 bytes allocated
==6539==
==6539== All heap blocks were freed -- no leaks are possible
==6539==
==6539== For counts of detected and suppressed errors, rerun with: -v
==6539== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 17 from 6)

There was another bug in the program since it could attempt to plot control polygons for uninitialized curves because of a missing else. I pushed the trivial fix to that. The program also crashed if the input file specified did not exist because fscanf would try to use a NULL parameter. The fix is a simple NULL check.


Modelling the Infamous Dining Philosophers

A sample implementation of the dining philosophers problem is provided in the JPF core source code. The solution I gave to this problem was to use the following locking scheme: if a thread has an even id i, then it should lock fork i first and then fork (i + 1) % N. If its id i is odd, then it should lock fork (i + 1) % N first and then lock fork i. Replacing

new Philosopher(forks[i], forks[(i + 1) % N]);

with

Fork leftFork, rightFork;
if (i % 2 == 0) {
    leftFork = forks[i];
    rightFork = forks[(i + 1) % N];
} else {
    leftFork = forks[(i + 1) % N];
    rightFork = forks[i];
}
new Philosopher(leftFork, rightFork);

Should do the trick. DiningPhil.jpf can then be launched to verify the absence of deadlock with this new locking scheme.


Getting into Motorcycling

I’ve had the desire to learn how to ride a motorcycle for a few years now. This summer, I decided to act on this bucket list item and enrolled in the Basic Rider Course with UtahRiderEd. I signed up for the weekend option. The classes ran all day Saturday and Sunday (until about 5pm). We were given a Motorcycle Safety Foundation text (from which the written portion of the test administered on Sunday came). My classes were at Murray High School and my bike for the course was a blue Yamaha XT225. Below are a few pictures of the setup. I now have my 649cc and below endorsement on my DL. It was nice only having to take the written test at the DLD since the MSF course eliminates the need for a road test. Now, to get a bike… a Ninja perhaps, anyone?


Categories: JPF

Copying Image Files to Build Folder in Eclipse

Part of my Google Summer of Code project this summer involved building a visualization tool to help examine trace files used by JPF Guided Test and a related under-approximation scheduler. The visualization tool is in the Guided Test repository. I was using Eclipse to manage the project. Everything built correctly but the program didn’t work because the icons were not in the build folder as expected. A quick hint from stackoverflow was that the solution is to use Ant.

<target name="-pre-jar" description="Copy Images">
  <property name="images.dir" value="build/main/edu/byu/cs/guided/search/visualize/graphics" />

  <copy todir="${images.dir}">
    <fileset dir="./src/main/edu/byu/cs/guided/search/visualize/graphics" />
  </copy>
  <echo level="info" message="Visualization icons was copied."/>
</target>

The key is to use the “-pre-jar” target in the build.xml file to copy the files into the right spot. This change was part of the visualization check-in into the repository. Some documentation on Ant targets is available in the Apache Ant User Manual. This StackOverflow entry on adding resource files to a jar file with Ant has some useful hints as well.


Categories: Eclipse

Attaching Java Source Files to an Eclipse JRE

As per this ubuntu thread, the solution is:

  1. Window > Preferences > Java > Installed JREs.
  2. Double click on the JRE for which you want to attach source code.
  3. Under “JRE System Libraries”, select rt.jar.
  4. Click on the “Source Attachment…” button.
  5. Supply a path to the source zip file, e.g. C:/Program Files/Java/jdk1.6.0_23/src.zip

That zip file was already on my system (since the JDK was installed) but some projects were using the JRE rather than the JDK. Therefore, I needed to specify the JDK source zip file for the JREs as well.