← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2000/manolios/pipeline/pipeline/non-deterministic-systems/128/netlist/ma128intnet-ma128intserial.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2000/manolios/pipeline/pipeline/non-deterministic-systems/128/netlist/ma128intnet-ma128intserial.lisp
 
1
;  Copyright (C) 2000 Panagiotis Manolios
 
2
 
 
3
;  This program is free software; you can redistribute it and/or modify
 
4
;  it under the terms of the GNU General Public License as published by
 
5
;  the Free Software Foundation; either version 2 of the License, or
 
6
;  (at your option) any later version.
 
7
 
 
8
;  This program is distributed in the hope that it will be useful,
 
9
;  but WITHOUT ANY WARRANTY; without even the implied warranty of
 
10
;  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
11
;  GNU General Public License for more details.
 
12
 
 
13
;  You should have received a copy of the GNU General Public License
 
14
;  along with this program; if not, write to the Free Software
 
15
;  Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 
16
 
 
17
;  Written by Panagiotis Manolios who can be reached as follows.
 
18
 
 
19
;  Email: pete@cs.utexas.edu
 
20
 
 
21
;  Postal Mail:
 
22
;  Department of Computer Science
 
23
;  The University of Texas at Austin
 
24
;  Austin, TX 78701 USA
 
25
 
 
26
(in-package "ACL2")
 
27
 
 
28
(include-book "ma128intnet")
 
29
 
 
30
(generate-full-system maserial-step maserial-p manet-step manet-p 
 
31
                      manet-to-maserial good-manet manet-rank)
 
32
 
 
33
(in-theory (disable n convert-regs value-of update-valuation ALU-output excp
 
34
                    b-to-num latch1 serial-excp serial-ALU net-excp net-ALU))
 
35
 
 
36
(prove-web maserial-step maserial-p manet-step manet-p manet-to-maserial manet-rank)
 
37
 
 
38
(wrap-it-up maserial-step maserial-p manet-step manet-p 
 
39
            good-manet manet-to-maserial manet-rank)