acl2 / acl2

ACL2 System and Books as Maintained by the Community
http://www.cs.utexas.edu/users/moore/acl2
Other
364 stars 100 forks source link

OR gate encounters error #392

Open ragerdl opened 9 years ago

ragerdl commented 9 years ago

This may be too academic in nature to warrant prioritizing, but the included code for gate.lisp, below, generates an error about an unnamed gate instance:

; SV::MODHIER-LOOPFREE-P: 0.00 seconds, 2,304 bytes.
; SV::MODULE->DB: 0.00 seconds, 60,288 bytes.
; SV::MODALIST-NAMED->INDEXED: 0.00 seconds, 1,456 bytes.

HARD ACL2 ERROR in SV::DEFSVTV-MAIN:  Error flattening design: Error
indexing wire names: Did not find wire: ("unnamed_gateinst_1" . "out")
in module OR2

=== begin gate.v===

module OR2  ( a, b, out );
    input   a;
    input   b;
    output  out;

    or (out, a, b);
endmodule

=== begin gate.lisp===

(in-package "SV")

(include-book "centaur/sv/top" :dir :system)
(include-book "centaur/vl/loader/top" :dir :system)
(include-book "centaur/gl/gl" :dir :system)
(include-book "centaur/aig/g-aig-eval" :dir :system)
(include-book "tools/plev-ccl" :dir :system)
(include-book "centaur/misc/memory-mgmt" :dir :system)

(gl::def-gl-clause-processor sv-tutorial-glcp)

(defconsts (*or-vl-design* state)
  (b* (((mv loadresult state)
        (vl::vl-load (vl::make-vl-loadconfig
                      :start-files '("gate.v")))))
    (mv (vl::vl-loadresult->design loadresult) state)))

(vl::cw-unformatted
   (vl::vl-reportcard-to-string (vl::vl-design-reportcard *or-vl-design*)))

(defconsts (*or-svex-design* *or-simplified-good* *or-simplified-bad*)
    (b* (((mv errmsg svex-design good bad)
          (vl::vl-design->svex-design "OR2" *or-vl-design*
                                      (vl::make-vl-simpconfig))))
      (and errmsg (raise "~@0~%" errmsg))
      (mv svex-design good bad)))

(vl::cw-unformatted
   (vl::vl-pps-modulelist (vl::vl-design->mods *or-simplified-good*)))

(defsvtv or-test-vector
  :mod *or-svex-design*
  :inputs '(("a" a _)
            ("b" b _))
  :outputs '(("out" out _)))

This is with version 16345 of CCL and a version of the ACL2 repository from the night of 5/26/2015.

As always, maybe there's a goofy typo.

ragerdl commented 9 years ago

My work-around, in case anyone is interested. Note that my original OR2 called OR with a delay, which is why I've added it to this example. I have no idea whether delays are supported (what would that even mean in a simulation system that's specified at the granularity of a half clock cycle), but I'd be surprised if they are.

module OR2  ( a, b, out );
    input   a;
    input   b;
    output  out;
   assign #20 out = a | b;
endmodule